Homotopy Type Theory left adjoint > history (Rev #1)

Idea

Many naturally arising functors in mathematics have adjoints. This makes them a useful thing to study.

Definition

A functor $F: A \to B$ is a left adjoint if there exists

A functor $G : B \to A$
A natural transformation $\eta:1_A \to G F$ (the unit).
A natural transformation $\epsilon G \to 1_B$ (the counit).
Which satisfy the triangle identities (a.k.a zig-zag identities)
- $(\epsilon F)(F \eta) = 1_F$
- $(G \epsilon)(\eta G) = 1_G$

Properties

Lemma 9.3.2

If $A$ s a category and $B$ is a precategory then the type “ $F$ is a left adjoint” is a mere proposition?.

Proof. Suppose we are given $(G, \eta, \epsilon)$ with the triangle identities and also $(G', \eta', \epsilon')$ . Define $\gamma: G \to G'$ to be $(G' \epsilon )(\eta G')$ . Then

\begin{aligned} \delta \gamma &= (G \epsilon')(\eta G')(G' \epsilon) (\eta' G)\\ &= (G \epsilon')(G F G' \epsilon_))\eta G' F G)(\eta' G)\\ &= (G \epsilon ')(G \epsilon' F G)(G F \eta' G)(\eta G)\\ &= (G \epsilon)(\eta G)\\ &= 1_G \end{aligned}

using Lemma 9.2.8 (see natural transformation) and the triangle identities. Similarly, we show $\gamma \delta=1_{G'}$ , so $\gamma$ is a natural isomorphism $G \cong G'$ . By Theorem 9.2.5 (see functor precategory), we have an identity $G=G'$ .

References

HoTT Book