In homotopy type theory, we say that a function $f$ is an equivalence between two types $A$ and $B$, if the inverse image of all points is contractible (as per say the n-lab or Paolo's Capriotti's Agda formalization). The "problem" with this definition is that if $A$ is a function type, the resulting definition asks for (propositional) equality of functions.

Equivalently, one could proceed as per section 2.4 of the HoTT book and define equivalence via quasi-inverse (which is the route we've chosen).

But this makes no actual difference: while one can ask if two equivalences are equivalent, the unwinding of the definitions still ends up asking if two functions are equal.

More precisely, question #1 is: given two equivalences $eq_1,\ eq_2 : A \simeq B$, how do I define a concept $eq_1 \approxeq eq_2$ that properly expresses that $eq_1$ and $eq_1$ are equivalent equivalences without resorting to extensionality?

One of my attempts (in Agda), reads as follows:

```
record _≋′_ {ℓ ℓ' : Level} {A : Set ℓ} {B : Set ℓ'} (eq₁ eq₂ : A ≃ B) : Set (ℓ ⊔ ℓ') where
constructor eq′
field
pA : A ≃ A -- automorphism of A
pB : B ≃ B -- automorphism of B
f≡ : ∀ x → eq₁ ⋆ x P.≡ (pB ● (eq₂ ● pA)) ⋆ x
g≡ : ∀ x → (sym≃ eq₁) ⋆ x P.≡ (pA ● (sym≃ eq₂ ● pB)) ⋆ x
```

where $\star$ is often called happly, and ● is composition of equivalences. But I must admit that this somehow doesn't feel quite right (even though it works perfectly well for my application).

Question #2: is there a unique definition of *equivalence* which would properly unify these? [I suspect that such a definition may end up having to be indexed by h-level].

notequivalent to the type of equivalences (2.4.11) and should not be used as a substitute. $\endgroup$ – Andrej Bauer Aug 19 '15 at 14:26