open import Cat.Bi.Base open import Cat.Prelude import Cat.Diagram.Monad as Cat import Cat.Reasoning as Cr module Cat.Bi.Diagram.Adjunction where

# Adjunctions in a bicategoryπ

Let
$\bf{B}$
be a bicategory,
$A, B : \bf{B}$
be objects, and
$f : A \to B$
and
$g : B \to A$
be 1-cells. Generalising the situation where
$f$
and
$g$
are functors, we say they are **adjoints** if there exist
2-cells
$\eta : \id{id} \to gf$
and
$\eps : fg \to \id{id}$
(the **unit** and **counit** respectively),
satisfying the equations

and

called the **triangle identities** (because of their
shape) or **zigzag identities** (because it sounds
cool).

record _β£_ {a b : B.Ob} (f : a B.β¦ b) (g : b B.β¦ a) : Type ββ² where field Ξ· : B.id B.β (g B.β f) Ξ΅ : (f B.β g) B.β B.id zig : B.Hom.id β‘ B.Ξ»β f B.β (Ξ΅ B.β f) B.β B.Ξ±β f g f B.β (f B.βΆ Ξ·) B.β B.Οβ f zag : B.Hom.id β‘ B.Οβ g B.β (g B.βΆ Ξ΅) B.β B.Ξ±β g f g B.β (Ξ· B.β g) B.β B.Ξ»β g

Working in a fully weak bicategory means the triangle identities, rather than simply expressing a compatibility relation between $\eta$ and $\eps$ as is the case for adjoint functors, instead exhibit a complicated compatibility relation between $\eta$, $\eps$, and the structural isomorphisms (the unitors and associator) of the ambient bicategory.

We have taken pains to draw the triangle identities as triangles, but counting the morphisms involved youβll find that they really want to be commutative pentagons instead (which we draw in this website as commutative altars):