open import Cat.Functor.Naturality
open import Cat.Diagram.Initial
open import Cat.Functor.Compose
open import Cat.Instances.Comma
open import Cat.Functor.Base
open import Cat.Prelude

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

module Cat.Functor.Adjoint where

private variable
  o h : Level
  C D E : Precategory o h

open Functor hiding (op)

adj-level : ∀ {o₁ h₁ o₂ h₂} (C : Precategory o₁ h₁) (D : Precategory o₂ h₂)
          → Level
adj-level {o₁ = o₁} {h₁} {o₂} {h₂} _ _ = o₁ ⊔ o₂ ⊔ h₁ ⊔ h₂

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 $x \leq 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 $x \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$ and $D$ is given by a pair of functors $L : C ⇆ D : R,$ equipped with natural isomorphisms $η : Id ≅ (R \circ L)$ (the “unit”) and $ε : (L \circ R) ≅ Id$ (the “counit”). We still want the correspondence to be bidirectional, so we can’t change the types of $R,$ $L;$ 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
  no-eta-equality
  private
    module C = Precategory C
    module D = Precategory D

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

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

  open unit using (η) public
  open counit using (ε) public

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

  field
    zig : ∀ {A} → ε (L .F₀ A) D.∘ L .F₁ (η A) ≡ D.id
    zag : ∀ {B} → R .F₁ (ε B) C.∘ η (R .F₀ B) ≡ C.id

infixr 15 _⊣_

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

{-
Characterising paths between adjoints.
-}
module _
  {L L' : Functor C D} {R R' : Functor D C}
  where
  private
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D

  module _
    {adj : L ⊣ R} {adj' : L' ⊣ R'}
    (p : L ≡ L') (q : R ≡ R')
    where
    private
      module adj = _⊣_ adj
      module adj' = _⊣_ adj'
      open Functor
      open _=>_

    adjoint-pathp
      : PathP (λ i → Id => q i F∘ p i) adj.unit adj'.unit
      → PathP (λ i → p i F∘ q i => Id) adj.counit adj'.counit
      → PathP (λ i → p i ⊣ q i) adj adj'
    adjoint-pathp r s i ._⊣_.unit = r i
    adjoint-pathp r s i ._⊣_.counit = s i
    adjoint-pathp r s i ._⊣_.zig {A} =
      is-prop→pathp (λ i → D.Hom-set _ _ (s i .η (p i .F₀ A) D.∘ p i .F₁ (r i .η A)) D.id)
        adj.zig adj'.zig i
    adjoint-pathp r s i ._⊣_.zag {A} =
      is-prop→pathp (λ i → C.Hom-set _ _ (q i .F₁ (s i .η A) C.∘ r i .η (q i .F₀ A)) C.id)
        adj.zag adj'.zag i

Adjuncts🔗

Another view on adjunctions, one which is productive when thinking about adjoint endofunctors $L ⊣ 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 (L a, b)$ and $Hom (a, R b),$ by composing the functorial action of $L$ (resp $R)$ with the natural transformations:

module _ {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) where
  private
    module L = Func L
    module R = Func R
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D
    module adj = _⊣_ adj

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

  R-adjunct : ∀ {a b} → C.Hom a (R.₀ b) → D.Hom (L.₀ a) b
  R-adjunct f = adj.ε _ 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 (L a, b) ≅ Hom (a, R b) .$

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

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

  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)

  module L-adjunct {a b} = Equiv (L-adjunct {a} {b} , L-adjunct-is-equiv)
  module R-adjunct {a b} = Equiv (R-adjunct {a} {b} , R-adjunct-is-equiv)

