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](http://ncatlab.org/nlab/show/equivalence+in+homotopy+type+theory) or Paolo's Capriotti's [Agda formalization](http://www.paolocapriotti.com/agda-base/trunc/hott.equivalence.core.html#1)). 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](http://homotopytypetheory.org/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].



Defining equivalence of equivalences without assuming extensionality
Equivalences $e\_1, e\_2 : A \simeq B$ are elements of the type $A \simeq B$. Recall from the HoTT book (2.4.11) that $A \simeq B$ is defined as $\sum\_{f : A \to B} \mathsf{isequiv}(f)$. The easiest way to compare elements is of course just (propostional) equality. Because $\mathsf{isprop}(f)$ is a proposition, $e\_1 = e\_2$ reduces to $f\_1 = f\_2$, as you note. Without function extensionality it is typically quite hard to prove equality of functions, so you could weaken the condition to $f\_1$ and $f\_2$ being homotopic: $\prod\_{x : A} f\_1 x = f\_2 x$. It's a standard trick. Or are you after something else?


