2-adjoint equivalences in homotopy type theory

There are numerous notions of equivalence in homotopy type theory: bi-invertible maps, contractible maps, and half adjoint equivalences. Other natural choices, such as quasi-invertible maps and adjoint equivalences, while logically equivalent to the above, are not propositions, making them unsuitable to serve as the definition of an equivalence. One can use a simple semantical argument, which in essence comes down to analyzing subcomplexes of the nerve of the groupoid $(0\cong 1)$, to see why some definitions work and others do not. The conclusion here is that while the definition as a “half $n$-adjoint equivalence” gives us a proposition, the definition as a “(full) $n$-adjoint equivalence” does not.

In this paper, we take the first step towards expressing these results internally in type theory, putting special emphasis on their formalization. In particular, we revisit the notions of a quasi-invertible map, a half adjoint equivalence, and an adjoint equivalence, giving the formal proofs of their expected properties. Our proofs are more modular than those given in [Uni13], and help improve efficiency. We then turn our attention to corresponding notions arising from $2$-adjunctions, namely half $2$-adjoint equivalences and (full) $2$-adjoint equivalences, and show that while the former is always a proposition, the latter fails to be one in general.

As indicated above, the results proven here certainly will not come as a surprise to experts and they constitute merely the first step towards understanding general $n$-adjoint equivalences. One can therefore envision future work in which the notions of $3$-, $4$-, …and, more generally, $n$-adjoint equivalence are studied. We have chosen not to pursue this direction, simply because the corresponding notions of $3$-, $4$-, and $n$-adjunction have not — to our knowledge — received rigorous treatment in literature on category theory. In particular, it is not immediately clear what the higher-dimensional analog of the coherences appearing in the swallow-tail identities ought to be (cf. $\mathsf{Coh}\>\eta$ in Definition 3.1). Having said that, we believe that the approach developed here can serve as a blueprint for proving analogous properties of $n$-adjoint equivalences when these notions are introduced.

