open import Cat.Prelude

module Cat.Diagram.Pushout {o β} (C : Precategory o β) where



# Pushoutsπ

open Precategory C
private variable
Q X Y Z : Ob
h iβ' iβ' : Hom X Y


A pushout $Y +_X Z$ of $f : X \to Y$ and $g : X \to Z$ is the dual construction to the pullback. Much like the pullback is a subobject of the product, the pushout is a quotient object of the coproduct. The maps $f$ and $g$ tell us which parts of the coproduct to identify.

record is-pushout {P} (f : Hom X Y) (iβ : Hom Y P) (g : Hom X Z) (iβ : Hom Z P)
: Type (o β β) where
field
square     : iβ β f β‘ iβ β g


The most important part of the pushout is a commutative square of the following shape:

This can be thought of as providing βgluing instructionsβ. The injection maps $i_1$ and $i_2$ embed $Y$ and $Z$ into $P$, and the maps $f$ and $g$ determine what parts of $Y$ and $Z$ we ought to identify in $P$.

The universal property ensures that we only perform the minimal number of identifications required to make the aforementioned square commute.

      universal : β {Q} {iβ' : Hom Y Q} {iβ' : Hom Z Q}
β iβ' β f β‘ iβ' β g β Hom P Q
iββuniversal : {p : iβ' β f β‘ iβ' β g} β universal p β iβ β‘ iβ'
iββuniversal : {p : iβ' β f β‘ iβ' β g} β universal p β iβ β‘ iβ'

unique : {p : iβ' β f β‘ iβ' β g} {colim' : Hom P Q}
β colim' β iβ β‘ iβ'
β colim' β iβ β‘ iβ'
β colim' β‘ universal p

uniqueβ
: {p : iβ' β f β‘ iβ' β g} {colim' colim'' : Hom P Q}
β colim' β iβ β‘ iβ' β colim' β iβ β‘ iβ'
β colim'' β iβ β‘ iβ' β colim'' β iβ β‘ iβ'
β colim' β‘ colim''
uniqueβ {p = o} p q r s = unique {p = o} p q β sym (unique r s)


We provide a convenient packaging of the pushout and the injection maps:

record Pushout (f : Hom X Y) (g : Hom X Z) : Type (o β β) where
field
{coapex} : Ob
iβ       : Hom Y coapex
iβ       : Hom Z coapex
has-is-po  : is-pushout f iβ g iβ

open is-pushout has-is-po public