# Coequalizers defined in terms of colimits

## Contents

• Definition of coequalizers
• Coincides with the direct definition

# Definition of coequalizers in terms of colimits

Section def_coequalizers.

Variable C : precategory.
Variable hs: has_homsets C.

Local Open Scope stn.
Definition One : two := 0.
Definition Two : two := 1.

Definition Coequalizer_graph : graph.
Proof.
two.
use (@two_rec (two UU)).
- apply two_rec.
+ apply empty.
+ apply (unit ⨿ unit).
- apply (λ _, empty).
Defined.

Definition Coequalizer_diagram {a b : C} (f g : Ca, b) : diagram Coequalizer_graph C.
Proof.
(two_rec a b).
use two_rec_dep.
- use two_rec_dep; simpl.
+ apply fromempty.
+ intro x. induction x.
exact f. exact g.
- intro. apply fromempty.
Defined.

Definition Coequalizer_cocone {a b : C} (f g : Ca, b) (d : C) (h : Cb, d)
(H : f · h = g · h) : cocone (Coequalizer_diagram f g) d.
Proof.
use make_cocone.
- use two_rec_dep.
+ exact (f · h).
+ exact h.
- use two_rec_dep; use two_rec_dep.
+ exact (empty_rect _).
+ intro e. induction e.
× apply idpath.
× apply (! H).
+ exact (empty_rect _).
+ exact (empty_rect _).
Defined.

Definition isCoequalizer {a b : C} (f g : Ca, b) (d : C) (h : Cb, d)
(H : f · h = g · h) : UU := isColimCocone (Coequalizer_diagram f g) d
(Coequalizer_cocone f g d h H).

