module Cat.Functor.Final where

Final functorsπŸ”—

A final functor expresses an equivalence of diagram schemata for the purposes of computing colimits: if is final, then colimits for are equivalent to colimits for 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.

Finality has an elementary characterisation: we define a functor to be final if, for every the comma category is connected. That is, unpacking, the following data: for every object an object and a map and for every span

a finite zigzag of morphisms from to inducing a chain of commuting triangles from to For example, in the case of a β€œcospan” zigzag

  is-final : Type (o βŠ” β„“ βŠ” o' βŠ” β„“')
  is-final = βˆ€ d β†’ is-connected-cat (d ↙ F)

The utility of this definition comes, as mentioned, from the ability to move (colimiting) cocones back and forth between a diagram and its restriction to the domain category If we have a cocone then precomposition with the map (where comes from the finality of defines a cocone

However, since the comma category is merely inhabited, we need to make sure that this extension is independent of the choice of and This follows from naturality of the cocone and by connectedness of 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 = βˆ₯-βˆ₯-rec!
          (Meander-rec-≑ (el! _) (extend d) (extend-const1 d))
          (fin.zigzag d f g)

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 2)
        (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 1)
        (Ξ» ex β†’ extend-cocone-elim y
          (Ξ» ey β†’ ey β„°.∘ D.₁ f ≑ extend x ex)
          (Ξ» _ β†’ hlevel 1)
          Ξ» ey β†’ β„°.pullr (sym (D.F-∘ _ _))
               βˆ™ sym (extend-const x ex (↓obj (ey .map π’Ÿ.∘ f))))
        βˆ™ sym (β„°.idl _)

In the other direction, suppose that we have a cocone β€” inserting in the appropriate places makes a cocone

    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 .inv = restrict-cocone
    extend-cocone-is-iso .rinv K = ext Ξ» o β†’
      extend-cocone-elim (restrict-cocone K) o
        (Ξ» ex β†’ ex ≑ K .Ξ· o)
        (Ξ» _ β†’ hlevel 1)
        Ξ» _ β†’ K .is-natural _ _ _ βˆ™ β„°.idl _
    extend-cocone-is-iso .linv K = ext Ξ» o β†’
      extend-cocone-elim K (F.β‚€ o)
        (Ξ» ex β†’ ex ≑ K .Ξ· o)
        (Ξ» _ β†’ hlevel 1)
        Ξ» 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)
The proof of the auxiliary lemma is a direct computation, so we’ll leave it in this <details> tag for the curious reader only.
    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 eps p =
          colim.universal (Ξ» j β†’ eps (F.β‚€ j)) Ξ» f β†’ p (F.₁ f)
        mc .factors {j} eps p =
          extend-cocone-elim K j
            (Ξ» ex β†’ mc .universal eps p β„°.∘ ex ≑ eps j)
            (Ξ» _ β†’ hlevel 1)
            Ξ» f β†’ β„°.pulll (colim.factors _ _) βˆ™ p (f .map)
        mc .unique eps 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 are fibres of over and so finality says that is a connected map.

Essential surjectivity on objects pretty much exactly says that each comma category 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 observe that connectedness of the comma category gives us a zigzag between and but since is a pregroupoid we can evaluate this zigzag to a single morphism such that

    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 universal morphisms: since the comma categories 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 (L⊣Rβ†’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! {A = π’ž} top)
terminal→inclusion-is-final top term = right-adjoint-is-final
  (terminal→inclusion-is-right-adjoint _ top term)

Closure under compositionπŸ”—

We now prove that final functors are closed under composition.

First, given an object we get a map using the finality of and a map using the finality of which we can compose into an object of

  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 finality of gives us a zigzag between and in but we need a zigzag between and in Thus we have to refine our zigzag step by step, using the finality of

  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 whereby and are related if, for any extensions and there merely exists a zigzag between the corresponding objects of

    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 1

That this is a congruence is easily checked using the finality of

      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

      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 = ↓Obj-path _ _ refl 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

References