open import Cat.Diagram.Colimit.Representable
open import Cat.Functor.Hom.Representable
open import Cat.Functor.Kan.Representable
open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Base
open import Cat.Functor.Kan.Unique
open import Cat.Functor.Naturality
open import Cat.Functor.Properties
open import Cat.Functor.Coherence
open import Cat.Functor.Constant
open import Cat.Functor.Kan.Base
open import Cat.Functor.Compose
open import Cat.Instances.Comma
open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Prelude

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

module Cat.Functor.Kan.Pointwise where

Pointwise Kan extensions🔗

One useful perspective on Kan extensions is that they are generalizations of (co)limits; in fact, we have defined (co)limits as a special case of Kan extensions! This means that many theorems involving (co)limits can be directly generalized to theorems of Kan extensions. A concrete example of this phenomena is the fact that right adjoints don’t just preserve limits, they preserve all right extensions!

However, this pattern of generalization fails in one critical way: corepresentable functors preserve limits, but corepresentable functors do not necessarily preserve Kan extensions! This seemingly slight issue has far-reaching consequences, to the point that some authors write off general Kan extensions entirely.

Instead of throwing the whole thing out, an alternative is to focus on only the Kan extensions that are preserved by arbitrary (co)representables; we call such extensions pointwise.

module _
  {o o' o'' ℓ ℓ' ℓ''}
  {C : Precategory o ℓ} {C' : Precategory o' ℓ'} {D : Precategory o'' ℓ''}
  {F : Functor C C'} {G : Functor C D} {E : Functor C' D}
  where

  private
    module C = Cat.Reasoning C
    module C' = Cat.Reasoning C'
    module D = Cat.Reasoning D
    module [C,D] = Cat.Reasoning (Cat[ C , D ])
    module [C',D] = Cat.Reasoning (Cat[ C' , D ])
    open Func
    open is-lan
    open _=>_

  is-pointwise-lan : ∀ {eta : G => E F∘ F} → is-lan F G E eta → Type _
  is-pointwise-lan lan =
    ∀ (x : D.Ob) → preserves-lan (Functor.op (Hom-into D x)) lan

  is-pointwise-ran : ∀ {eps : E F∘ F => G} → is-ran F G E eps → Type _
  is-pointwise-ran ran =
    ∀ (x : D.Ob) → preserves-ran (Hom-from D x) ran

Absolute Kan extensions are trivially pointwise, since they are preserved by all functors.

  absolute-lan→pointwise
    : {eta : G => E F∘ F}
    → {lan : is-lan F G E eta}
    → is-absolute-lan lan
    → is-pointwise-lan lan
  absolute-lan→pointwise abs _ = abs _

  absolute-ran→pointwise
    : {eps : E F∘ F => G}
    → {ran : is-ran F G E eps}
    → is-absolute-ran ran
    → is-pointwise-ran ran
  absolute-ran→pointwise abs _ = abs _

module _
  {o o' ℓ ℓ'}
  {J : Precategory o' ℓ'} {C : Precategory o ℓ}
  {Dia : Functor J C} {x : ⌞ C ⌟}
  where

  private
    module C = Cat.Reasoning C
    open Func
    open is-lan
    open _=>_

As noted earlier, limits and colimits are pointwise Kan extensions.

  limit→pointwise
    : {eps : Const x => Dia}
    → (lim : is-limit Dia x eps)
    → is-pointwise-ran lim
  limit→pointwise lim x = Hom-from-preserves-limits x lim

  colimit→pointwise
    : {eta : Dia => Const x}
    → (colim : is-colimit Dia x eta)
    → is-pointwise-lan colim
  colimit→pointwise colim x = よ-reverses-colimits x colim

Computing pointwise extensions🔗

