open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Pushout where


# Pushoutsπ

module _ {o β} (C : Precategory o β) where
open Cat.Reasoning C
private variable
Q X Y Z : Ob
h iβ' iβ' : Hom X Y


A pushout of and 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 and 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 and embed and into and the maps and determine what parts of and we ought to identify in

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
universalβiβ : {p : iβ' β f β‘ iβ' β g} β universal p β iβ β‘ iβ'
universalβiβ : {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