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 B\bf{B} be a bicategory, A,B:BA, B : \bf{B} be objects, and f:A→Bf : A \to B and g:B→Ag : B \to A be 1-cells. Generalising the situation where ff and gg are functors, we say they are adjoints if there exist 2-cells η:id→gf\eta : \id{id} \to gf and Ρ:fg→id\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):