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≤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→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∘L)$
(the “unit”) and
$ε:(L∘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∘L$
and eliminate
$L∘R$
in a composition, which gives us two ways of mapping
$L⇒L.$
One is the identity, and the other is going through the unit:
$L⇒L∘R∘L⇒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 *endo*functors
$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(La,b)$
and
$Hom(a,Rb),$
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(La,b)≅Hom(a,Rb).$

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) adjunct-hom-equiv : ∀ {a b} → D.Hom (L.₀ a) b ≃ C.Hom a (R.₀ b) adjunct-hom-equiv = L-adjunct , L-adjunct-is-equiv

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→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→Sets$
lets us consider maps “from a set to a group”.

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→∅$
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
$gh=hg$
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→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

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→C,$
consists of an object
$F(X):D$
and an arrow
$η:X→UF(X),$
such that every
$f:X→UY,$
$f$
factors uniquely through
$η.$
Expanding this to an *operations-and”properties” presentation, we could
say that:

- There is a map
`fold`

from $D(X,UY)$ to $C(FX,Y),$ and - for every $f,$ we have $U(foldf)η=f,$ and
- for every $f$ and $g,$ if $U(g)η=f,$ then $g=foldf.$

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,UY)$
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.

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→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∘−⊣R∘−$ and $−∘R⊣−∘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)