open import Cat.Diagram.Initial
open import Cat.Instances.Comma
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning

module Cat.Functor.Adjoint where

Adjoint functors🔗

Category theory is, in general, the study of how things can be related. For instance, structures at the level of sets (e.g. the collection of natural numbers) are often interestingly related by propositions (i.e. the proposition xyx \le y). Structures at the level of groupoids (e.g. the collection of all sets) are interestingly related by sets (i.e. the set of maps xyx \to y). Going further, we have structures at the level of 2-groupoids, which could be given an interesting category of relations, etc.

A particularly important relationship is, of course, “sameness.” Going up the ladder of category number, we have equality at the (-1)-level, isomorphism at the 0-level, and what’s generally referred to as “equivalence” at higher levels. It’s often interesting to weaken these relations, by making some components directed: This starts at the level of categories, where “directing” an equivalence gives us the concept of adjunction.

An equivalence of categories between C\ca{C} and D\ca{D} is given by a pair of functors L:CD:RL : \ca{C} \leftrightarrows \ca{D} : R, equipped with natural isomorphisms η:Id(RL)\eta : \id{Id} \cong (R \circ L) (the “unit”) and ε:(LR)Id\eps : (L \circ R) \cong \id{Id} (the “counit”). We still want the correspondence to be bidirectional, so we can’t change the types of RR, LL; What we can do is weaken the natural isomorphisms to natural transformations. The data of an adjunction starts as such:

record _⊣_ (L : Functor C D) (R : Functor D C) : Type (adj-level C D) where
    module C = Precategory C
    module D = Precategory D

    unit   : Id => (R F∘ L)
    counit : (L F∘ R) => Id

  module unit = _=>_ unit
  module counit = _=>_ counit renaming (η to ε)

Unfortunately, the data that we have here is not particularly coherent. The unit and counit let us introduce RLR\circ L and eliminate LRL\circ R in a composition, which gives us two ways of mapping LLL \To L. One is the identity, and the other is going through the unit: LLRLLL \To L\circ R\circ L \To L (the situation with RR is symmetric). We must impose further equations on the natural transformations to make sure these match:

    zig :  {A}  counit.ε (F₀ L A) D.∘ F₁ L (unit.η A)
    zag :  {B}  F₁ R (counit.ε B) C.∘ unit.η (F₀ R B)

infixr 15 _⊣_

These are called “triangle identities” because of the shape they have as commutative diagrams:

Universal morphisms🔗

Another perspective on adjoint functors is given by finding “most efficient solutions” to the “problem” posed by a functor. For instance, the (ff) inclusion of prosets into strict precategories poses the problem of turning a precategory into a proset. While this can’t be done in a 1:1 way (precategories are strictly more general than prosets), we can still ponder whether there is some “most efficient” way to turn a category into a proset.

While we can’t directly consider maps from precategories to proset, we can consider maps from precategories to the inclusion of a proset; Let us write C\ca{C} for a generic precategory, P\ca{P} for a generic proset, and U(P)U(\ca{P}) for P\ca{P} considered as a precategory. Any functor CU(P)\ca{C} \to U(\ca{P}) can be seen as “a way to turn C\ca{C} into a proset,” but not all of these can be the “most efficient” way. In fact, there is a vast sea of uninteresting ways to turn a precategory into a proset: turn them all into the terminal proset!

A “most efficient” solution, then, would be one through which all others factor. A “universal” way of turning a strict precategory into a proset: A universal morphism from C\ca{C} to UU. The way we think about universal morphisms (reusing the same variables) is as initial objects in the comma category CU\ca{C} \swarrow U, where that category is conceptualised as being “the category of maps from C\ca{C} to UU.

  Universal-morphism : C.Ob  Functor D C  Type _
  Universal-morphism X R = Initial (X  R)

Abstracting away, suppose that R:DCR : D \to C has universal morphisms for every object of CC. To show the correspondence between these two ideas of adjunction, we show that this assignment extends to a functor L:CDL : C \to D, with LRL \dashv R as defined above.

Defining the L🔗

We first show that the assignment of universal morphisms restricts to a functorial assignment L:CDL : C \to D. Recall that an object in XRX \swarrow R is given by a codomain yy and a map XR(y)X \to R(y). We define L0(x)L_0(x) to be the codomain of the universal morphism:

  L₀ : C.Ob  D.Ob
  L₀ x = universal-map-for x .bot .↓Obj.y

  L₀′ : (c : C.Ob)  C.Hom c (R.₀ (L₀ c))
  L₀′ x = universal-map-for x .bot .map

