open import Cat.Instances.Shape.Terminal
open import Cat.Instances.Localisation
open import Cat.Diagram.Colimit.Base
open import Cat.Functor.Adjoint.Hom
open import Cat.Functor.Properties
open import Cat.Instances.Discrete
open import Cat.Diagram.Terminal
open import Cat.Functor.Constant
open import Cat.Functor.Adjoint
open import Cat.Instances.Comma
open import Cat.Connected
open import Cat.Groupoid
open import Cat.Prelude

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

open is-connected-cat
open Precategory
open Congruence
open Functor
open _=>_
open ↓Obj
open ↓Hom

module Cat.Functor.Final where

Final functors🔗

A final functor expresses an equivalence of diagram schemata for the purposes of computing colimits: if $F:\mathcal{C}\to \mathcal{D}$ is final, then colimits for $D:\mathcal{D}\to \mathcal{E}$ are equivalent to colimits for $D\circ F:\mathcal{C}\to \mathcal{E}\text{.}$ A terminological warning: in older literature (e.g. (Borceux 1994) and (Adamek and Rosicky 1994)), these functors are called cofinal, but we stick with terminology from the nLab here.

module
  _ {o ℓ o' ℓ'} {𝒞 : Precategory o ℓ} {𝒟 : Precategory o' ℓ'}
    (F : Functor 𝒞 𝒟)
  where

  open Functor

  private
    module 𝒞 = Cr 𝒞
    module 𝒟 = Cr 𝒟
    module F = Functor F

Finality has an elementary characterisation: we define a functor $F$ to be final if, for every $d\text{,}$ the comma category $d\swarrow F$ is connected. That is, unpacking, the following data: for every object $d:\mathcal{D}\text{,}$ an object $d_0$ and a map $d_{!}:d\to F(d_0)\text{,}$ and for every span

a finite zigzag of morphisms from $a$ to $b\text{,}$ inducing a chain of commuting triangles from $f$ to $g\text{.}$ For example, in the case of a “cospan” zigzag $a\to a_0\leftarrow b\text{:}$

  is-final : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ')
  is-final = ∀ d → is-connected-cat (d ↙ F)

  module is-final (fin : is-final) (d : 𝒟.Ob) = is-connected-cat (fin d)

  module
    _ {o'' ℓ''} {ℰ : Precategory o'' ℓ''} {D : Functor 𝒟 ℰ} (final : is-final)
    where
    private
      module fin = is-final final
      module D = Func D
      module ℰ = Cr ℰ

The utility of this definition comes, as mentioned, from the ability to move (colimiting) cocones back and forth between a diagram $D$ and its restriction $D_{|F}$ to the domain category $\mathcal{C}\text{.}$ If we have a cocone $\kappa :\{DF(d)\to K\}\text{,}$ then precomposition with the map $D(d_{!}):D(d)\to DF(d_0)$ (where $d_{!}:d\to F(d_0)$ comes from the finality of $F\text{)}$ defines a cocone $\{D(d)\to K\}\text{.}$

However, since the comma category $d\swarrow F$ is merely inhabited, we need to make sure that this extension is independent of the choice of $d_0$ and $d_{!}\text{.}$ This follows from naturality of the cocone and by connectedness of $d\swarrow F\text{,}$ as expressed by the commutativity of the following diagram:

    module _ {coapex} (cone : D F∘ F => Const coapex) where
      extend : ∀ d → Ob (d ↙ F) → ℰ.Hom (D.₀ d) coapex
      extend d f = cone .η (f .y) ℰ.∘ D.₁ (f .map)

      opaque
        extend-const1
          : ∀ d {f g : Ob (d ↙ F)} (h : ↓Hom _ _ f g)
          → extend d f ≡ extend d g
        extend-const1 d {f} {g} h =
          cone .η _ ℰ.∘ D.₁ (f .map)                        ≡˘⟨ cone .is-natural _ _ _ ∙ ℰ.idl _ ℰ.⟩∘⟨refl ⟩≡˘
          (cone .η _ ℰ.∘ D.₁ (F.₁ (h .β))) ℰ.∘ D.₁ (f .map) ≡⟨ D.pullr refl ⟩≡
          cone .η _ ℰ.∘ D.₁ ⌜ F.₁ (h .β) 𝒟.∘ f .map ⌝       ≡⟨ ap! (sym (h .sq) ∙ 𝒟.idr _) ⟩≡
          cone .η _ ℰ.∘ D.₁ (g .map)                        ∎

      opaque
        extend-const
          : ∀ d (f g : Ob (d ↙ F))
          → extend d f ≡ extend d g
        extend-const d f g = case fin.zigzag d f g of
          Meander-rec-≡ (el! _) (extend d) (extend-const1 d)

