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₂


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 Structures at the level of groupoids (e.g. the collection of all sets) are interestingly related by sets (i.e. the set of maps 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 and is given by a pair of functors equipped with natural isomorphisms (the “unit”) and (the “counit”). We still want the correspondence to be bidirectional, so we can’t change the types of 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 and eliminate in a composition, which gives us two ways of mapping One is the identity, and the other is going through the unit: (the situation with 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:

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

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

: 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)
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)


Another view on adjunctions, one which is productive when thinking about adjoint endofunctors is the concept of adjuncts. Any pair of natural transformations typed like a unit and counit allow you to pass between the Hom-sets and by composing the functorial action of (resp 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

  L-adjunct : ∀ {a b} → D.Hom (L.₀ a) b → C.Hom a (R.₀ b)

R-adjunct : ∀ {a b} → C.Hom a (R.₀ b) → D.Hom (L.₀ a) b


The important part that the actual data of an adjunction gets you is these functions are inverse equivalences between the hom-sets

  L-R-adjunct : ∀ {a b} → is-right-inverse (R-adjunct {a} {b}) L-adjunct
R.₁ (adj.ε _ D.∘ L.₁ f) C.∘ adj.η _        ≡⟨ R.pushl refl ⟩≡
R.₁ (adj.ε _) C.∘ R.₁ (L.₁ f) C.∘ adj.η _  ≡˘⟨ C.refl⟩∘⟨ adj.unit.is-natural _ _ _ ⟩≡˘
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                                         ∎

adjunct-hom-equiv : ∀ {a b} → D.Hom (L.₀ a) b ≃ C.Hom a (R.₀ b)

  module L-adjunct {a b} = Equiv (L-adjunct {a} {b} , L-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)
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 induces a notion of morphism from groups to abelian groups this is the hom-set 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 lets us consider maps “from a set to a group”. By letting the abelian group vary, we can consider morphisms from a group to some abelian group. These form a category in their own right, the comma category In a sense, these are all solutions to the problem of turning into an abelian group — or, more precisely, mapping into an abelian group. For a given there can be arbitrarily many of these, and some are extremely boring: for example, the zero group is abelian, so we can always consider as a way to “turn 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 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 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 and are both ways of turning into an abelian group, then we can factor as a map if and only if imposes less relations on the elements of than does. The most efficient solution to turning 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 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 relative to consists of an object and an arrow such that every factors uniquely through Expanding this to an *operations-and”properties” presentation, we could say that: • There is a map fold from to and • for every we have and • for every and if then  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 and In other words, free objects are representing objects for the functor  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  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 relative to and the more abstract construction of initial object in the comma category 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 _)


If has a left adjoint then every has a corresponding free object: where is the unit of the adjunction. This justifies our use of the notation for a free object on even if a functor 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 .unique g p =


Conversely, if has all free objects, then has a left adjoint. We begin by constructing a functor 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 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                                ∎
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                                              ∎


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
Functor-path (λ _ → refl) λ f →
ap (R-adjunct F⊣U) (unit.is-natural _ _ f)
where
module F = Functor F
open _⊣_ F⊣U

: ∀ {F : Functor D C}
→ (F⊣U : F ⊣ U)
F⊣U
(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)


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 is often presented in two seemingly unconnected ways: 1. Via a left adjoint to the forgetful functor that forgets the structure of a or 2. As an initial object in the category of Left adjoints encode the universal property “syntax with generators”: structure-preserving maps out of the syntax generated by are given by non-structure 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 is 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 has an initial object If there is a free object on then is an initial object in  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 has an initial object then is a free object for

    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 does not guarantee an initial object in 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!

Any adjunction induces, in a very boring way, an opposite adjunction 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

open _⊣_
open _=>_

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


As well as adjunctions and between postcomposition and precomposition functors, respectively:

  open import Cat.Functor.Coherence

postcomposite-adjunction : postcompose L {D = E} ⊣ postcompose R
postcomposite-adjunction .unit .is-natural F G α = ext λ _ → adj.unit.is-natural _ _ _
postcomposite-adjunction .counit .is-natural F G α = ext λ _ → adj.counit.is-natural _ _ _

precomposite-adjunction : precompose R {D = E} ⊣ precompose L
precomposite-adjunction .unit .is-natural F G α = ext λ _ → sym (α .is-natural _ _ _)
precomposite-adjunction .counit .is-natural F G α = ext λ _ → sym (α .is-natural _ _ _)

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 ∎

: ∀ {L L' : Functor C D} {R : Functor D C}
→ L ≅ⁿ L' → L ⊣ R → L' ⊣ R

: ∀ {L : Functor C D} {R R' : Functor D C}
→ R ≅ⁿ R' → L ⊣ R → L ⊣ R'

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))