These results have been formalized using the Lean Theorem Prover, version 3.4.2 (https://github.com/leanprover/lean) as part of the HoTT in Lean 3 library (https://github.com/gebner/hott3); the formalization consists of 528 lines of code across 3 files and may be found in the directory hott3/src/hott/types/2_adj. We write file/name for a newly-formalized result, where file denotes the file it is found in and name denotes the name of the formal proof in the code.

Section 1 recalls the necessary background on equivalences which will be used throughout. Section 2 introduces new formal proofs that the types of quasi-inverses and adjoint equivalences are not propositions. Note that specific examples where this fails are presented, but not formally proven since the current version of the HoTT in Lean 3 library does not contain induction principles for the higher inductive types $S^{1}$ and $S^{2}$. Section 3 introduces half 2-adjoint equivalences, which are propositions containing the data of adjoint equivalences, as well as 2-adjoint equivalences, which are non-propositions related to both quasi-inverses and adjoint equivalences.

We largely adopt the notation of [Uni13], with additional and differing notation stated here. We notate the $\mathsf{ap}$ function for $f:A\to B$ by

For $\mathsf{ap}_{2}$, the action of $f$ on 2-dimensional paths, we write

We write $\mathsf{refl}$ for the homotopy $\lambda x.\mathsf{refl}_{x}\colon\mathsf{id}_{A}\sim\mathsf{id}_{A}$. For a homotopy $H:f\sim g$ between dependent functions $f,g:\prod\limits_{x:A}Bx$ and a non-dependent function $h:C\to A$, we write

for the composition of $H$ and $h$. If $f,g:A\to B$ are non-dependent and we instead have $h:B\to C$, we write

for the composition of $h[-]$ and $H$. Given an additional homotopy $H^{\prime}:f\sim g$ and $\alpha:H\sim H^{\prime}$, we similarly write

for the composition of $h\llbracket-\rrbracket$ and $\alpha$. Lastly, for $H:f\sim g$ and $H^{\prime}:g\sim h$, we write transitivity of homotopies as

in path-concatenation order.

[adj/qinv, adj/is_hadj_l] A function $f:A\to B$

1. (1)

   has a quasi-inverse if the following type is inhabited:

   $$\mathsf{qinv}\>f:\equiv\sum_{g:B\to A}gf\sim\mathsf{id}_{A}\times fg\sim\mathsf{id}_{B}.$$

2. (2)

   is a half-adjoint equivalence if the following type is inhabited:

   $$\mathsf{ishadj}\>f:\equiv\sum_{g:B\to A}\ \sum_{\eta:gf\sim\mathsf{id}_{A}}\ \sum_{\varepsilon:fg\sim\mathsf{id}_{B}}f[\eta]\sim\varepsilon_{f}.$$

3. (3)

   is a left half-adjoint equivalence if the following type is inhabited:

   $$\mathsf{ishadjl}\>f:\equiv\sum_{g:B\to A}\ \sum_{\eta:gf\sim\mathsf{id}_{A}}\ \sum_{\varepsilon:fg\sim\mathsf{id}_{B}}\eta_{g}\sim g[\varepsilon].$$

   For types $A,B:\mathcal{U}$, the type of equivalences between $A$ and $B$ is:

   $$A\simeq B:\equiv\sum_{f:A\to B}\mathsf{ishadj}\>f.$$

[[Uni13, Lem. 4.2.2, Thms. 4.2.3, 4.2.13]] For $f:A\to B$, there are maps

where the top two types are propositions. ∎

The perhaps most intuitive definition of an equivalence between types $A,B:\mathcal{U}$ is that of a quasi-inverse. However, as this type is not a proposition, we define equivalences to be half adjoint equivalences. Since both half and left half adjoint equivalences are propositional types, one could also define the type of equivalences to be left half adjoint equivalences.

With a well-behaved notion of equivalence, we present the remaining lemmas to be used throughout.

[[Uni13, Lem. 4.2.5]] For any $f:A\to B$, $y:B$ and $(x,p),(x^{\prime},p^{\prime}):\mathsf{fib}_{f}\>y$, we have

[[Uni13, Thm. 4.2.6]] If $f:A\to B$ is a half-adjoint equivalence, then for any $y:B$ the fiber $\mathsf{fib}_{f}\>y$ is contractible. ∎

We present a proof that the type of quasi-inverses is not a proposition, using Lemma 2 for increased modularity over the proof presented in [Uni13, Lem. 4.1.1].

This result implies that any type with non-trivial $\pi_{1}$ may be used to construct non-trivial inhabitants of this type. For instance, since $\pi_{1}(S^{1})=\mathbb{Z}$, we have:

Conceptually, this proof takes the pair $(g,\eta)$ and uses Lemma 2 to contract it so that only one homotopy remains. This differs from the proof in [Uni13], which uses function extensionality to write the homotopies as paths and contracts using based path induction. This proof modularizes the proof in [Uni13] by packaging function extensionality and rewriting of contractible types into one result, simplifying both the proof and the formalization.

Thus, the type of half and left half adjoint equivalences each append an additional coherence to contract with the remaining homotopy. However, appending both coherences gives us a non-proposition. {defi}[adj/adj] Given $f:A\to B$, the structure of an adjoint equivalence on $f$ is the type:

This result implies that any type with non-trivial $\pi_{2}$ may be used to construct non-trivial inhabitants of this type. In particular, $\pi_{2}(S^{2})=\mathbb{Z}$ proves the following:

This is a solution to Exercise 4.1 in [Uni13]. As before, this proof uses Lemma 2 to contract the pairs $(g,\eta)$ and $(\varepsilon,\tau)$ so that a single homotopy remains. Trying to apply path induction directly requires an equivalence which writes each homotopy as an equality; a formal proof using function extensionality for such an equivalence along with path induction reaches 60 lines of code (varying by format, syntax choice, etc.). By modularizing the case of $\mathsf{qinv}$, this proof is reduced to manipulating $\Sigma$-types and applying Lemma 2 twice, with the formal proof in the library being 23 lines of code.

As in the case of $\mathsf{qinv}$, we expect there is an additional coherence that may be appended to the type $\mathsf{adj}\>f$ to create a proposition. To define this coherence, we use the following homotopy:

With this, we define the type of half 2-adjoint equivalences. {defi}[two_adj/is_two_hae] A function $f:A\to B$ is a half 2-adjoint equivalence if the following type is inhabited:

In parallel with adjoint equivalences, we give a definition which uses an alternate coherence. {defi}[two_adj/is_two_hae_l] A function $f:A\to B$ is a left half 2-adjoint equivalence if the following type is inhabited:

To show the type of half 2-adjoint equivalences is a proposition, we prove the following lemma:

Parallels of these proofs are used to obtain similar results about left half two-adjoint equivalences as well.

As well, either half adjoint equivalence may be promoted to the alternate half 2-adjoint equivalence.

This implies that an adjoint equivalence may be promoted to either half 2-adjoint equivalence.

Finally, we have that the half 2-adjoint and left half 2-adjoint equivalences are logically equivalent.

We summarize the properties of these 2-adjoint equivalances with the following diagram of maps:

where rows 1 and 3 are propositions.

As before, appending either one of these coherences yields a proposition, but appending both coherences yields a non-proposition once more. {defi}[two_adj/two_adj] Given $f:A\to B$, the structure of a 2-adjoint equivalence on $f$ is the type:

Once again, this result implies any type with non-trivial $\pi_{3}$ may be used to construct non-trivial inhabitants of this type. We know $\pi_{3}(S^{2})=\mathbb{Z}$, which proves:

Proving this result using function extensionality directly and path induction requires an equivalence that writes homotopies as equalities. By modularizing the case of $\mathsf{qinv}$, similar to the analogous proof for $\mathsf{adj}$, this result may be proven by manipulating $\Sigma$-types and applying Lemma 2 three times, with the formal proof in the library being 44 lines of code. As with $\mathsf{adj}$, one would expect this approach to be 40 to 80 lines shorter than one which uses function extensionality directly.

This work was carried out when the first, second, and fourth authors were undergraduates at the University of Western Ontario and was supported through two Undergraduate Student Research Awards and a Discovery Grant, all funded by the Natural Sciences and Engineering Research Council (NSERC) of Canada. We thank NSERC for its generosity.