In order to make reasoning easier, we define the extended cocone simultaneously with an elimination principle for its components.

      extend-cocone : D => Const coapex
      extend-cocone-elim
        : ∀ d {ℓ} (P : ℰ.Hom (D.₀ d) coapex → Type ℓ)
        → (∀ f → is-prop (P f))
        → (∀ f → P (extend d f))
        → P (extend-cocone .η d)

      extend-cocone .η d = ∥-∥-rec-set (hlevel )
        (extend d) (extend-const d) (fin.point d)

      extend-cocone .is-natural x y f = extend-cocone-elim x
        (λ ex → extend-cocone .η y ℰ.∘ D.₁ f ≡ ex)
        (λ _ → hlevel )
        (λ ex → extend-cocone-elim y
          (λ ey → ey ℰ.∘ D.₁ f ≡ extend x ex)
          (λ _ → hlevel )
          λ ey → ℰ.pullr (sym (D.F-∘ _ _))
               ∙ sym (extend-const x ex (↓obj (ey .map 𝒟.∘ f))))
        ∙ sym (ℰ.idl _)

      extend-cocone-elim d P prop h = ∥-∥-elim
        {P = λ f → P (∥-∥-rec-set (hlevel ) (extend d) (extend-const d) f)}
        (λ _ → prop _) h (fin.point d)

In the other direction, suppose that we have a cocone $\{D(x)\to K\}$ — inserting $F$ in the appropriate places makes a cocone $\{DF(x)\to K\}\text{.}$

    restrict-cocone : ∀ {coapex} → D => Const coapex → D F∘ F => Const coapex
    restrict-cocone K .η x = K .η (F.₀ x)
    restrict-cocone K .is-natural x y f = K .is-natural (F.₀ x) (F.₀ y) (F.₁ f)

A computation using connectedness of the comma categories shows that these formulae are mutually inverse:

    open is-iso
    extend-cocone-is-iso : ∀ {coapex} → is-iso (extend-cocone {coapex})
    extend-cocone-is-iso .from = restrict-cocone
    extend-cocone-is-iso .rinv K = ext λ o →
      extend-cocone-elim (restrict-cocone K) o
        (λ ex → ex ≡ K .η o)
        (λ _ → hlevel )
        λ _ → K .is-natural _ _ _ ∙ ℰ.idl _
    extend-cocone-is-iso .linv K = ext λ o →
      extend-cocone-elim K (F.₀ o)
        (λ ex → ex ≡ K .η o)
        (λ _ → hlevel )
        λ f → extend-const K (F.₀ o) f (↓obj 𝒟.id) ∙ D.elimr refl

The most important conclusion that we get is the following: If you can show that the restricted cocone is a colimit, then the original cocone was a colimit, too! We’ll do this in two steps: first, show that the extension of a colimiting cocone is a colimit. Then, using the fact that restrict-cocone is an equivalence, we’ll be able to fix up the polarity mismatch.

    extend-is-colimit
      : ∀ {coapex} (K : D F∘ F => Const coapex)
      → is-colimit (D F∘ F) coapex K
      → is-colimit D coapex (extend-cocone K)

    extend-is-colimit {coapex} K colim =
      to-is-colimitp mc refl
      module extend-is-colimit where
        module colim = is-colimit colim
        open make-is-colimit

        mc : make-is-colimit D coapex
        mc .ψ x = extend-cocone K .η x
        mc .commutes f = extend-cocone K .is-natural _ _ _ ∙ ℰ.idl _
        mc .universal eta p =
          colim.universal (λ j → eta (F.₀ j)) λ f → p (F.₁ f)
        mc .factors {j} eta p =
          extend-cocone-elim K j
            (λ ex → mc .universal eta p ℰ.∘ ex ≡ eta j)
            (λ _ → hlevel )
            λ f → ℰ.pulll (colim.factors _ _) ∙ p (f .map)
        mc .unique eta p other q =
          colim.unique _ _ _ λ j →
            sym (ℰ.refl⟩∘⟨ extend-cocone-is-iso .linv K ηₚ j)
            ∙ q (F.₀ j)

    is-colimit-restrict
      : ∀ {coapex}
      → (K : D => Const coapex)
      → is-colimit (D F∘ F) coapex (restrict-cocone K)
      → is-colimit D coapex K
    is-colimit-restrict {coapex} K colim =
      to-is-colimitp
        (extend-is-colimit.mc (restrict-cocone K) colim)
        (extend-cocone-is-iso .rinv K ηₚ _)
        where open is-iso

