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 universal : β {F} {eβ² : Hom B F} (p : eβ² β f β‘ eβ² β g) β Hom E F factors : β {F} {eβ² : Hom B F} {p : eβ² β f β‘ eβ² β g} β universal p β coeq β‘ eβ² unique : β {F} {eβ² : Hom B F} {p : eβ² β f β‘ eβ² β g} {colim : Hom E F} β colim β coeq β‘ eβ² β colim β‘ universal p uniqueβ : β {F} {eβ² : Hom B F} {o1 o2 : Hom E F} β (eβ² β f β‘ eβ² β g) β o1 β coeq β‘ eβ² β o2 β coeq β‘ eβ² β o1 β‘ o2 uniqueβ p q r = unique {p = p} q β sym (unique r) id-coequalise : id β‘ universal coequal id-coequalise = unique (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 p β©β‘ universal (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 .universal {eβ² = c2} (co2 .coequal)) (co2 .universal {eβ² = c1} (co1 .coequal)) (uniqueβ co2 (co2 .coequal) (pullr (co2 .factors) β co1 .factors) (idl _)) (uniqueβ co1 (co1 .coequal) (pullr (co1 .factors) β co2 .factors) (idl _)) where open is-coequaliser