Furthermore, these equivalences are natural.

  L-adjunct-naturall
    : ∀ {a b c} (f : D.Hom (L.₀ b) c) (g : C.Hom a b)
    → L-adjunct (f D.∘ L.₁ g) ≡ L-adjunct f C.∘ g
  L-adjunct-naturall f g =
    R.₁ (f D.∘ L.₁ g) C.∘ adj.η _       ≡⟨ R.F-∘ _ _ C.⟩∘⟨refl ⟩≡
    (R.₁ f C.∘ R.₁ (L.₁ g)) C.∘ adj.η _ ≡⟨ C.extendr (sym $ adj.unit.is-natural _ _ _) ⟩≡
    (R.₁ f C.∘ adj.η _) C.∘ g           ∎

  L-adjunct-naturalr
      : ∀ {a b c} (f : D.Hom b c) (g : D.Hom (L.₀ a) b)
      → L-adjunct (f D.∘ g) ≡ R.₁ f C.∘ L-adjunct g
  L-adjunct-naturalr f g = C.pushl (R.F-∘ f g)

  L-adjunct-natural₂
      : ∀ {a b c d} (f : D.Hom a b) (g : C.Hom c d) (x : D.Hom (L.F₀ d) a)
      → L-adjunct (f D.∘ x D.∘ L.₁ g) ≡ R.₁ f C.∘ L-adjunct x C.∘ g
  L-adjunct-natural₂ f g x =
    L-adjunct-naturalr f (x D.∘ L.₁ g) ∙ ap (R.₁ f C.∘_) (L-adjunct-naturall x g)

  R-adjunct-naturall
      : ∀ {a b c} (f : C.Hom b (R.₀ c)) (g : C.Hom a b)
      → R-adjunct (f C.∘ g) ≡ R-adjunct f D.∘ L.₁ g
  R-adjunct-naturall f g = D.pushr (L.F-∘ f g)

  R-adjunct-naturalr
    : ∀ {a b c} (f : D.Hom b c) (g : C.Hom a (R.₀ b))
    → R-adjunct (R.₁ f C.∘ g) ≡ f D.∘ R-adjunct g
  R-adjunct-naturalr f g =
    adj.ε _ D.∘ L.₁ (R.₁ f C.∘ g)     ≡⟨ D.refl⟩∘⟨ L.F-∘ _ _ ⟩≡
    adj.ε _ D.∘ L.₁ (R.₁ f) D.∘ L.₁ g ≡⟨ D.extendl (adj.counit.is-natural _ _ _) ⟩≡
    f D.∘ (adj.ε _ D.∘ L.₁ g)         ∎

  R-adjunct-natural₂
    : ∀ {a b c d} (f : D.Hom a b) (g : C.Hom c d) (x : C.Hom d (R.F₀ a))
    → R-adjunct (R.₁ f C.∘ x C.∘ g) ≡ f D.∘ R-adjunct x D.∘ L.₁ g
  R-adjunct-natural₂ f g x =
    R-adjunct-naturalr f (x C.∘ g) ∙ ap (f D.∘_) (R-adjunct-naturall x g)

  R-adjunct-ap
    : ∀ {a b c}
    → {f : D.Hom b c} {g : C.Hom a (R.₀ b)} {h : C.Hom a (R.₀ c)}
    → R.₁ f C.∘ g ≡ h
    → f D.∘ R-adjunct g ≡ R-adjunct h
  R-adjunct-ap p = sym (R-adjunct-naturalr _ _) ∙ ap R-adjunct p

  R-adjunct-square
    : ∀ {a b c d}
    → {p1 : C.Hom a (R.₀ b)} {f : D.Hom b d} {p2 : C.Hom a (R.₀ c)} {g : D.Hom c d}
    → R.₁ f C.∘ p1 ≡ R.₁ g C.∘ p2
    → f D.∘ R-adjunct p1 ≡ g D.∘ R-adjunct p2
  R-adjunct-square sq =
    sym (R-adjunct-naturalr _ _) ·· ap R-adjunct sq ·· R-adjunct-naturalr _ _

Free objects🔗

In contrast to the formal descriptions above, this section presents an intuitive perspective on adjoint functors: namely, a (left) adjoint, when it exists, provides the most efficient possible solutions to the problem posed by its (right) adjoint. This perspective is particularly helpful when the right adjoint in question is easily conceptualised as a forgetful functor. For a concrete example, we could consider the (fully faithful) inclusion of abelian groups into all groups.

The first thing to notice is that $U : Ab \to Grp$ induces a notion of morphism from groups $G$ to abelian groups $H :$ this is the hom-set $Hom_{Grp} (G, U (H)) .$ This observation isn’t particularly deep in this case, since the maps between abelian groups are also group homomorphisms, but note that this works for any functor: the forgetful functor $U : Grp \to Sets$ lets us consider maps “from a group to a set”.

