open import Cat.Prelude module Cat.Diagram.Coequaliser {o β} (C : Precategory o β) where
Coequalisersπ
The coequaliser of two maps (if it exists), represents the largest quotient object of that identifies and .
record is-coequaliser {E} (f g : Hom A B) (coeq : Hom B E) : Type (o β β) where field coequal : coeq β f β‘ coeq β g coequalise : β {F} {eβ² : Hom B F} (p : eβ² β f β‘ eβ² β g) β Hom E F universal : β {F} {eβ² : Hom B F} {p : eβ² β f β‘ eβ² β g} β coequalise p β coeq β‘ eβ² unique : β {F} {eβ² : Hom B F} {p : eβ² β f β‘ eβ² β g} {colim : Hom E F} β eβ² β‘ colim β coeq β colim β‘ coequalise p uniqueβ : β {F} {eβ² : Hom B F} {p : eβ² β f β‘ eβ² β g} {colim' colim'' : Hom E F} β eβ² β‘ colim' β coeq β eβ² β‘ colim'' β coeq β colim' β‘ colim'' uniqueβ {p = p} q r = unique {p = p} q β sym (unique r) id-coequalise : id β‘ coequalise coequal id-coequalise = unique (sym (idl _))
There is also a convenient bundling of an coequalising arrow together with its codomain:
record Coequaliser (f g : Hom A B) : Type (o β β) where field {coapex} : Ob coeq : Hom B coapex has-is-coeq : is-coequaliser f g coeq open is-coequaliser has-is-coeq public
Coequalisers are epicπ
Dually to the situation with equalisers, coequaliser arrows are always
is-coequaliserβis-epic : β {E} (coequ : Hom A E) β is-coequaliser f g coequ β is-epic coequ is-coequaliserβis-epic {f = f} {g = g} equ equalises h i p = h β‘β¨ unique (sym p) β©β‘ coequalise (extendr coequal) β‘Λβ¨ unique refl β©β‘Λ i β where open is-coequaliser equalises coequaliser-unique : β {E Eβ²} {c1 : Hom A E} {c2 : Hom A Eβ²} β is-coequaliser f g c1 β is-coequaliser f g c2 β E β Eβ² coequaliser-unique {c1 = c1} {c2} co1 co2 = make-iso (co1 .coequalise {eβ² = c2} (co2 .coequal)) (co2 .coequalise {eβ² = c1} (co1 .coequal)) (uniqueβ co2 {p = co2 .coequal} (sym (pullr (co2 .universal) β co1 .universal)) (introl refl)) (uniqueβ co1 {p = co1 .coequal} (sym (pullr (co1 .universal) β co2 .universal)) (introl refl)) where open is-coequaliser