Examples🔗

Final functors between pregroupoids have a very simple characterisation: they are the full, essentially surjective functors. In this case, there is a direct connection with homotopy type theory: groupoids are 1-types, comma categories $d\swarrow F$ are fibres of $F$ over $d\text{,}$ and so finality says that $F$ is a connected map.

Essential surjectivity on objects pretty much exactly says that each comma category $d\swarrow F$ is inhabited. To see that fullness implies the existence of zigzags, meditate on the following diagram:

  module _ (𝒞-grpd : is-pregroupoid 𝒞) (𝒟-grpd : is-pregroupoid 𝒟) where
    full+eso→final : is-full F → is-eso F → is-final
    full+eso→final full eso d .zigzag f g = do
      z , p ← full (g .map 𝒟.∘ 𝒟-grpd (f .map) .inv)
      pure $ zig
        (↓hom {β = z}
          (𝒟.idr _ ∙ sym (𝒟.rswizzle p (𝒟-grpd (f .map) .invr))))
        []
      where open 𝒟.is-invertible
    full+eso→final full eso d .point =
      ∥-∥-map (λ e → ↓obj (𝒟.from (e .snd))) (eso d)

For the other direction, given $f:Fx\to Fy\text{,}$ observe that connectedness of the comma category $Fx\swarrow F$ gives us a zigzag between $x$ and $y\text{,}$ but since $\mathcal{C}$ is a pregroupoid we can evaluate this zigzag to a single morphism $z:x\to y$ such that $Fz=f\text{.}$

    final→full+eso : is-final → is-full F × is-eso F
    final→full+eso fin .fst {x} {y} f = do
      zs ← fin (F.₀ x) .zigzag (↓obj 𝒟.id) (↓obj f)
      let z = Free-groupoid-counit
            (↓-is-pregroupoid _ _ ⊤Cat-is-pregroupoid 𝒞-grpd)
            .F₁ zs
      pure (z .β , sym (𝒟.idr _) ∙ sym (z .sq) ∙ 𝒟.idr _)
    final→full+eso fin .snd d = do
      fd ← fin d .point
      pure (fd .y , 𝒟.invertible→iso (fd .map) (𝒟-grpd _) 𝒟.Iso⁻¹)

Another general class of final functors is given by right adjoint functors. This follows directly from the characterisation of right adjoints in terms of free objects: since the comma categories $c\swarrow R$ have initial objects, they are connected.