Given an arrow aba \to b in C\ca{C}, we can send it to a uniquely-determined object in aRa \swarrow R: We take the universal arrow assigned to bb (an object of bRb \swarrow R), and precompose with aa. This object will then serve as the domain of the morphism part of LL, which is given by the unique assignment arrows out of the initial object in aRa \swarrow R (see lift↓ below).

    to-ob :  {a b}  C.Hom a b  (a  R) .Precategory.Ob
    to-ob {a} {b} h = record { map = L₀′ b C.∘ h }

    lift↓ :  {x y} (g : C.Hom x y)
           Precategory.Hom (x  R) (universal-map-for x .bot) (to-ob g)
    lift↓ {x} {y} g = ¡ (universal-map-for x) {to-ob g}

  L₁ :  {a b}  C.Hom a b  D.Hom (L₀ a) (L₀ b)
  L₁ {a} {b} x = lift↓ x .β
It now suffices to show the functor identities hold for L₁. They follow essentially from the uniqueness of maps out of an initial object.
  private abstract
    L-id :  {a}  L₁ ( {a}) {L₀ a}
    L-id {a} = ap β (¡-unique (universal-map-for a)
                      (record { sq = C.elimr refl
                                  ·· C.elimr refl
                                  ·· sym (C.eliml R.F-id) }))

    lemma :  {x y z} (f : C.Hom y z) (g : C.Hom x y)
           R.₁ (L₁ f D.∘ L₁ g) C.∘ (L₀′ x)
           to-ob (f C.∘ g) .map C.∘
    lemma {x} {y} {z} f g =
      R.₁ (lift↓ f .β D.∘ lift↓ g .β) C.∘ (L₀′ x)       ≡⟨ C.pushl (R.F-∘ _ _) 
      R.₁ (lift↓ f .β) C.∘ R.₁ (lift↓ g .β) C.∘ (L₀′ x) ≡⟨ ap (R.₁ (lift↓ f .β) C.∘_) (sym (lift↓ g .↓Hom.sq)  C.idr _) 
      R.₁ (lift↓ f .β) C.∘ L₀′ y C.∘ g                  ≡⟨ C.extendl (sym (lift↓ f .↓Hom.sq)  C.idr _) 
      L₀′ z C.∘ f C.∘ g                                 ≡˘⟨ C.idr _ ≡˘
      to-ob (f C.∘ g) .map C.∘                     

    L-∘ :  {x y z} (f : C.Hom y z) (g : C.Hom x y)
         L₁ (f C.∘ g)  L₁ f D.∘ L₁ g
    L-∘ f g = ap β (¡-unique (universal-map-for _) (record { sq = sym (lemma f g) }))

That out of the way, we have our LL functor. We now have to show that it defines a left adjoint to the RR we started with.

  universal-maps→L : Functor C D
  universal-maps→L .F₀ = L₀
  universal-maps→L .F₁ = L₁
  universal-maps→L .F-id = L-id
  universal-maps→L .F-∘ = L-∘

Building the adjunction🔗

We now prove that LRL \dashv R, which, recall, means giving natural transformations η:Id(RFL)\eta : \id{Id} \To (R F\circ L) (the adjunction unit) and ε:(LR)Id\eps : (L \circ R) \To \id{Id} (the adjunction counit). We begin with the counit, since that’s more involved.

The construction begins by defining a function mapd which sends each object of C\ca{C} to the initial object in xRx \swarrow R. Note that this is the same as L₀, but returning the entire object rather than a part of it.

    mapd :  (x : C.Ob)  Ob (x  R)
    mapd x = universal-map-for x .bot

Now for an object x:Dx : \ca{D}, we have R(x):CR(x) : \ca{C}, so by the assumption that RR has a collection of universal objects, the comma category R(x)RR(x) \swarrow R has an initial object; Let us write that object as (L(R(x)),!)(L(R(x)), !) — recall that here, !:R(x)RLR(x)! : R(x) \to RLR(x).

This means, in particular, that for any other object (y,f)(y, f) (with yDy \in \ca{D} and f:R(x)R(y)f : R(x) \to R(y) in C\ca{C}), there is a unique map mapd(x)(y,f)\id{mapd}(x) \to (y, f), which breaks down as a map β:L(R(x))y\beta : L(R(x)) \to y such that the square below commutes.

    ε :  (x : D.Ob)  Hom (R.₀ x  R) (mapd (R.₀ x)) _
    ε x = Initial.¡ (universal-map-for (R.₀ x)) {x = record { y = x ; map = }}

