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].