right-adjoint-is-final
  : ∀ {o ℓ o' ℓ'} {𝒞 : Precategory o ℓ} {𝒟 : Precategory o' ℓ'}
  → {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (L⊣R : L ⊣ R)
  → is-final R
right-adjoint-is-final L⊣R c =
  initial→connected (left-adjoint→universal-maps L⊣R c)

In particular, the inclusion of a terminal object into a category is a final functor. This means that the colimit of any diagram over a shape category with a terminal object is simply the value of the diagram on the terminal object.

terminal→inclusion-is-final
  : ∀ {o ℓ} {𝒞 : Precategory o ℓ}
  → (top : 𝒞 .Ob) (term : is-terminal 𝒞 top)
  → is-final (!Const {C = 𝒞} top)
terminal→inclusion-is-final top term = right-adjoint-is-final
  (is-terminal→inclusion-is-right-adjoint _ top term)

Closure under composition🔗

module
  _ {o ℓ o' ℓ' o'' ℓ''}
    {𝒞 : Precategory o ℓ} {𝒟 : Precategory o' ℓ'} {ℰ : Precategory o'' ℓ''}
    (F : Functor 𝒞 𝒟) (G : Functor 𝒟 ℰ)
    (f-fin : is-final F) (g-fin : is-final G)
  where
  private
    module 𝒟 = Cr 𝒟
    module ℰ = Cr ℰ
    module G = Func G
    module F = Functor F
    module ff = is-final F f-fin
    module gf = is-final G g-fin
  open ↙-compose F G

We now prove that final functors are closed under composition.

First, given an object $c:\mathcal{C}$ we get a map $g:c\to G{c}_0$ using the finality of $G$ and a map $f:c_0\to F{c}_1$ using the finality of $F\text{,}$ which we can compose into an object of $c\swarrow G\circ F\text{.}$

  F∘-is-final : is-final (G F∘ F)
  F∘-is-final c .point = do
    g ← gf.point c
    f ← ff.point (g .y)
    pure (g ↙> f)

Now, given a span $GFx\leftarrow c\to GFy\text{,}$ finality of $G$ gives us a zigzag between $Fx$ and $Fy$ in $c\swarrow G\text{,}$ but we need a zigzag between $x$ and $y$ in $c\swarrow G\circ F\text{.}$ Thus we have to refine our zigzag step by step, using the finality of $F\text{.}$

  F∘-is-final c .zigzag f g = do
    gz ← gf.zigzag c (↓obj (f .map)) (↓obj (g .map))
    fz ← refine gz (↓obj 𝒟.id) (↓obj 𝒟.id)
    pure (subst₂ (Meander (c ↙ G F∘ F)) ↙>-id ↙>-id fz)

We start by defining a congruence on the objects of $c\swarrow G\text{,}$ whereby $f:c\to Gx$ and $g:c\to Gy$ are related if, for any extensions $f^{\prime }:x\swarrow F$ and $g^{\prime }:y\swarrow F\text{,}$ there merely exists a zigzag between the corresponding objects of $c\swarrow G\circ F\text{:}$

    where
      R : Congruence (Ob (c ↙ G)) _
      R ._∼_ f g =
        ∀ (f' : Ob (f .y ↙ F)) (g' : Ob (g .y ↙ F))
        → ∥ Meander (c ↙ G F∘ F) (f ↙> f') (g ↙> g') ∥
      R .has-is-prop _ _ = hlevel 

That this is a congruence is easily checked using the finality of $F\text{.}$

      R .reflᶜ {f} f' g' =
        Free-groupoid-map (↙-compose f) .F₁ <$> ff.zigzag (f .y) f' g'
      R ._∙ᶜ_ {f} {g} {h} fg gh f' h' = do
        g' ← ff.point (g .y)
        ∥-∥-map₂ _++_ (gh g' h') (fg f' g')
      R .symᶜ fg g' f' = ∥-∥-map (reverse _) (fg f' g')

Using the universal mapping property of the free groupoid into congruences, we conclude by showing that any two arrows connected by a morphism are related, which again involves the connectedness of $x\swarrow F\text{.}$

      refine1 : ∀ {f g} → Hom (c ↙ G) f g → R ._∼_ f g
      refine1 {f} {g} h f' g' = do
        z ← ff.zigzag (f .y) f' (↓obj (g' .map 𝒟.∘ h .β))
        let
          z' : Meander (c ↙ G F∘ F) _ _
          z' = Free-groupoid-map (↙-compose f) .F₁ z
          fixup : f ↙> ↓obj (g' .map 𝒟.∘ h .β) ≡ g ↙> g'
          fixup = ext $ refl ,ₚ G.pushl refl ∙ (ℰ.refl⟩∘⟨ sym (h .sq) ∙ ℰ.idr _)
        pure (subst (Meander (c ↙ G F∘ F) (f ↙> f')) fixup z')

      refine : ∀ {f g} → Meander (c ↙ G) f g → R ._∼_ f g
      refine = Meander-rec-congruence R refine1