open import Cat.Bi.Base
open import Cat.Prelude

module Cat.Bi.Diagram.Adjunction where

open _=>_

module _ {o β ββ²} (B : Prebicategory o β ββ²) where
private module B = Prebicategory B


Let $\mathbf{B}$ be a bicategory, $A, B : \mathbf{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 : \operatorname{id}_{} \to gf$ and $\varepsilon : fg \to \operatorname{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 $\varepsilon$ as is the case for adjoint functors, instead exhibit a complicated compatibility relation between $\eta$, $\varepsilon$, 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):