3
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Aug 19 '15 at 14:26
  • 2
    $\begingroup$ You might be interested in Mike Shulman's blog post "Universal properties without function extensionality" (homotopytypetheory.org/2014/11/02/…) $\endgroup$ – Jason Gross Aug 19 '15 at 17:46
  • $\begingroup$ @AndrejBauer: I was working with quasi-inverses, but you are right, I should work with proper equivalences instead. $\endgroup$ – Jacques Carette Aug 19 '15 at 18:04
  • $\begingroup$ @JasonGross: I had read it, but forgot that it was topical. Thanks for the reminder, I am re-reading it now. $\endgroup$ – Jacques Carette Aug 19 '15 at 18:05
2
$\begingroup$

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?

$\endgroup$
9
  • $\begingroup$ 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. $\endgroup$ – Jacques Carette Aug 19 '15 at 17:56
  • $\begingroup$ Actually, I guess what I really need is to unravel (2.4.11) completely, as I don't want just the first component to be a homotopy, but the inverses as well. $\endgroup$ – Jacques Carette Aug 19 '15 at 19:12
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Aug 19 '15 at 19:12
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Aug 19 '15 at 19:21
  • $\begingroup$ I am not sure what Agda's problem is, but I think it's a problem with Agda or with your use of it; as Andrej said, you shouldn't need to even mention the inverse in defining what it means for two equivalences to be equal. $\endgroup$ – Mike Shulman Aug 20 '15 at 3:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.