open import Cat.Diagram.Pushout.Properties
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Coproduct
open import Cat.Diagram.Initial
open import Cat.Diagram.Pushout
open import Cat.Prelude
open import Cat.Finite

import Cat.Reasoning as Cat

module Cat.Diagram.Colimit.Finite where

module _ {β β'} (C : Precategory β β') where
open Cat C


# Finitely cocomplete categoriesπ

Finitely cocomplete categories are dual to finitely complete categories in that they admit colimits for all diagrams of finite shape.

  is-finitely-cocomplete : TypeΟ
is-finitely-cocomplete = β {o β} {D : Precategory o β} β is-finite-precategory D
β (F : Functor D C) β Colimit F


Equivalently, a finitely cocomplete category has:

• An initial object (colimit over the empty diagram)
• All binary coproducts (colimits over any diagrams of shape
• All binary coequalisers (colimits over any diagrams of shape
• All binary pushouts (colimits over any diagrams of shape
  record Finitely-cocomplete : Type (β β β') where
field
initial      : Initial C
coproducts   : β A B β Coproduct C A B
coequalisers : β {A B} (f g : Hom A B) β Coequaliser C f g
pushouts     : β {A B X} (f : Hom X A) (g : Hom X B) β Pushout C f g

Coequ : β {A B} (f g : Hom A B) β Ob
Coequ f g = coequalisers f g .Coequaliser.coapex

Po : β {A B C} (f : Hom C A) (g : Hom C B) β Ob
Po f g = pushouts f g .Pushout.coapex

open Finitely-cocomplete


As seen on the page for finitely complete categories, this definition equivalently states that a finitely cocomplete category has either of the following:

• An initial object, all binary coproducts, and all binary coequalisers
• An initial object and all binary pushouts

This follows from the fact that we can build coproducts and coequalisers from pushouts, and that conversely, we can build pushouts from coproducts and coequalisers. We begin by proving the latter.

## With coequalisersπ

We construct a pushout under a span as a quotient object of a coproduct i.e.Β the coequaliser of and where and are injections into the coproduct.

Where is some object which admits injections and from X and Y respectively. This coequaliser represents a pushout

where is the pushoutβs coapex, or equivalently, the coequaliser of and

  coproduct-coequaliserβpushout
: β {E P X Y Z} {in1 : Hom X P} {in2 : Hom Y P} {f : Hom Z X}
{g : Hom Z Y} {e : Hom P E}
β is-coproduct C in1 in2
β is-coequaliser C (in1 β f) (in2 β g) e
β is-pushout C f (e β in1) g (e β in2)
coproduct-coequaliserβpushout {in1 = in1} {in2} {f} {g} {e} cp cq = po where
open is-pushout
module cq = is-coequaliser cq
module cp = is-coproduct cp

po : is-pushout C _ _ _ _
po .square = sym (assoc _ _ _) β cq.coequal β assoc _ _ _
po .universal {iβ' = iβ'} {iβ'} p =
cq.universal {e' = cp.[ iβ' , iβ' ]} (
cp.[ iβ' , iβ' ] β (in1 β f) β‘β¨ pulll cp.[]βΞΉβ β©β‘
iβ' β f                      β‘β¨ p β©β‘
iβ' β g                      β‘Λβ¨ pulll cp.[]βΞΉβ β©β‘Λ
cp.[ iβ' , iβ' ] β (in2 β g) β
)
po .universalβiβ = pulll cq.factors β cp.[]βΞΉβ
po .universalβiβ = pulll cq.factors β cp.[]βΞΉβ
po .unique p q =
cq.unique ((cp.unique (sym (assoc _ _ _) β p) (sym (assoc _ _ _) β q)))


Thus, if a category has an initial object, binary coproducts, and binary coequalisers, it is finitely cocomplete.

  with-coequalisers
: Initial C
β (β A B β Coproduct C A B)
β (β {A B} (f g : Hom A B) β Coequaliser C f g)
β Finitely-cocomplete
with-coequalisers init copr coeq .initial      = init
with-coequalisers init copr coeq .coproducts   = copr
with-coequalisers init copr coeq .coequalisers = coeq
with-coequalisers init copr coeq .pushouts {A} {B} {X} f g =
record { has-is-po = coproduct-coequaliserβpushout Copr.has-is-coproduct Coequ.has-is-coeq }
where
module Copr = Coproduct (copr A B)
module Coequ = Coequaliser (coeq (Copr.ΞΉβ β f) (Copr.ΞΉβ β g))


## With pushoutsπ

A coproduct is a pushout under a span whose vertex is the initial object.

  initial-pushoutβcoproduct
: β {P X Y I} {in1 : Hom X P} {in2 : Hom Y P} {f : Hom I X} {g : Hom I Y}
β is-initial C I β is-pushout C f in1 g in2 β is-coproduct C in1 in2
initial-pushoutβcoproduct {in1 = in1} {in2} {f} {g} init po = coprod where
module Po = is-pushout po

coprod : is-coproduct C in1 in2
coprod .is-coproduct.[_,_] in1' in2' =
Po.universal {iβ' = in1'} {iβ' = in2'} (is-contrβis-prop (init _) _ _)
coprod .is-coproduct.[]βΞΉβ = Po.universalβiβ
coprod .is-coproduct.[]βΞΉβ = Po.universalβiβ
coprod .is-coproduct.unique p q = Po.unique p q

with-pushouts
: Initial C
β (β {A B X} (f : Hom X A) (g : Hom X B) β Pushout C f g)
β Finitely-cocomplete
with-pushouts bot po = fcc where
module bot = Initial bot
mkcoprod : β A B β Coproduct C A B
mkcoprod A B = record { has-is-coproduct = initial-pushoutβcoproduct bot.hasβ₯ po' }
where po' = po (bot.hasβ₯ A .centre) (bot.hasβ₯ B .centre) .Pushout.has-is-po

mkcoeq : β {A B} (f g : Hom A B) β Coequaliser C f g
mkcoeq {A = A} {B} f g = coequ where


The construction of coequalisers from pushouts follows its dual.

      module A+A = Coproduct (mkcoprod A A)
[id,id] : Hom A+A.coapex A
[id,id] = A+A.[ id , id ]

[f,g] : Hom A+A.coapex B
[f,g] = A+A.[ f , g ]

module Po = Pushout (po [f,g] [id,id])

open is-coequaliser
open Coequaliser

      coequ : Coequaliser C f g
coequ .coapex = Po.coapex
coequ .coeq = Po.iβ
coequ .has-is-coeq .coequal =
Po.iβ β f                  β‘Λβ¨ ap (Po.iβ β_) A+A.[]βΞΉβ β©β‘Λ
Po.iβ β [f,g] β A+A.ΞΉβ     β‘β¨ assoc _ _ _ β ap (_β A+A.ΞΉβ) Po.square β©β‘
(Po.iβ β [id,id]) β A+A.ΞΉβ β‘β¨ sym (assoc _ _ _) β pushr (A+A.[]βΞΉβ β sym A+A.[]βΞΉβ) β©β‘
(Po.iβ β [id,id]) β A+A.ΞΉβ β‘β¨ ap (_β A+A.ΞΉβ) (sym Po.square) β©β‘
(Po.iβ β [f,g]) β A+A.ΞΉβ   β‘β¨ sym (assoc _ _ _) β ap (Po.iβ β_) A+A.[]βΞΉβ β©β‘
Po.iβ β g                  β
coequ .has-is-coeq .universal {e' = e'} p =
Po.universal (A+A.uniqueβ refl refl (in1) (in2))
where
in1 : ((e' β f) β [id,id]) β A+A.ΞΉβ β‘ (e' β [f,g]) β A+A.ΞΉβ
in1 =
((e' β f) β [id,id]) β A+A.ΞΉβ β‘β¨ cancelr A+A.[]βΞΉβ β©β‘ -- β‘β¨ cancell A+A.[]βΞΉβ β©
e' β f                        β‘Λβ¨ pullr A+A.[]βΞΉβ β©β‘Λ -- β‘Λβ¨ pulll A+A.[]βΞΉβ β©
(e' β [f,g]) β A+A.ΞΉβ         β

in2 : ((e' β f) β [id,id]) β A+A.ΞΉβ β‘ (e' β [f,g]) β A+A.ΞΉβ
in2 =
((e' β f) β [id,id]) β A+A.ΞΉβ β‘β¨ cancelr A+A.[]βΞΉβ β©β‘
e' β f                        β‘β¨ p β©β‘
e' β g                        β‘Λβ¨ pullr A+A.[]βΞΉβ β©β‘Λ
(e' β [f,g]) β A+A.ΞΉβ         β

coequ .has-is-coeq .factors = Po.universalβiβ
coequ .has-is-coeq .unique {F} {e' = e'} {colim = colim} e'=colβiβ =
Po.unique e'=colβiβ path
where
path : colim β Po.iβ β‘ e' β f
path =
colim β Po.iβ                        β‘β¨ insertr A+A.[]βΞΉβ β©β‘
((colim β Po.iβ) β [id,id]) β A+A.ΞΉβ β‘β¨ ap (_β A+A.ΞΉβ) (extendr (sym Po.square)) β©β‘
((colim β Po.iβ) β [f,g]) β A+A.ΞΉβ   β‘β¨ ap (_β A+A.ΞΉβ) (ap (_β [f,g]) e'=colβiβ) β©β‘
(e' β [f,g]) β A+A.ΞΉβ                β‘β¨ pullr A+A.[]βΞΉβ β©β‘
e' β f           β

fcc : Finitely-cocomplete
fcc .initial      = bot
fcc .coproducts   = mkcoprod
fcc .coequalisers = mkcoeq
fcc .pushouts     = po

  coproductβinitial-pushout
: β {P X Y I} {in1 : Hom X P} {in2 : Hom Y P} {f : Hom I X} {g : Hom I Y}
β is-initial C I β is-coproduct C in1 in2 β is-pushout C f in1 g in2
coproductβinitial-pushout i r = po where
open is-pushout
po : is-pushout C _ _ _ _
po .square = is-contrβis-prop (i _) _ _
po .universal _ = r .is-coproduct.[_,_] _ _
po .universalβiβ = r .is-coproduct.[]βΞΉβ
po .universalβiβ = r .is-coproduct.[]βΞΉβ
po .unique p q = r .is-coproduct.unique p q


# Rex functorsπ

A right exact, or rex, functor is a functor that preserves finite colimits.

module _ {o β o' β'} {C : Precategory o β} {D : Precategory o' β'} where
private module C = Cat C
private module D = Cat D

  record is-rex (F : Functor C D) : Type (o β β β o' β β') where
private module F = Functor F

field
pres-β₯ : β {I} β is-initial C I β is-initial D (F.β I)
pres-pushout
: β {P X Y Z} {in1 : C.Hom X P} {in2 : C.Hom Y P}
{f : C.Hom Z X} {g : C.Hom Z Y}
β is-pushout C f in1 g in2
β is-pushout D (F.β f) (F.β in1) (F.β g) (F.β in2)
pres-coproduct
: β {P A B I} {in1 : C.Hom A P} {in2 : C.Hom B P}
β is-initial C I
β is-coproduct C in1 in2
β is-coproduct D (F.β in1) (F.β in2)
pres-coproduct  init copr = initial-pushoutβcoproduct D (pres-β₯ init)
(pres-pushout {f = init _ .centre} {g = init _ .centre}
(coproductβinitial-pushout C init copr))
pres-epis : β {A B} {f : C.Hom A B} β C.is-epic f β D.is-epic (F.β f)
pres-epis {f = f} epi = is-pushoutβis-epic
(subst (Ξ» x β is-pushout D _ x _ x) F.F-id
(pres-pushout
(is-epicβis-pushout epi)))