open import Cat.Prelude module Cat.Diagram.Pushout {o β} (C : Precategory o β) where
Pushoutsπ
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.
colimiting : β {Q} {iββ² : Hom Y Q} {iββ² : Hom Z Q} β iββ² β f β‘ iββ² β g β Hom P Q iββcolimiting : {p : iββ² β f β‘ iββ² β g} β colimiting p β iβ β‘ iββ² iββcolimiting : {p : iββ² β f β‘ iββ² β g} β colimiting p β iβ β‘ iββ² unique : {p : iββ² β f β‘ iββ² β g} {colimβ² : Hom P Q} β colimβ² β iβ β‘ iββ² β colimβ² β iβ β‘ iββ² β colimβ² β‘ colimiting p
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