# Defining equivalence of equivalences without assuming extensionality

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

• What do you mean "quasi-inverses as per section 2.4"? The type of quasi-inverses (2.4.5) is not equivalent to the type of equivalences (2.4.11) and should not be used as a substitute. – Andrej Bauer Aug 19 '15 at 14:26
• You might be interested in Mike Shulman's blog post "Universal properties without function extensionality" (homotopytypetheory.org/2014/11/02/…) – Jason Gross Aug 19 '15 at 17:46
• @AndrejBauer: I was working with quasi-inverses, but you are right, I should work with proper equivalences instead. – Jacques Carette Aug 19 '15 at 18:04
• @JasonGross: I had read it, but forgot that it was topical. Thanks for the reminder, I am re-reading it now. – Jacques Carette Aug 19 '15 at 18:05

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?
• This is what I am after. I definitely want to weaken $f_1 = f_2$ to just being a homotopy. But if I do that, Agda complains about lots of unresolved metas. Basically I need to weaken both $f$ and $g$ (inverse of $f$) for the metas to resolve. I was hoping there was a 'deep' reason for this. – Jacques Carette Aug 19 '15 at 17:56
• You should also specify that the homotopy between $f_1$ and $f_2$ takes $\mathsf{isequiv}(f_1)$ to $\mathsf{isequiv}(f_1)$, whatever that means. – Andrej Bauer Aug 19 '15 at 19:12
• I wonder if my last comment makes any sense. If $f_1$ is an equivalence and is homotopic to $f_2$ then surely $f_2$ is an equivalence. – Andrej Bauer Aug 19 '15 at 19:21