The magic trick is that, if we pick (x,id)(x, \id{id}) as the object of R(x)RR(x)\swarrow R to map into, then β\beta in the diagram above must be LR(x)xLR(x) \to x! We choose this map as our adjunction counit. A tedious calculation shows that this assignment is natural, essentially because β\beta is unique.

  universal-maps→L⊣R : universal-maps→L  R
  universal-maps→L⊣R .counit .η x = ε x .↓Hom.β
  universal-maps→L⊣R .counit .is-natural x y f =
    ap ↓Hom.β (
      ¡-unique₂ (universal-map-for (R.₀ x)) {record { map = R.₁ f }}
      (record { sq =
        R.₁ f C.∘                                          ≡⟨ C.idr _ 
        R.₁ f                                                   ≡˘⟨ C.cancell (sym (ε y .↓Hom.sq)  C.idr _) ≡˘
        R.₁ (ε y .β) C.∘ _ C.∘ R.₁ f                            ≡˘⟨ ap₂ C._∘_ refl (sym (lift↓ (R.₁ f) .↓Hom.sq)  C.idr _) ≡˘
        R.₁ (ε y .β) C.∘ R.₁ (L₁ (R.₁ f)) C.∘ mapd (R.₀ x) .map ≡⟨ C.pulll (sym (R.F-∘ _ _)) 
        R.₁ (ε y .β D.∘ L₁ (R.₁ f)) C.∘ mapd (R.₀ x) .map        })
      (record { sq =
        R.₁ f C.∘                               ≡˘⟨ ap (R.₁ f C.∘_) (sym (ε x .↓Hom.sq)  C.idr _) ≡˘
        R.₁ f C.∘ R.₁ (ε x .β) C.∘ mapd (R.₀ x) .map ≡⟨ C.pulll (sym (R.F-∘ _ _)) 
        R.₁ (f D.∘ ε x .β) C.∘ mapd (R.₀ x) .map      }))

For the adjunction unit, the situation is a lot easier. Recall that we defined L(x)L(x) on objects (L₀) to be the codomain part of the initial object of xRx \swarrow R; The map part of that object then gives us a natural family of morphisms xR(L(x))x \to R(L(x)). By definition. It’s so “by definition” that Agda can figure out the components by itself:

  universal-maps→L⊣R .unit .η x              = _
  universal-maps→L⊣R .unit .is-natural x y f = sym (C.idr _)  lift↓ f .↓Hom.sq

If you think back to the adjunction counit, you’ll recall that it satisfied a triangle that looks like the one below, and that the top map (the map component of the initial object) is what we defined the adjunction unit to be, so.. It’s zag.

  universal-maps→L⊣R .zag {x} = sym (ε x .↓Hom.sq)  C.idr _