One useful fact about pointwise left Kan extensions (resp. right) is that they can be computed via colimits (resp. limits). We will focus on the left extensions for the moment. Given functors $F:\mathcal{C}\to {\mathcal{C}}^{\prime }$ and $G:\mathcal{C}\to \mathcal{D}\text{,}$ if $\mathcal{C}$ is a $\kappa \text{-small}$ category, ${\mathcal{C}}^{\prime }$ is locally $\kappa \text{-small,}$ and $\mathcal{D}$ has $\kappa \text{-small}$ colimits, then ${\mathrm{Lan}}_F(G)$ exists and is pointwise.

module _
  {o o' ℓ ℓ'}
  {C : Precategory ℓ ℓ} {C' : Precategory o ℓ} {D : Precategory o' ℓ'}
  (F : Functor C C') (G : Functor C D)
  where

  private
    module C = Cat.Reasoning C
    module C' = Cat.Reasoning C'
    module D = Cat.Reasoning D
    open Func
    open ↓Obj
    open ↓Hom
    open _=>_
    open is-lan

The big idea of our construction is to approximate $G$ by gluing together “all the ways that $C$ is able to see $C^{\prime }$ through $G$”. Concretely, this means looking at the comma category $F\swarrow c^{\prime }$ for a given $c^{\prime }:{\mathcal{C}}^{\prime }\text{.}$ Objects in this category are pairs of an object $c:\mathcal{C}$ and morphisms ${\mathcal{C}}^{\prime }(F(c),c^{\prime })\text{.}$ If we apply the “domain” projection $F\swarrow c^{\prime }\to \mathcal{C}\text{,}$ we obtain a diagram in $\mathcal{C}$ encoding the hand-wavy intuition from before.

To finish the construction, we take our diagram in $\mathcal{C}$ and post-compose with $G$ to obtain a diagram

Since $F\swarrow c^{\prime }$ is put together out of objects in $\mathcal{C}$ and morphisms in ${\mathcal{C}}^{\prime }\text{,}$ it is also a $\kappa \text{-small}$ category, so these diagrams all have colimits in $\mathcal{D}\text{.}$

    ↓Dia : (c' : C'.Ob) → Functor (F ↘ c') D
    ↓Dia c' = G F∘ Dom F (!Const c')

In fact, we can weaken the precondition from cocompleteness of $\mathcal{D}$ to having colimits of these comma-category-shaped diagrams.

  comma-colimits→lan
    : (∀ (c' : C'.Ob) → Colimit (↓Dia c'))
    → Lan F G
  comma-colimits→lan ↓colim = lan module comma-colimits→lan where
      module ↓colim c' = Colimit (↓colim c')

Taking the colimit at each $c^{\prime }:{\mathcal{C}}^{\prime }$ gives an assignment of objects $F^{\prime }(c^{\prime }):\mathcal{D}\text{,}$ so we’re left with extending it to a proper functor ${\mathcal{C}}^{\prime }\to \mathcal{D}\text{.}$ Coming up with morphisms in the image of $F^{\prime }$ isn’t too complicated, and universality of colimits guarantees the functoriality constraints are satisfied.

      F' : Functor C' D
      F' .F₀ c' = ↓colim.coapex c'
      F' .F₁ f = ↓colim.universal _
        (λ j → ↓colim.ψ _ (↓obj (f C'.∘ j .map)))
        (λ f → ↓colim.commutes _ (↓hom {β = f .β} (C'.pullr (f .sq)
            ·· C'.elim-inner refl
            ·· sym (C'.idl _))))

      F' .F-id =
        sym $ ↓colim.unique _ _ _ _ λ j →
          D.idl _
          ∙ ap (↓colim.ψ _) (↓Obj-path _ _ refl refl (sym (C'.idl _)))
      F' .F-∘ f g =
        sym $ ↓colim.unique _ _ _ _ λ j →
          D.pullr (↓colim.factors _ _ _)
          ∙ ↓colim.factors _ _ _
          ∙ ap (↓colim.ψ _) (↓Obj-path _ _ refl refl (C'.assoc _ _ _))

Next, we need to show that the functor we constructed actually is a left extension. The first step will be to construct a “unit” natural transformation $\eta :G\to F^{\prime }F\text{,}$ which, in components, means we’re looking for maps $G(x)\to F^{\prime }(F(x))\text{.}$ Since each $F^{\prime }(-)$ is a colimit, we can use the coprojections!

      eta : G => F' F∘ F
      eta .η c = ↓colim.ψ (F .F₀ c) (↓obj C'.id)

This “type checks” because the colimit coprojections for our $F\swarrow c^{\prime }\text{-colimits,}$ essentially, convert maps $C^{\prime }(F(X),Y)$ into maps $G(X)\to F^{\prime }(Y)\text{.}$ If we take the identity $C^{\prime }(F(c),F(c))\text{,}$ we get what we wanted: a map $G(c)\to F^{\prime }(F(c))\text{.}$

      eta .is-natural x y f =
        ↓colim.commutes (F .F₀ y) (↓hom (ap (C'.id C'.∘_) (sym (C'.idr _))))
        ∙ sym (↓colim.factors _ _ _)

For the other obligation, suppose we’re given some $M:{\mathcal{C}}^{\prime }\to \mathcal{D}$ and natural transformation $\alpha :G\to MF\text{.}$ How do we extend it to a transformation $F^{\prime }\to M\text{?}$ By “matching” on the colimit, with a slight adjustment to $\alpha \text{:}$

      has-lan : is-lan F G F' eta
      has-lan .σ {M = M} α .η c' = ↓colim.universal c'
        (λ j → M .F₁ (j .map) D.∘ α .η (j .x))
        (λ f → D.pullr (α .is-natural _ _ _)
            ∙ pulll M ((f .sq) ∙ C'.idl _))
      has-lan .σ {M = M} α .is-natural x y f = ↓colim.unique₂ _ _
        (λ f → D.pullr (α .is-natural _ _ _)
             ∙ pulll M (C'.pullr (f .sq) ∙ C'.elim-inner refl))
        (λ j → D.pullr (↓colim.factors _ _ _)
             ∙ ↓colim.factors _ _ _)
        (λ j → D.pullr (↓colim.factors _ _ _)
             ∙ D.pulll (sym (M .F-∘ _ _)))

Finally, commutativity and uniqueness follow from the corresponding properties of colimits.

      has-lan .σ-comm {M = M} = ext λ c →
        ↓colim.factors _ _ _ ∙ D.eliml (M .F-id)
      has-lan .σ-uniq {M = M} {α = α} {σ' = σ'} p = ext λ c' → sym $
        ↓colim.unique _ _ _ _ λ j →
        σ' .η c' D.∘ ↓colim.ψ c' j                                ≡⟨ ap (λ ϕ → σ' .η c' D.∘ ↓colim.ψ c' ϕ) (↓Obj-path _ _ refl refl (sym (C'.idr _))) ⟩≡
        (σ' .η c' D.∘ ↓colim.ψ c' (↓obj (j .map C'.∘ C'.id)))     ≡⟨ D.pushr (sym $ ↓colim.factors _ _ _) ⟩≡
        (σ' .η c' D.∘ ↓colim.universal _ _ _) D.∘ ↓colim.ψ _ _    ≡⟨ D.pushl (σ' .is-natural _ _ _) ⟩≡
        M .F₁ (j .map) D.∘ (σ' .η _ D.∘ ↓colim.ψ _ (↓obj C'.id))  ≡˘⟨ (D.refl⟩∘⟨ (p ηₚ j .x)) ⟩≡˘
        M .F₁ (j .map) D.∘ α .η (j .x)                            ∎

All that remains is to bundle up the data!

      lan : Lan F G
      lan .Lan.Ext = F'
      lan .Lan.eta = eta
      lan .Lan.has-lan = has-lan

And, if $\mathcal{D}$ is $\kappa \text{-cocomplete,}$ then it certainly has the required colimits: we can “un-weaken” our result.

  cocomplete→lan : is-cocomplete ℓ ℓ D → Lan F G
  cocomplete→lan colimits = comma-colimits→lan (λ c' → colimits (↓Dia c'))

Next, we shall show that the left extension we just constructed is pointwise. To do this, we will show a more general fact: if $H:D\to E$ is $\kappa \text{-cocontinuous,}$ then it also preserves extensions “built from” colimits.

module _
  {o o' ℓ ℓ'}
  {C : Precategory ℓ ℓ} {C' : Precategory o ℓ} {D : Precategory o' ℓ'}
  (F : Functor C C') (G : Functor C D)
  where

  private
    module C = Cat.Reasoning C
    module C' = Cat.Reasoning C'
    module D = Cat.Reasoning D
    open Func
    open ↓Obj
    open ↓Hom
    open _=>_
    open is-lan

The mathematical content of the proof is quite straightforward: $H$ preserves the colimits used to construct the extension, so we can perform the exact same process in $\mathcal{E}$ to obtain a left extension. However, the mechanical content of this proof is less pleasant: we end up being off by a bunch of natural isomorphisms.

  preserves-colimits→preserves-pointwise-lan
    : ∀ {o'' ℓ''} {E : Precategory o'' ℓ''}
    → (colimits : is-cocomplete ℓ ℓ D)
    → (H : Functor D E)
    → is-cocontinuous ℓ ℓ H
    → preserves-lan H (Lan.has-lan (cocomplete→lan F G colimits))
  preserves-colimits→preserves-pointwise-lan {E = E} colimits H cocont =
    natural-isos→is-lan idni idni HF'-cohere fixup $
      comma-colimits→lan.has-lan F (H F∘ G) H-↓colim
    where
      module E = Cat.Reasoning E
      open make-natural-iso
      open Func

      ↓colim : (c' : C'.Ob) → Colimit (G F∘ Dom F (!Const c'))
      ↓colim c' = colimits (G F∘ Dom F (!Const c'))

      module ↓colim c' = Colimit (↓colim c')

      H-↓colim : (c' : C'.Ob) → Colimit ((H F∘ G) F∘ Dom F (!Const c'))
      H-↓colim c' =
        natural-iso→colimit ni-assoc $
        preserves-colimit.colimit cocont (↓colim c')

      module H-↓colim c' = Colimit (H-↓colim c')

      F' : Functor C' D
      F' = comma-colimits→lan.F' F G λ c' → colimits (G F∘ Dom F (!Const c'))

      HF' : Functor C' E
      HF' = comma-colimits→lan.F' F (H F∘ G) H-↓colim

      HF'-cohere : HF' ≅ⁿ H F∘ F'
      HF'-cohere = to-natural-iso mi where
        mi : make-natural-iso HF' (H F∘ F')
        mi .eta c' = E.id
        mi .inv c' = E.id
        mi .eta∘inv _ = E.idl _
        mi .inv∘eta _ = E.idl _
        mi .natural _ _ _ =
          E.idr _
          ∙ H-↓colim.unique _ _ _ _ (λ j → pulll H (↓colim.factors _ _ _))
          ∙ sym (E.idl _)

      module HF'-cohere = Isoⁿ HF'-cohere

      abstract
        fixup : (HF'-cohere.to ◆ idnt) ∘nt comma-colimits→lan.eta F (H F∘ G) _ ∘nt idnt ≡ nat-assoc-to (H ▸ comma-colimits→lan.eta F G _)
        fixup = ext λ j →
          (H .F₁ (↓colim.universal _ _ _) E.∘ E.id) E.∘ (H-↓colim.ψ _ _ E.∘ E.id) ≡⟨ ap₂ E._∘_ (E.idr _) (E.idr _) ⟩≡
          H .F₁ (↓colim.universal _ _ _) E.∘ H-↓colim.ψ _ _                       ≡⟨ pulll H (↓colim.factors _ _ _) ⟩≡
          H .F₁ (↓colim.ψ _ _) E.∘ E.id                                           ≡⟨ E.idr _ ⟩≡
          H .F₁ (↓colim.ψ _ (↓obj ⌜ C'.id C'.∘ C'.id ⌝))                          ≡⟨ ap! (C'.idl _) ⟩≡
          H .F₁ (↓colim.ψ _ (↓obj (C'.id)))                                       ∎

Hom functors take colimits in $\mathcal{D}$ to colimits in ${\mathbf{Sets}}^{o}p\text{,}$ so by the previous lemma, they must preserve the left extension. In other words, the extension we constructed is pointwise.

  cocomplete→pointwise-lan
    : (colim : is-cocomplete ℓ ℓ D)
    → is-pointwise-lan (Lan.has-lan (cocomplete→lan F G colim))
  cocomplete→pointwise-lan colim d =
    preserves-colimits→preserves-pointwise-lan
      colim (Functor.op (Hom-into D d))
      (よ-reverses-colimits d)

All pointwise extensions are computed via (co)limits🔗

As we’ve seen earlier, we can compute the extension of $F:\mathcal{C}\to \mathcal{D}$ along $p:\mathcal{C}\to {\mathcal{C}}^{\prime }$ when $\mathcal{D}$ has enough colimits, and that this extension is pointwise. It turns out that this is an exact characterization of the pointwise extensions: if $L$ is a pointwise extension of $F$ along $p\text{,}$ then $\mathcal{D}$ must have colimits of all diagrams of the form $F\circ \mathrm{Dom}:p\swarrow c^{\prime }\to C\to D\text{,}$ and $L$ must be computed via these colimits. This is where the name “pointwise extension” comes from — they really are computed pointwise!

module _
  {o ℓ}
  {C : Precategory ℓ ℓ} {C' : Precategory ℓ ℓ} {D : Precategory o ℓ}
  {p : Functor C C'} {F : Functor C D} {L : Functor C' D} {eta : F => L F∘ p}
  (lan : is-lan p F L eta) (pointwise : is-pointwise-lan lan)
  where

  private
    module C = Cat.Reasoning C
    module C' = Cat.Reasoning C'
    module D = Cat.Reasoning D
    module [D,Sets] = Cat.Reasoning (Cat[ D , Sets ℓ ])
    open Func
    open ↓Obj
    open ↓Hom
    open _=>_
    module lan = is-lan lan
    module pointwise d = is-lan (pointwise d)
    open is-lan

We begin by constructing a cocone for every object $c^{\prime }:{\mathcal{C}}^{\prime }\text{.}$

  ↓cocone : ∀ (c' : C'.Ob) → F F∘ Dom p (!Const c') => Const (L .F₀ c')
  ↓cocone c' .η j = L .F₁ (j .map) D.∘ eta .η _
  ↓cocone c' .is-natural _ _ f =
    D.pullr (eta .is-natural _ _ _ )
    ∙ pulll L (f .sq ∙ C'.idl _)
    ∙ sym (D.idl _)

To show that the extension is computed pointwise by these extensions, we shall appeal to the fact that colimits are representable.

  pointwise-lan→has-comma-colimits
    : ∀ (c' : C'.Ob)
    → is-colimit (F F∘ Dom p (!Const c')) (L .F₀ c') (↓cocone c')
  pointwise-lan→has-comma-colimits c' =
    represents→is-colimit $
    [D,Sets].make-invertible inv invl invr
    where

As $(L,\eta )$ is pointwise, we can represent every cocone $F\circ p\searrow c^{\prime }\to d$ as a natural transformation ${\mathcal{C}}^{\prime }(-,c^{\prime })\to \mathcal{D}(L(-),d)\text{,}$ though we do need to pass through some abstract representability nonsense to get there.

      represent-↓cocone
        : ∀ (d : D.Ob)
        → F F∘ Dom p (!Const c') => Const d
        → Functor.op (よ₀ D d) F∘ F => Functor.op (よ₀ C' c') F∘ p
      represent-↓cocone d α .η c f = α .η (↓obj f)
      represent-↓cocone d α .is-natural _ _ f = funext λ g →
        α .is-natural (↓obj (g C'.∘ p .F₁ f)) (↓obj g) (↓hom (sym (C'.idl _)))
        ∙ D.idl _

      pointwise-↓cocone
        : ∀ (d : D.Ob)
        → (α : F F∘ Dom p (!Const c') => Const d)
        → Functor.op (Hom-into D d) F∘ L => Functor.op (Hom-into C' c')
      pointwise-↓cocone d α = pointwise.σ d (represent-↓cocone d α)

We can use this representation to construct the required inverse, via the usual Yoneda-like argument.

      inv : Lim[C[F-,=]] => Hom-from D (L .F₀ c')
      inv .η d α =
        pointwise-↓cocone d α .η c' C'.id
      inv .is-natural x y f = funext λ α →
        pointwise.σ-uniq y {σ' = pointwise-↓cocone x α ∘nt (_=>_.op (よ₁ D f) ◂ L)}
          (ext λ c g → D.pushr (sym (pointwise.σ-comm x ηₚ _ $ₚ _))) ηₚ c' $ₚ C'.id

      invl : Hom-into-inj (↓cocone c') ∘nt inv ≡ idnt
      invl = ext λ d α p↓c' →
        pointwise-↓cocone d α .η _ C'.id D.∘ L .Functor.F₁ (p↓c' .map) D.∘ eta .η _ ≡⟨ D.pulll (pointwise.σ d (represent-↓cocone d α) .is-natural _ _ _ $ₚ _) ⟩≡
        pointwise-↓cocone d α .η _ ⌜ C'.id C'.∘ p↓c' .map ⌝ D.∘ eta .η _            ≡⟨ ap! (C'.idl _) ⟩≡
        pointwise-↓cocone d α .η _ (p↓c' .map) D.∘ eta .η (x p↓c')                  ≡⟨ pointwise.σ-comm d ηₚ _ $ₚ p↓c' .map ⟩≡
        α .η (↓obj (p↓c' .map))                                                     ≡⟨ ap (α .η) (↓Obj-path _ _ refl refl refl) ⟩≡
        α .η p↓c'                                                                   ∎

      vaguely-yoneda
        : ∀ {d : D.Ob} (α : D.Hom (L .F₀ c') d)
        → Functor.op (Hom-into D d) F∘ L => Functor.op (Hom-into C' c')
      vaguely-yoneda α .η c'' f = α D.∘ L .F₁ f
      vaguely-yoneda α .is-natural x y f =
        funext λ g → D.pullr (sym (L .F-∘ _ _))

      invr : inv ∘nt Hom-into-inj (↓cocone c') ≡ idnt
      invr = ext λ d α →
        unext (pointwise.σ-uniq d {σ' = vaguely-yoneda α}
          (ext λ c f → D.assoc _ _ _)) c' C'.id
        ∙ D.elimr (L .F-id)

A corollary is that if $(L,\eta )$ is a pointwise left extension along a fully faithful functor, then $\eta$ is a natural isomorphism.

  ff→pointwise-lan-ext : is-fully-faithful p → is-invertibleⁿ eta

The idea is to use the fact that $L$ is computed via colimits to construct an inverse to $\eta \text{.}$ In particular, we use the universal map out of each colimit, relying on the full faithfulness of $p$ to construct the requisite cocone.

  ff→pointwise-lan-ext p-ff =
     invertible→invertibleⁿ eta λ c →
       D.make-invertible (inv c)
         (pointwise-colim.unique₂ _ _
           (λ f → D.pullr (eta .is-natural _ _ _)
                ∙ pulll L (sym (p .F-∘ _ _) ∙ path f))
           (λ j → D.pullr (pointwise-colim.factors _ {j = j} _ _)
                ∙ eta .is-natural _ _ _)
           (λ j → D.idl _
                ∙ ap₂ D._∘_ (ap (L .F₁) (sym (equiv→counit p-ff (j .map)))) refl))
         (pointwise.σ-comm _ ηₚ c $ₚ C'.id
          ∙ elim F (ap (equiv→inverse p-ff) (sym (p .F-id)) ∙ equiv→unit p-ff _))

    where
      module pointwise-colim c' = is-colimit (pointwise-lan→has-comma-colimits c')

      path
        : {c : C.Ob} {x y : ↓Obj p (!Const (p .F₀ c))} (f : ↓Hom p (!Const (p .F₀ c)) x y)
        → p .F₁ (equiv→inverse p-ff (y .map) C.∘ f .α) ≡ p .F₁ (equiv→inverse p-ff (x .map))
      path {c} {x} {y} f =
        p .F₁ (equiv→inverse p-ff (y .map) C.∘ f .α)          ≡⟨ p .F-∘ _ _ ⟩≡
        p .F₁ (equiv→inverse p-ff (y .map)) C'.∘ p .F₁ (f .α) ≡⟨ equiv→counit p-ff _ C'.⟩∘⟨refl ⟩≡
        y .map C'.∘ p .F₁ (f .α)                              ≡⟨ f .sq ⟩≡
        C'.id C'.∘ x .map                                     ≡⟨ C'.idl _ ⟩≡
        x .map                                                ≡˘⟨ equiv→counit p-ff _ ⟩≡˘
        p .F₁ (equiv→inverse p-ff (x .map)) ∎

      inv : ∀ c → D.Hom (L .F₀ (p .F₀ c)) (F .F₀ c)
      inv c =
        pointwise-colim.universal (p .F₀ c)
          (λ j → F .F₁ (equiv→inverse p-ff (j .map)))
          (λ {x} {y} f → collapse F (ff→faithful {F = p} p-ff (path f)))

module _
  {o o' ℓ ℓ'}
  {C : Precategory ℓ ℓ} {C' : Precategory o ℓ} {D : Precategory o' ℓ'}
  (F : Functor C C') (G : Functor C D)
  where

  private
    module C = Cat.Reasoning C
    module C' = Cat.Reasoning C'
    module D = Cat.Reasoning D
    open Func
    open ↓Obj
    open ↓Hom
    open _=>_
    open Lan

  -- We don't use 'ff→pointwise-lan-ext' here, as it has a more restrictive
  -- universe bound.
  ff→cocomplete-lan-ext
    : (cocompl : is-cocomplete ℓ ℓ D)
    → is-fully-faithful F
    → cocomplete→lan F G cocompl .Ext F∘ F ≅ⁿ G
  ff→cocomplete-lan-ext cocompl ff = (to-natural-iso ni) ni⁻¹ where
    open comma-colimits→lan F G (λ c' → cocompl (G F∘ Dom F (!Const c')))
    open make-natural-iso renaming (eta to to)
    module ff {x} {y} = Equiv (_ , ff {x} {y})

    ni : make-natural-iso G (F' F∘ F)
    ni .to x = ↓colim.ψ _ (↓obj C'.id)
    ni .inv x = ↓colim.universal _
      (λ j → G .F₁ (ff.from (j .map)))
      (λ f → collapse G $ ff→faithful {F = F} ff $
           F .F-∘ _ _
        ·· ap₂ C'._∘_ (ff.ε _) refl
        ·· f .sq
        ·· C'.idl _
        ·· sym (ff.ε _))
    ni .eta∘inv x = ↓colim.unique₂ _ _
      (λ f → ↓colim.commutes _ f)
      (λ j → D.pullr (↓colim.factors _ _ _)
           ∙ ↓colim.commutes _ (↓hom (ap₂ C'._∘_ refl (ff.ε _))))
      (λ j → D.idl _)
    ni .inv∘eta x =
        ↓colim.factors _ _ _
      ∙ elim G (ap ff.from (sym (F .F-id)) ∙ ff.η _)
    ni .natural x y f =
        ↓colim.factors _ _ _
      ∙ sym (↓colim.commutes _ (↓hom (ap₂ C'._∘_ refl (sym (C'.idr _)))))