By letting the abelian group $H$ vary, we can consider morphisms from a group $G$ to some abelian group. These form a category in their own right, the comma category $G ↙ U .$ In a sense, these are all solutions to the problem of turning $G$ into an abelian group — or, more precisely, mapping $G$ into an abelian group. For a given $G,$ there can be arbitrarily many of these, and some are extremely boring: for example, the zero group is abelian, so we can always consider $G \to \emptyset$ as a way to “turn $G$ into an abelian group”!

So we’re left with defining which of these solutions is the most efficient. Since turning a group abelian necessarily involves identifying elements that were previously distinct — all the $g h \neq = h g$ have to be squashed — we could attempt to measure how many elements got identified, and choose the one that imposes the least amount of these relations. While this might be tractable for finitely presented groups, it would be really hard to define, let alone measure, these imposed relations for an arbitrary $U : D \to C!$

However, we don’t need any actual count of the relations imposed, or even a notion of relation. The important thing to observe is that, if $(H, η)$ and $(H^{'}, η^{'})$ are both ways of turning $G$ into an abelian group, then we can factor $η^{'}$ as a map

G η H f H^{'}

if and only if $η$ imposes less relations on the elements of $G$ than $η^{'}$ does. The most efficient solution to turning $G$ into an abelian group, then, would be the one through which all others factor, since it will impose the least number of relations! Abstractly, we are looking for an initial object in the comma category $G ↙ U .$

While the abstract phrasing we’ve arrived at is very elegant, it does seriously obfuscate the data necessary. To work with left adjoints smoothly, and to present the ideas more clearly, we introduce an auxiliary notion: free objects.

module _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} (U : Functor C D) where
  private
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D
    module U = Func U

A free object on $X : C,$ relative to $U : D \to C,$ consists of an object $F (X) : D$ and an arrow $η : X \to U F (X),$ such that every $f : X \to U Y,$ $f$ factors uniquely through $η .$ Expanding this to an *operations-and”properties” presentation, we could say that:

There is a map fold from $D (X, U Y)$ to $C (FX, Y),$ and
for every $f,$ we have $U (fold f) η = f,$ and
for every $f$ and $g,$ if $U (g) η = f,$ then $g = fold f .$

  record Free-object (X : D.Ob) : Type (adj-level C D) where
    field
      {free} : C.Ob
      unit   : D.Hom X (U.₀ free)

      fold    : ∀ {Y} (f : D.Hom X (U.₀ Y)) → C.Hom free Y
      commute : ∀ {Y} {f : D.Hom X (U.₀ Y)} → U.₁ (fold f) D.∘ unit ≡ f
      unique
        : ∀ {Y} {f : D.Hom X (U.₀ Y)} (g : C.Hom free Y)
        → U.₁ g D.∘ unit ≡ f
        → g ≡ fold f

    abstract
      fold-natural
        : ∀ {Y Y'} (f : C.Hom Y Y') (g : D.Hom X (U.₀ Y))
        → fold (U.₁ f D.∘ g) ≡ f C.∘ fold g
      fold-natural f g = sym (unique (f C.∘ fold g) (U.popr commute))

      fold-unit : fold unit ≡ C.id
      fold-unit = sym (unique C.id (D.eliml U.F-id))

      unique₂
        : ∀ {B} {f : D.Hom X (U.₀ B)} (g₁ g₂ : C.Hom free B)
        → U.₁ g₁ D.∘ unit ≡ f
        → U.₁ g₂ D.∘ unit ≡ f
        → g₁ ≡ g₂
      unique₂ g₁ g₂ p q = unique g₁ p ∙ sym (unique g₂ q)

Note that factors uniquely through $η$ is precisely equivalent to saying that $η$ induces an equivalence between $D (X, U Y)$ and $C (FX, Y) .$ In other words, free objects are representing objects for the functor $D (X, U (-)) .$

    fold-is-equiv : ∀ B → is-equiv (fold {B})
    fold-is-equiv B = is-iso→is-equiv λ where
      .is-iso.inv  f → U.₁ f D.∘ unit
      .is-iso.rinv _ → sym (unique _ refl)
      .is-iso.linv _ → commute

module _ {U : Functor C D} where
  private
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D
    module U = Func U

  open Free-object

This implies that free objects have all the usual properties of universal constructions: they are unique up to unique isomorphism, and identity of free objects is determined by identity of the unit maps — put another way, being a free object is truly a property of the pair $(FX, η) .$

  free-object-unique : ∀ {X} (A B : Free-object U X) → A .free C.≅ B .free

  Free-object-path
    : ∀ {X} {x y : Free-object U X}
    → (p : x .free ≡ y .free)
    → (q : PathP (λ i → D.Hom X (U.₀ (p i))) (x .unit) (y .unit))
    → x ≡ y

The proofs follow the usual script for universal constructions, so we will omit the details.

  free-object-unique a b =
    C.make-iso (a .fold (b .unit)) (b .fold (a .unit))
      (unique₂ b _ _ (U.popr (b .commute) ∙ a .commute) (D.eliml U.F-id))
      (unique₂ a _ _ (U.popr (a .commute) ∙ b .commute) (D.eliml U.F-id))

  Free-object-path {X = X} {x} {y} p q = r where
    folds : ∀ {Y} (f : D.Hom X (U.₀ Y)) → PathP (λ i → C.Hom (p i) Y) (x .fold f) (y .fold f)
    folds {Y} f = to-pathp $
      let
        it : U.₁ (x .fold f) D.∘ x .unit
           ≡ U.₁ (transport (λ i → C.Hom (p i) Y) (x .fold f)) D.∘ y .unit
        it i = U.₁ (coe0→i (λ i → C.Hom (p i) Y) i (x .fold f)) D.∘ q i
      in y .unique _ (sym it ∙ x .commute)

    r : x ≡ y
    r i .free = p i
    r i .unit = q i
    r i .fold f = folds f i
    r i .commute {f = f} = is-prop→pathp
      (λ i → D.Hom-set _ _ (U.₁ (folds f i) D.∘ q i) f) (x .commute) (y .commute) i
    r i .unique {Y = Y} {f} = is-prop→pathp
      (λ i → Π-is-hlevel² {A = C.Hom (p i) Y} {B = λ g → U.₁ g D.∘ q i ≡ f} 1 λ g _ → C.Hom-set _ _ g (folds f i))
      (x .unique) (y .unique) i

  instance
    -- This lets us ignore 'is-free-object' when proving equality.
    Extensional-Free-object
      : ∀ {X ℓr}
      → ⦃ sa : Extensional (Σ[ A ∈ C.Ob ] (D.Hom X (U.₀ A))) ℓr ⦄
      → Extensional (Free-object U X) ℓr
    Extensional-Free-object ⦃ sa = sa ⦄ .Pathᵉ x y = sa .Pathᵉ (_ , x .unit) (_ , y .unit)
    Extensional-Free-object ⦃ sa = sa ⦄ .reflᵉ x = sa .reflᵉ (_ , x .unit)
    Extensional-Free-object ⦃ sa = sa ⦄ .idsᵉ .to-path h =
      let p = sa .idsᵉ .to-path h
       in Free-object-path (ap fst p) (ap snd p)
    Extensional-Free-object ⦃ sa = sa ⦄ .idsᵉ .to-path-over p =
      sa .idsᵉ .to-path-over p


  private module I = Initial
  open ↓Hom

Finally, we sketch one direction of the equivalence between our new definition of free object for $X$ relative to $U$ and the more abstract construction of initial object in the comma category $X ↙ U$ which we had arrived at earlier. This is simply a re-labelling of data: it would not be hard to complete this to a full equivalence, but it would not be very useful, either.

  free-object→universal-map
    : ∀ {X} → Free-object U X → Initial (X ↙ U)
  free-object→universal-map fo = λ where
    .I.bot → ↓obj (fo .unit)
    .I.has⊥ x .centre  → ↓hom (D.idr _ ∙ sym (fo .commute))
    .I.has⊥ x .paths p → ↓Hom-path _ _ refl $ sym $
      fo .unique _ (sym (p .sq) ∙ D.idr _)

Free objects and adjoints🔗

If $U$ has a left adjoint $F,$ then every $X : D$ has a corresponding free object: $(FX, η),$ where $η$ is the unit of the adjunction. This justifies our use of the notation $FX$ for a free object on $X,$ even if a functor $F (-)$ does not necessarily exist.

  module _ {F : Functor D C} (F⊣U : F ⊣ U) where
    open _⊣_ F⊣U

    left-adjoint→free-objects : ∀ X → Free-object U X
    left-adjoint→free-objects X .free    = F .F₀ X
    left-adjoint→free-objects X .unit    = unit.η X
    left-adjoint→free-objects X .fold f  = R-adjunct F⊣U f
    left-adjoint→free-objects X .commute = L-R-adjunct F⊣U _
    left-adjoint→free-objects X .unique g p =
      Equiv.injective (_ , L-adjunct-is-equiv F⊣U) (p ∙ sym (L-R-adjunct F⊣U _))

Conversely, if $D$ has all free objects, then $U$ has a left adjoint. We begin by constructing a functor $F : D \to C$ that assigns each object to its free counterpart; functoriality follows from the universal property.

  module _ (free-objects : ∀ X → Free-object U X) where
    private module F {X} where open Free-object (free-objects X) public
    open Functor
    open _=>_
    open _⊣_

    free-objects→functor : Functor D C
    free-objects→functor .F₀ X = F.free {X}
    free-objects→functor .F₁ f = F.fold (F.unit D.∘ f)
    free-objects→functor .F-id =
      F.fold (F.unit D.∘ D.id)  ≡⟨ ap F.fold (D.idr _) ⟩≡
      F.fold F.unit             ≡⟨ F.fold-unit ⟩≡
      C.id                      ∎
    free-objects→functor .F-∘ f g =
      F.fold (F.unit D.∘ f D.∘ g)                              ≡⟨ ap F.fold (D.extendl (sym F.commute)) ⟩≡
      F.fold (U.₁ (F.fold (F.unit D.∘ f)) D.∘ (F.unit D.∘ g))  ≡⟨ F.fold-natural _ _ ⟩≡
      F.fold (F.unit D.∘ f) C.∘ F.fold (F.unit D.∘ g)          ∎

The unit of the adjunction is given by $η,$ the counit by $ε id,and$ Both naturality and the zig-zag identities follow from some short arguments about adjuncts.

    free-objects→left-adjoint : free-objects→functor ⊣ U
    free-objects→left-adjoint .unit .η X = F.unit {X}
    free-objects→left-adjoint .unit .is-natural X Y f = sym F.commute
    free-objects→left-adjoint .counit .η X = F.fold D.id
    free-objects→left-adjoint .counit .is-natural X Y f =
      F.fold D.id C.∘ F.fold (F.unit D.∘ U.₁ f)        ≡˘⟨ F.fold-natural _ _ ⟩≡˘
      F.fold (U.₁ (F.fold D.id) D.∘ F.unit D.∘ U.₁ f)  ≡⟨ ap F.fold (D.cancell F.commute ∙ sym (D.idr _)) ⟩≡
      F.fold (U.₁ f D.∘ D.id)                          ≡⟨ F.fold-natural _ _ ⟩≡
      f C.∘ F.fold D.id                                ∎
    free-objects→left-adjoint .zig =
      F.fold D.id C.∘ F.fold (F.unit D.∘ F.unit)        ≡˘⟨ F.fold-natural _ _ ⟩≡˘
      F.fold (U.₁ (F.fold D.id) D.∘ F.unit D.∘ F.unit)  ≡⟨ ap F.fold (D.cancell F.commute) ⟩≡
      F.fold F.unit                                     ≡⟨ F.fold-unit ⟩≡
      C.id                                              ∎
    free-objects→left-adjoint .zag = F.commute

If we round-trip a left adjoint through these two constructions, then we obtain the same functor we started with. Moreover, we also obtain the same unit/counit!

  left-adjoint→free-objects→left-adjoint
    : ∀ {F : Functor D C}
    → (F⊣U : F ⊣ U)
    → free-objects→functor (left-adjoint→free-objects F⊣U) ≡ F
  left-adjoint→free-objects→left-adjoint {F = F} F⊣U =
    Functor-path (λ _ → refl) λ f →
      ap (R-adjunct F⊣U) (unit.is-natural _ _ f)
      ∙ R-L-adjunct F⊣U (F.₁ f)
    where
      module F = Functor F
      open _⊣_ F⊣U

  adjoint-pair→free-objects→adjoint-pair
    : ∀ {F : Functor D C}
    → (F⊣U : F ⊣ U)
    → PathP (λ i → left-adjoint→free-objects→left-adjoint F⊣U i ⊣ U)
      (free-objects→left-adjoint (left-adjoint→free-objects F⊣U))
      F⊣U
  adjoint-pair→free-objects→adjoint-pair {F = F} F⊣U =
    adjoint-pathp _ _
      (Nat-pathp _ _ λ _ → refl)
      (Nat-pathp _ _ λ x → C.elimr F.F-id)
    where module F = Functor F

A similar result holds for a system of free objects.

  free-objects→left-adjoint→free-objects
    : ∀ (free-objects : ∀ x → Free-object U x)
    → left-adjoint→free-objects (free-objects→left-adjoint free-objects) ≡ free-objects
  free-objects→left-adjoint→free-objects free-objects = trivial!

This yields an equivalence between systems of free objects and left adjoints.

  free-objects≃left-adjoint
    : (∀ X → Free-object U X) ≃ (Σ[ F ∈ Functor D C ] F ⊣ U)

Constructing the equivalence is straightforward, as we already have all the pieces laying about!

  free-objects≃left-adjoint = Iso→Equiv $
    (λ free-objects →
      free-objects→functor free-objects ,
      free-objects→left-adjoint free-objects) ,
    iso (λ left-adj → left-adjoint→free-objects (left-adj .snd))
      (λ left-adj →
        left-adjoint→free-objects→left-adjoint (left-adj .snd) ,ₚ
        adjoint-pair→free-objects→adjoint-pair (left-adj .snd))
      free-objects→left-adjoint→free-objects

Free objects and initiality🔗

In categorical semantics, syntax for a theory $T$ is often presented in two seemingly unconnected ways:

Via a left adjoint to the forgetful functor that forgets the structure of a $T -model;$ or
As an initial object in the category of $T -models.$

Left adjoints encode the universal property “syntax with generators”: structure-preserving maps $C (F (X), A)$ out of the syntax generated by $X$ are given by non-structure $D (X, U (A))$ on the generators. Conversely, initial objects give us the universal property of “syntax without generators”: there is a unique structure-preserving map out of the syntax into each model.

We can somewhat reconcile these views by recalling that left adjoints preserve colimits. The initial object is a colimit, so the initial object in the category $T -models$ is $F (⊥) .$ In other words: “syntax without generators” and “syntax on 0 generators” coincide. This correspondence remains intact even when we lack a full left adjoint.

For the remainder of this section, assume that $D$ has an initial object $⊥_{D} .$ If there is a free object $A : C$ on $⊥_{D},$ then $A$ is an initial object in $C .$

  module _ (initial : Initial D) where
    open Initial initial

    free-on-initial→initial
      : (F[⊥] : Free-object U bot)
      → is-initial C (F[⊥] .free)
    free-on-initial→initial F[⊥] x .centre = F[⊥] .fold ¡
    free-on-initial→initial F[⊥] x .paths f =
      sym $ F[⊥] .unique f (sym (¡-unique _))

Conversely, if $C$ has an initial object $⊥_{C},$ then $⊥_{C}$ is a free object for $⊥_{C} .$

    is-initial→free-on-initial
      : (c-initial : Initial C)
      → Free-object U bot
    is-initial→free-on-initial c-init = record
      { free    = Initial.bot c-init
      ; unit    = ¡
      ; fold    = λ _ → Initial.¡ c-init
      ; commute = ¡-unique₂ _ _
      ; unique  = λ _ _ → Initial.¡-unique₂ c-init _ _
      }

Note an initial object in $C$ does not guarantee an initial object in $D,$ regardless of how many free objects there are. Put syntactically, a notion of “syntax without generators” does not imply that there is an object of 0 generators!

Induced adjunctions🔗

Any adjunction $L ⊣ R$ induces, in a very boring way, an opposite adjunction $R^{op} ⊣ L^{op}$ between opposite functors:

module _ {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) where
  private
    module L = Functor L
    module R = Functor R
    module adj = _⊣_ adj

  open _⊣_
  open _=>_

  opposite-adjunction : R.op ⊣ L.op
  opposite-adjunction .unit .η _ = adj.ε _
  opposite-adjunction .unit .is-natural x y f = sym (adj.counit.is-natural _ _ _)
  opposite-adjunction .counit .η _ = adj.η _
  opposite-adjunction .counit .is-natural x y f = sym (adj.unit.is-natural _ _ _)
  opposite-adjunction .zig = adj.zag
  opposite-adjunction .zag = adj.zig

As well as adjunctions $L \circ - ⊣ R \circ -$ and $- \circ R ⊣ - \circ L$ between postcomposition and precomposition functors, respectively:

  open import Cat.Functor.Coherence

  postcomposite-adjunction : postcompose L {D = E} ⊣ postcompose R
  postcomposite-adjunction .unit .η F = cohere! (adj.unit ◂ F)
  postcomposite-adjunction .unit .is-natural F G α = ext λ _ → adj.unit.is-natural _ _ _
  postcomposite-adjunction .counit .η F = cohere! (adj.counit ◂ F)
  postcomposite-adjunction .counit .is-natural F G α = ext λ _ → adj.counit.is-natural _ _ _
  postcomposite-adjunction .zig = ext λ _ → adj.zig
  postcomposite-adjunction .zag = ext λ _ → adj.zag

  precomposite-adjunction : precompose R {D = E} ⊣ precompose L
  precomposite-adjunction .unit .η F = cohere! (F ▸ adj.unit)
  precomposite-adjunction .unit .is-natural F G α = ext λ _ → sym (α .is-natural _ _ _)
  precomposite-adjunction .counit .η F = cohere! (F ▸ adj.counit)
  precomposite-adjunction .counit .is-natural F G α = ext λ _ → sym (α .is-natural _ _ _)
  precomposite-adjunction .zig {F} = ext λ _ → Func.annihilate F adj.zag
  precomposite-adjunction .zag {F} = ext λ _ → Func.annihilate F adj.zig

adjoint-natural-iso
  : ∀ {L L' : Functor C D} {R R' : Functor D C}
  → L ≅ⁿ L' → R ≅ⁿ R' → L ⊣ R → L' ⊣ R'
adjoint-natural-iso {C = C} {D = D} {L} {L'} {R} {R'} α β L⊣R = L'⊣R' where
  open _⊣_ L⊣R
  module α = Isoⁿ α
  module β = Isoⁿ β
  open _=>_ using (is-natural)
  module C = Cat.Reasoning C
  module D = Cat.Reasoning D
  module L = Func L
  module L' = Func L'
  module R = Func R
  module R' = Func R'

  -- Abbreviations for equational reasoning
  α→ : ∀ {x} → D.Hom (L.₀ x) (L'.₀ x)
  α→ {x} = α.to ._=>_.η x

  α← : ∀ {x} → D.Hom (L'.₀ x) (L.₀ x)
  α← {x} = α.from ._=>_.η x

  β→ : ∀ {x} → C.Hom (R.₀ x) (R'.₀ x)
  β→ {x} = β.to ._=>_.η x

  β← : ∀ {x} → C.Hom (R'.₀ x) (R.₀ x)
  β← {x} = β.from ._=>_.η x

  L'⊣R' : L' ⊣ R'
  L'⊣R' ._⊣_.unit =  (β.to ◆ α.to) ∘nt unit
  L'⊣R' ._⊣_.counit = counit ∘nt (α.from ◆ β.from)
  L'⊣R' ._⊣_.zig =
    (ε _ D.∘ (L.₁ β← D.∘ α←)) D.∘ L'.₁ (⌜ R'.₁ α→ C.∘ β→ ⌝ C.∘ η _) ≡⟨ ap! (sym $ β.to .is-natural _ _ _) ⟩≡
    (ε _ D.∘ ⌜ L.₁ β← D.∘ α← ⌝) D.∘ L'.₁ ((β→ C.∘ R.₁ α→) C.∘ η _)  ≡⟨ ap! (sym $ α.from .is-natural _ _ _) ⟩≡
    (ε _ D.∘ α← D.∘ L'.₁ β←) D.∘ L'.₁ ((β→ C.∘ R.₁ α→) C.∘ η _)     ≡⟨ D.pullr (D.pullr (L'.collapse (C.pulll (C.cancell (β.invr ηₚ _))))) ⟩≡
    ε _ D.∘ α← D.∘ L'.₁ (R.₁ α→ C.∘ η _)                            ≡⟨ ap (ε _ D.∘_) (α.from .is-natural _ _ _) ⟩≡
    ε _ D.∘ L.₁ (R.₁ α→ C.∘ η _) D.∘ α←                             ≡⟨ D.push-inner (L.F-∘ _ _) ⟩≡
    (ε _ D.∘ L.₁ (R.₁ α→)) D.∘ (L.₁ (η _) D.∘ α←)                   ≡⟨ D.pushl (counit.is-natural _ _ _) ⟩≡
    α→ D.∘ ε _ D.∘ L.₁ (η _) D.∘ α←                                 ≡⟨ ap (α→ D.∘_) (D.cancell zig) ⟩≡
    α→ D.∘ α←                                                       ≡⟨ α.invl ηₚ _ ⟩≡
    D.id ∎
  L'⊣R' ._⊣_.zag =
    R'.₁ (ε _ D.∘ L.₁ β← D.∘ α←) C.∘ ((R'.₁ α→ C.∘ β→) C.∘ η _) ≡⟨ C.extendl (C.pulll (R'.collapse (D.pullr (D.cancelr (α.invr ηₚ _))))) ⟩≡
    R'.₁ (ε _ D.∘ L.₁ β←) C.∘ β→ C.∘ η _                        ≡⟨ C.extendl (sym (β.to .is-natural _ _ _)) ⟩≡
    β→ C.∘ R.₁ (ε _ D.∘ L.₁ β←) C.∘ η _                         ≡⟨ C.push-inner (R.F-∘ _ _) ⟩≡
    ((β→ C.∘ R.₁ (ε _)) C.∘ (R.₁ (L.₁ β←) C.∘ η _))             ≡⟨ ap₂ C._∘_ refl (sym $ unit.is-natural _ _ _) ⟩≡
    (β→ C.∘ R.₁ (ε _)) C.∘ (η _ C.∘ β←)                         ≡⟨ C.cancel-inner zag ⟩≡
    β→ C.∘ β←                                                   ≡⟨ β.invl ηₚ _ ⟩≡
    C.id ∎

adjoint-natural-isol
  : ∀ {L L' : Functor C D} {R : Functor D C}
  → L ≅ⁿ L' → L ⊣ R → L' ⊣ R
adjoint-natural-isol α = adjoint-natural-iso α idni

adjoint-natural-isor
  : ∀ {L : Functor C D} {R R' : Functor D C}
  → R ≅ⁿ R' → L ⊣ R → L ⊣ R'
adjoint-natural-isor β = adjoint-natural-iso idni β

module _ {o h o' h'} {C : Precategory o h} {D : Precategory o' h'} where
  private module C = Precategory C

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

  open Free-object
  open Initial
  open ↓Obj
  open ↓Hom

  universal-map→free-object : ∀ {R X} → Universal-morphism R X → Free-object R X
  universal-map→free-object x .free = _
  universal-map→free-object x .unit = x .bot .map
  universal-map→free-object x .fold f = x .has⊥ (↓obj f) .centre .β
  universal-map→free-object x .commute = sym (x .has⊥ _ .centre .sq) ∙ C.idr _
  universal-map→free-object x .unique g p = ap β (sym (x .has⊥ _ .paths (↓hom (sym (p ∙ sym (C.idr _))))))

  universal-maps→functor : ∀ {R} → (∀ X → Universal-morphism R X) → Functor C D
  universal-maps→functor u = free-objects→functor (λ X → universal-map→free-object (u X))

  universal-maps→left-adjoint
    : ∀ {R} (h : ∀ X → Universal-morphism R X)
    → universal-maps→functor h ⊣ R
  universal-maps→left-adjoint h = free-objects→left-adjoint _

  left-adjoint→universal-maps : ∀ {L R} → L ⊣ R → ∀ X → Universal-morphism R X
  left-adjoint→universal-maps L⊣R X =
    free-object→universal-map (left-adjoint→free-objects L⊣R X)