Definition make_isCoequalizer {a b : C} (f g : Ca, b) (d : C) (h : Cb, d)
(H : f · h = g · h) :
( e (h' : Cb, e) (H' : f · h' = g · h'),
iscontr (total2 (fun hk : Cd, eh · hk = h')))
isCoequalizer f g d h H.
Proof.
intros H' x cx.
assert (H1 : f · coconeIn cx Two = g · coconeIn cx Two).
{
use (pathscomp0 (coconeInCommutes cx One Two (ii1 tt))).
use (pathscomp0 _ (!(coconeInCommutes cx One Two (ii2 tt)))).
apply idpath.
}
set (H2 := (H' x (coconeIn cx Two) H1)).
use tpair.
- use (tpair _ (pr1 (pr1 H2)) _).
use two_rec_dep.
+ use (pathscomp0 _ (coconeInCommutes cx One Two (ii1 tt))).
change (coconeIn (Coequalizer_cocone f g d h H) _) with (f · h).
change (dmor _ _) with f.
rewrite <- assoc.
apply cancel_precomposition, (pr2 (pr1 H2)).
+ apply (pr2 (pr1 H2)).
- abstract (intro t; apply subtypePath;
[intros y; apply impred; intros t0; apply hs
|induction t as [t p]; apply path_to_ctr, (p Two)]).
Defined.

Definition Coequalizer {a b : C} (f g : Ca, b) : UU := ColimCocone (Coequalizer_diagram f g).

Definition make_Coequalizer {a b : C} (f g : Ca, b) (d : C) (h : Cb, d) (H : f · h = g · h)
(isCEq : isCoequalizer f g d h H) : Coequalizer f g.
Proof.
use tpair.
- use tpair.
+ exact d.
+ use Coequalizer_cocone.
× exact h.
× exact H.
- exact isCEq.
Defined.

Definition Coequalizers : UU := (a b : C) (f g : Ca, b), Coequalizer f g.

Definition hasCoequalizers : UU := (a b : C) (f g : Ca, b), ishinh (Coequalizer f g).

Definition CoequalizerObject {a b : C} {f g : Ca, b} :
Coequalizer f g C := λ H, colim H.

Definition CoequalizerArrow {a b : C} {f g : Ca, b} (E : Coequalizer f g) :
Cb, colim E := colimIn E Two.

Definition CoequalizerArrowEq {a b : C} {f g : Ca, b} (E : Coequalizer f g) :
f · CoequalizerArrow E = g · CoequalizerArrow E.
Proof.
use (pathscomp0 (colimInCommutes E One Two (ii1 tt))).
use (pathscomp0 _ (!(colimInCommutes E One Two (ii2 tt)))).
apply idpath.
Qed.

Definition CoequalizerOut {a b : C} {f g : Ca, b} (E : Coequalizer f g) e (h : Cb, e)
(H : f · h = g · h) : Ccolim E, e.
Proof.
now use colimArrow; use Coequalizer_cocone.
Defined.

Lemma CoequalizerArrowComm {a b : C} {f g : Ca, b} (E : Coequalizer f g) (e : C) (h : Cb, e)
(H : f · h = g · h) : CoequalizerArrow E · CoequalizerOut E e h H = h.
Proof.
exact (colimArrowCommutes E e _ Two).
Qed.

Lemma CoequalizerOutUnique {a b : C} {f g : Ca, b} (E : Coequalizer f g) (e : C) (h : Cb, e)
(H : f · h = g · h) (w : Ccolim E, e) (H' : CoequalizerArrow E · w = h) :
w = CoequalizerOut E e h H.
Proof.
apply path_to_ctr.
use two_rec_dep.
- set (X := colimInCommutes E One Two (ii1 tt)).
apply (maponpaths (λ h : _, h · w)) in X.
use (pathscomp0 (!X)); rewrite <- assoc.
change (dmor _ _) with f.
change (coconeIn _ _) with (f · h).
apply cancel_precomposition, H'.
- apply H'.
Qed.

Definition isCoequalizer_Coequalizer {a b : C} {f g : Ca, b} (E : Coequalizer f g) :
isCoequalizer f g (CoequalizerObject E) (CoequalizerArrow E)
(CoequalizerArrowEq E).
Proof.
apply make_isCoequalizer.
intros e h H.
use (unique_exists (CoequalizerOut E e h H)).
- exact (CoequalizerArrowComm E e h H).
- intros y. apply hs.
- intros y t. cbn in t.
use CoequalizerOutUnique.
exact t.
Qed.

## Coequalizers to coequalizers

Definition identity_is_Coequalizer_input {a b : C} {f g : Ca, b} (E : Coequalizer f g) :
total2 (fun hk : Ccolim E, colim ECoequalizerArrow E · hk = CoequalizerArrow E).
Proof.
use tpair.
exact (identity _).
apply id_right.
Defined.

Lemma CoequalizerEndo_is_identity {a b : C} {f g : Ca, b} (E : Coequalizer f g)
(k : Ccolim E, colim E) (kH :CoequalizerArrow E · k = CoequalizerArrow E) :
identity (colim E) = k.
Proof.
apply colim_endo_is_identity.
unfold colimIn.
use two_rec_dep; cbn.
+ set (X := (coconeInCommutes (colimCocone E) One Two (ii1 tt))).
use (pathscomp0 (! (maponpaths (λ h' : _, h' · k) X))).
use (pathscomp0 _ X).
rewrite <- assoc. apply cancel_precomposition.
apply kH.
+ apply kH.
Qed.

Definition from_Coequalizer_to_Coequalizer {a b : C} {f g : Ca, b} (E1 E2 : Coequalizer f g) :
Ccolim E1, colim E2.
Proof.
apply (CoequalizerOut E1 (colim E2) (CoequalizerArrow E2)).
exact (CoequalizerArrowEq E2).
Defined.

Lemma are_inverses_from_Coequalizer_to_Coequalizer {a b : C} {f g : Ca, b}
(E1 E2 : Coequalizer f g) :
is_inverse_in_precat (from_Coequalizer_to_Coequalizer E2 E1)
(from_Coequalizer_to_Coequalizer E1 E2).
Proof.
split; apply pathsinv0.
- apply CoequalizerEndo_is_identity.
rewrite assoc.
unfold from_Coequalizer_to_Coequalizer.
repeat rewrite CoequalizerArrowComm.
apply idpath.
- apply CoequalizerEndo_is_identity.
rewrite assoc.
unfold from_Coequalizer_to_Coequalizer.
repeat rewrite CoequalizerArrowComm.
apply idpath.
Qed.

Lemma isiso_from_Coequalizer_to_Coequalizer {a b : C} {f g : Ca, b} (E1 E2 : Coequalizer f g) :
is_iso (from_Coequalizer_to_Coequalizer E1 E2).
Proof.
apply (is_iso_qinv _ (from_Coequalizer_to_Coequalizer E2 E1)).
apply are_inverses_from_Coequalizer_to_Coequalizer.
Qed.

Definition iso_from_Coequalizer_to_Coequalizer {a b : C} {f g : Ca, b}
(E1 E2 : Coequalizer f g) : iso (colim E1) (colim E2) :=
tpair _ _ (isiso_from_Coequalizer_to_Coequalizer E1 E2).

Lemma inv_from_iso_iso_from_Pullback {a b : C} {f g : Ca , b} (E1 E2 : Coequalizer f g):
inv_from_iso (iso_from_Coequalizer_to_Coequalizer E1 E2) =
from_Coequalizer_to_Coequalizer E2 E1.
Proof.
apply pathsinv0.
apply inv_iso_unique'.
apply (pr1 (are_inverses_from_Coequalizer_to_Coequalizer E2 E1)).
Qed.

## Connections to other colimits

Lemma Coequalizers_from_Colims : Colims C Coequalizers.
Proof.
intros H a b f g. apply H.
Defined.

End def_coequalizers.

# Definitions coincide

In this section we show that the definition of coequalizer as a colimit coincides with the direct definition.
Section coequalizers_coincide.

Variable C : precategory.
Variable hs: has_homsets C.

## isCoequalizers

Lemma equiv_isCoequalizer1 {a b : C} {f g : Ca, b} (e : C) (h : Cb, e) (H : f · h = g · h) :
limits.coequalizers.isCoequalizer f g h H isCoequalizer C f g e h H.
Proof.
intros X.
set (E := limits.coequalizers.make_Coequalizer f g h H X).
use (make_isCoequalizer C hs).
intros e' h' H'.
use (unique_exists (limits.coequalizers.CoequalizerOut E e' h' H')).
- exact (limits.coequalizers.CoequalizerCommutes E e' h' H').
- intros y. apply hs.
- intros y T. cbn in T.
use (limits.coequalizers.CoequalizerOutsEq E).
use (pathscomp0 T).
exact (!(limits.coequalizers.CoequalizerCommutes E e' h' H')).
Qed.

Lemma equiv_isCoequalizer2 {a b : C} (f g : Ca, b) (e : C) (h : Cb, e) (H : f · h = g · h) :
limits.coequalizers.isCoequalizer f g h H <- isCoequalizer C f g e h H.
Proof.
intros X.
set (E := make_Coequalizer C f g e h H X).
intros e' h' H'.
use (unique_exists (CoequalizerOut C E e' h' H')).
- exact (CoequalizerArrowComm C E e' h' H').
- intros y. apply hs.
- intros y T. cbn in T.
use (CoequalizerOutUnique C E).
exact T.
Qed.

## Coequalizers

Definition equiv_Coequalizer1 {a b : C} (f g : Ca, b) :
limits.coequalizers.Coequalizer f g Coequalizer C f g.
Proof.
intros E.
exact (make_Coequalizer
C f g _ _ _
(equiv_isCoequalizer1
(limits.coequalizers.CoequalizerObject E)
(limits.coequalizers.CoequalizerArrow E)
(limits.coequalizers.CoequalizerEqAr E)
(limits.coequalizers.isCoequalizer_Coequalizer E))).
Defined.

Definition equiv_Coequalizer2 {a b : C} (f g : Ca, b) :
limits.coequalizers.Coequalizer f g <- Coequalizer C f g.
Proof.
intros E.
exact (@limits.coequalizers.make_Coequalizer
C a b (CoequalizerObject C E) f g
(CoequalizerArrow C E)
(CoequalizerArrowEq C E)
(@equiv_isCoequalizer2
a b f g (CoequalizerObject C E)
(CoequalizerArrow C E)
(CoequalizerArrowEq C E)
(isCoequalizer_Coequalizer C hs E))).
Defined.

End coequalizers_coincide.