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$ Aug 19, 2015 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$ Aug 19, 2015 at 17:46
  • $\begingroup$ @AndrejBauer: I was working with quasi-inverses, but you are right, I should work with proper equivalences instead. $\endgroup$ Aug 19, 2015 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$ Aug 19, 2015 at 18:05

1 Answer 1

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$ Aug 19, 2015 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$ Aug 19, 2015 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$ Aug 19, 2015 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$ Aug 19, 2015 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$ Aug 20, 2015 at 3:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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