The other triangle identity is slightly more annoying, but it works just as well. It follows from the uniqueness of maps out of the initial object:

  universal-maps→L⊣R .zig {x} =
    ap ↓Hom.β (
      ¡-unique₂ (universal-map-for x) {record { map = α }}
        (record { sq =
          α C.∘                     ≡⟨ C.idr _ 
          α                              ≡˘⟨ C.cancell (sym (ε (L₀ x) .↓Hom.sq)  C.idr _) ≡˘
          R.₁ _ C.∘ _ C.∘ α              ≡˘⟨ C.pullr (sym (lift↓ α .↓Hom.sq)  C.idr _) ≡˘
          (R.₁ _ C.∘ R.₁ (F₁ L α)) C.∘ α ≡˘⟨ ap (C._∘ α) (R.F-∘ _ _) ≡˘
          R.₁ (_ D.∘ F₁ L α) C.∘ α       
        (record { sq =  ap (C._∘ _) (sym R.F-id) })
    where α = L₀′ x
          L = universal-maps→L

From an adjunction🔗

To finish the correspondence, we show that any (left) adjoint functor LRL \dashv R defines a system of universal arrows R- \swarrow R; This means that, not only does a “universal way of solving RRgive a left adjoint to RR, it is a left adjoint to RR.

So, given an object xCx \in \ca{C}, we must find an object yy and a universal map xR(y)x \to R(y). Recall that, in the previous section, we constructed the left adjoint LL’s action on objects by using our system of universal arrows; Symetrically, in this section, we take the codomain to be y=L(x)y = L(x). We must then find an arrow xRLxx \to RLx, but this is exactly the adjunction unit η\eta!

  L⊣R→map-to-R :  x  Precategory.Ob (x  R)
  L⊣R→map-to-R x .↓Obj.x = tt
  L⊣R→map-to-R x .↓Obj.y = L.₀ x
  L⊣R→map-to-R x .↓ = adj.unit.η _

We must now show that the unit η\eta is universal among the pairs (y,f)(y, f), with ff a map xR(y)x \to R(y). Recall that for our object (Lx,η)(Lx, \eta) to be initial, we must find an arrow (y,f)(Lx,η)(y, f) \to (Lx, \eta), and prove that this is the only possible such arrow; And that morphisms in the comma category xRx \swarrow R break down as maps g:Lxyg : Lx \to y such that the triangle below commutes:

We can actually read off the map gg pretty directly from the diagram: It must be a map LxyLx \to y, but we’ve been given a map LRxxLRx \to x (the adjunction counit) and a map xRyx \to Ry; We may then take our gg to be the composite

LxLRyy Lx \to LRy \to y

    :  x  is-initial (x  R) (L⊣R→map-to-R x)
  L⊣R→map-to-R-is-initial x other-map .centre .↓Hom.α = tt
  L⊣R→map-to-R-is-initial x other-map .centre .↓Hom.β =
    adj.counit.ε _ D.∘ L.₁ (other-map .↓
  L⊣R→map-to-R-is-initial x other-map .centre .↓Hom.sq =
    sym (
      R.₁ (adj.counit.ε _ D.∘ L.₁ C.∘ adj.unit.η _       ≡⟨ ap₂ C._∘_ (R.F-∘ _ _) refl  sym (C.assoc _ _ _) 
      R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ C.∘ adj.unit.η _ ≡˘⟨ C.refl⟩∘⟨ _ _ _ ≡˘
      (R.₁ (adj.counit.ε _) C.∘ adj.unit.η _ C.∘         ≡⟨ C.cancell adj.zag                                                     ≡⟨ sym (C.idr _) C.∘                                            
    where module om = ↓Obj other-map

Checking that the triangle above commutes is a routine application of naturality and the triangle identities; The same is true for proving that the map gg above is unique.

  L⊣R→map-to-R-is-initial x other-map .paths y =
    ↓Hom-path _ _ refl (
      adj.counit.ε _ D.∘ L.₁                            ≡⟨ D.refl⟩∘⟨ L.expand (sym (C.idr _)  y .↓Hom.sq) 
      adj.counit.ε _ D.∘ L.₁ (R.₁ y.β) D.∘ L.₁ (adj.unit.η _)  ≡⟨ D.pulll ( _ _ _)  -- nvmd
      (y.β D.∘ adj.counit.ε _) D.∘ L.₁ (adj.unit.η _)          ≡⟨ D.cancelr adj.zig 
      module om = ↓Obj other-map
      module y = ↓Hom y

Hence, we can safely say that having a functor LL and an adjunction LRL \dashv R is the same thing as having a functor RR and a system of universal arrows into RR:

  L⊣R→universal-maps :  x  Universal-morphism x R
  L⊣R→universal-maps x = L⊣R→map-to-R x
  L⊣R→universal-maps x .Initial.has⊥ = L⊣R→map-to-R-is-initial x


Another view on adjunctions, one which is productive when thinking about adjoint endofunctors LRL \dashv R, is the concept of adjuncts. Any pair of natural transformations typed like a unit and counit allow you to pass between the Hom-sets hom(La,b)\hom(La,b) and hom(a,Rb)\hom(a,Rb), by composing the functorial action of LL (resp RR) with the natural transformations:

  L-adjunct :  {a b}  D.Hom (L.₀ a) b  C.Hom a (R.₀ b)
  L-adjunct f = R.₁ f C.∘ adj.unit.η _

  R-adjunct :  {a b}  C.Hom a (R.₀ b)  D.Hom (L.₀ a) b
  R-adjunct f = adj.counit.ε _ D.∘ L.₁ f

The important part that the actual data of an adjunction gets you is these functions are inverse equivalences between the hom-sets hom(La,b)hom(a,Rb)\hom(La,b) \cong \hom(a,Rb).

  L-R-adjunct :  {a b}  is-right-inverse (R-adjunct {a} {b}) L-adjunct
  L-R-adjunct f =
    R.₁ (adj.counit.ε _ D.∘ L.₁ f) C.∘ adj.unit.η _        ≡⟨ R.pushl refl 
    R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ f) C.∘ adj.unit.η _  ≡˘⟨ C.refl⟩∘⟨ _ _ _ ≡˘
    R.₁ (adj.counit.ε _) C.∘ adj.unit.η _ C.∘ f            ≡⟨ C.cancell adj.zag 

  R-L-adjunct :  {a b}  is-left-inverse (R-adjunct {a} {b}) L-adjunct
  R-L-adjunct f =
    adj.counit.ε _ D.∘ L.₁ (R.₁ f C.∘ adj.unit.η _)       ≡⟨ D.refl⟩∘⟨ L.F-∘ _ _ 
    adj.counit.ε _ D.∘ L.₁ (R.₁ f) D.∘ L.₁ (adj.unit.η _) ≡⟨ D.extendl ( _ _ _) 
    f D.∘ adj.counit.ε _ D.∘ L.₁ (adj.unit.η _)           ≡⟨ D.elimr adj.zig 

  L-adjunct-is-equiv :  {a b}  is-equiv (L-adjunct {a} {b})
  L-adjunct-is-equiv = is-iso→is-equiv
    (iso R-adjunct L-R-adjunct R-L-adjunct)

  R-adjunct-is-equiv :  {a b}  is-equiv (R-adjunct {a} {b})
  R-adjunct-is-equiv = is-iso→is-equiv
    (iso L-adjunct R-L-adjunct L-R-adjunct)