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 $\bullet\quad\bullet$)
• All binary coequalisers (colimits over any diagrams of shape $\bullet\rightrightarrows\bullet$)
• All binary pushouts (colimits over any diagrams of shape $\bullet\to\bullet\leftarrow\bullet$)
  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 $X \xleftarrow{f} Z \xrightarrow{g} Y$ as a quotient object of a coproduct $X + Y$, i.e.Β the coequaliser of $in_0f$ and $in_1g$ where $in_0$ and $in_1$ are injections into the coproduct.

Where $P'$ is some object which admits injections $i_1'$ and $i_2'$ from X and Y respectively. This coequaliser represents a pushout

where $E$ is the pushoutβs coapex, or equivalently, the coequaliser of $in_0f$ and $in_1g$.

  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.inββfactor β©β‘
iβ' β f                      β‘β¨ p β©β‘
iβ' β g                      β‘Λβ¨ pulll cp.inββfactor β©β‘Λ
cp.[ iβ' , iβ' ] β (in2 β g) β
)
po .iββuniversal = pulll cq.factors β cp.inββfactor
po .iββuniversal = pulll cq.factors β cp.inββfactor
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.inβ β f) (Copr.inβ β 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.inββfactor = Po.iββuniversal
coprod .is-coproduct.inββfactor = Po.iββuniversal
coprod .is-coproduct.unique other 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.inββfactor β©β‘Λ
Po.iβ β [f,g] β A+A.inβ   β‘β¨ assoc _ _ _ β ap (_β A+A.inβ) Po.square β©β‘
(Po.iβ β [id,id]) β A+A.inβ β‘β¨ sym (assoc _ _ _) β pushr (A+A.inββfactor β sym A+A.inββfactor) β©β‘
(Po.iβ β [id,id]) β A+A.inβ β‘β¨ ap (_β A+A.inβ) (sym Po.square) β©β‘
(Po.iβ β [f,g]) β A+A.inβ   β‘β¨ sym (assoc _ _ _) β ap (Po.iβ β_) A+A.inββfactor β©β‘
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.inβ β‘ (e' β [f,g]) β A+A.inβ
in1 =
((e' β f) β [id,id]) β A+A.inβ β‘β¨ cancelr A+A.inββfactor β©β‘ -- β‘β¨ cancell A+A.inββfactor β©
e' β f                     β‘Λβ¨ pullr A+A.inββfactor β©β‘Λ -- β‘Λβ¨ pulll A+A.inββfactor β©
(e' β [f,g]) β A+A.inβ       β

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

coequ .has-is-coeq .factors = Po.iββuniversal
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.inββfactor β©β‘
((colim β Po.iβ) β [id,id]) β A+A.inβ β‘β¨ ap (_β A+A.inβ) (extendr (sym Po.square)) β©β‘
((colim β Po.iβ) β [f,g]) β A+A.inβ   β‘β¨ ap (_β A+A.inβ) (ap (_β [f,g]) e'=colβiβ) β©β‘
(e' β [f,g]) β A+A.inβ                β‘β¨ pullr A+A.inββfactor β©β‘
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 .iββuniversal = r .is-coproduct.inββfactor
po .iββuniversal = r .is-coproduct.inββfactor
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)))