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. and ), 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 .Ξ· _ β°.β D.β (F.β (h .Ξ²))) β°.β D.β (f .map) β‘
cone .Ξ· _ β°.β D.β β F.β (h .Ξ²) π.β f .map β       β‘
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 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 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 1)
Ξ» f β β°.pulll (colim.factors _ _) β p (f .map)
mc .unique eta p other q =
colim.unique _ _ _ Ξ» j β
sym (
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 free objects: 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 (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π 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 = 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