Library UniMath.CategoryTheory.limits.coequalizers
- Proof that the coequalizer arrow is epi (CoequalizerArrowisEpi)
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Section def_coequalizers.
Context {C : precategory}.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Section def_coequalizers.
Context {C : precategory}.
Definition and construction of isCoequalizer.
Definition isCoequalizer {x y z : C} (f g : x --> y) (e : y --> z)
(H : f · e = g · e) : UU :=
∏ (w : C) (h : y --> w) (H : f · h = g · h),
∃! φ : z --> w, e · φ = h.
Definition make_isCoequalizer {y z w : C} (f g : y --> z) (e : z --> w)
(H : f · e = g · e) :
(∏ (w0 : C) (h : z --> w0) (H' : f · h = g · h),
∃! ψ : w --> w0, e · ψ = h) -> isCoequalizer f g e H.
Show proof.
Lemma isaprop_isCoequalizer {y z w : C} (f g : y --> z) (e : z --> w)
(H : f · e = g · e) :
isaprop (isCoequalizer f g e H).
Show proof.
Lemma isCoequalizer_path {hs : has_homsets C} {x y z : C} {f g : x --> y} {e : y --> z}
{H H' : f · e = g · e} (iC : isCoequalizer f g e H) :
isCoequalizer f g e H'.
Show proof.
(H : f · e = g · e) : UU :=
∏ (w : C) (h : y --> w) (H : f · h = g · h),
∃! φ : z --> w, e · φ = h.
Definition make_isCoequalizer {y z w : C} (f g : y --> z) (e : z --> w)
(H : f · e = g · e) :
(∏ (w0 : C) (h : z --> w0) (H' : f · h = g · h),
∃! ψ : w --> w0, e · ψ = h) -> isCoequalizer f g e H.
Show proof.
Lemma isaprop_isCoequalizer {y z w : C} (f g : y --> z) (e : z --> w)
(H : f · e = g · e) :
isaprop (isCoequalizer f g e H).
Show proof.
Lemma isCoequalizer_path {hs : has_homsets C} {x y z : C} {f g : x --> y} {e : y --> z}
{H H' : f · e = g · e} (iC : isCoequalizer f g e H) :
isCoequalizer f g e H'.
Show proof.
use make_isCoequalizer.
intros w0 h H'0.
use unique_exists.
- exact (pr1 (pr1 (iC w0 h H'0))).
- exact (pr2 (pr1 (iC w0 h H'0))).
- intros y0. apply hs.
- intros y0 X. exact (base_paths _ _ (pr2 (iC w0 h H'0) (tpair _ y0 X))).
intros w0 h H'0.
use unique_exists.
- exact (pr1 (pr1 (iC w0 h H'0))).
- exact (pr2 (pr1 (iC w0 h H'0))).
- intros y0. apply hs.
- intros y0 X. exact (base_paths _ _ (pr2 (iC w0 h H'0) (tpair _ y0 X))).
Proves that the arrow from the coequalizer object with the right
commutativity property is unique.
Lemma isCoequalizerOutUnique {y z w: C} (f g : y --> z) (e : z --> w)
(H : f · e = g · e) (E : isCoequalizer f g e H)
(w0 : C) (h : z --> w0) (H' : f · h = g · h)
(φ : w --> w0) (H'' : e · φ = h) :
φ = (pr1 (pr1 (E w0 h H'))).
Show proof.
(H : f · e = g · e) (E : isCoequalizer f g e H)
(w0 : C) (h : z --> w0) (H' : f · h = g · h)
(φ : w --> w0) (H'' : e · φ = h) :
φ = (pr1 (pr1 (E w0 h H'))).
Show proof.
set (T := tpair (fun ψ : w --> w0 => e · ψ = h) φ H'').
set (T' := pr2 (E w0 h H') T).
apply (base_paths _ _ T').
set (T' := pr2 (E w0 h H') T).
apply (base_paths _ _ T').
Definition and construction of coequalizers.
Definition Coequalizer {y z : C} (f g : y --> z) : UU :=
∑ e : (∑ w : C, z --> w),
(∑ H : f · (pr2 e) = g · (pr2 e), isCoequalizer f g (pr2 e) H).
Definition make_Coequalizer {y z w : C} (f g : y --> z) (e : z --> w)
(H : f · e = g · e) (isE : isCoequalizer f g e H) :
Coequalizer f g.
Show proof.
∑ e : (∑ w : C, z --> w),
(∑ H : f · (pr2 e) = g · (pr2 e), isCoequalizer f g (pr2 e) H).
Definition make_Coequalizer {y z w : C} (f g : y --> z) (e : z --> w)
(H : f · e = g · e) (isE : isCoequalizer f g e H) :
Coequalizer f g.
Show proof.
Coequalizers in precategories.
Definition Coequalizers := ∏ (y z : C) (f g : y --> z),
Coequalizer f g.
Definition hasCoequalizers := ∏ (y z : C) (f g : y --> z),
ishinh (Coequalizer f g).
Coequalizer f g.
Definition hasCoequalizers := ∏ (y z : C) (f g : y --> z),
ishinh (Coequalizer f g).
Returns the coequalizer object.
Definition CoequalizerObject {y z : C} {f g : y --> z} (E : Coequalizer f g) :
C := pr1 (pr1 E).
Coercion CoequalizerObject : Coequalizer >-> ob.
C := pr1 (pr1 E).
Coercion CoequalizerObject : Coequalizer >-> ob.
Returns the coequalizer arrow.
Definition CoequalizerArrow {y z : C} {f g : y --> z} (E : Coequalizer f g) :
C⟦z, E⟧ := pr2 (pr1 E).
C⟦z, E⟧ := pr2 (pr1 E).
The equality on morphisms that coequalizers must satisfy.
Definition CoequalizerEqAr {y z : C} {f g : y --> z} (E : Coequalizer f g) :
f · CoequalizerArrow E = g · CoequalizerArrow E := pr1 (pr2 E).
f · CoequalizerArrow E = g · CoequalizerArrow E := pr1 (pr2 E).
Returns the property isCoequalizer from Coequalizer.
Definition isCoequalizer_Coequalizer {y z : C} {f g : y --> z}
(E : Coequalizer f g) :
isCoequalizer f g (CoequalizerArrow E) (CoequalizerEqAr E) := pr2 (pr2 E).
(E : Coequalizer f g) :
isCoequalizer f g (CoequalizerArrow E) (CoequalizerEqAr E) := pr2 (pr2 E).
Every morphism which satisfy the coequalizer equality on morphism factors
uniquely through the CoequalizerArrow.
Definition CoequalizerOut {y z : C} {f g : y --> z} (E : Coequalizer f g)
(w : C) (h : z --> w) (H : f · h = g · h) :
C⟦E, w⟧ := pr1 (pr1 (isCoequalizer_Coequalizer E w h H)).
Lemma CoequalizerCommutes {y z : C} {f g : y --> z} (E : Coequalizer f g)
(w : C) (h : z --> w) (H : f · h = g · h) :
(CoequalizerArrow E) · (CoequalizerOut E w h H) = h.
Show proof.
Lemma isCoequalizerOutsEq {y z w: C} {f g : y --> z} {e : z --> w}
{H : f · e = g · e} (E : isCoequalizer f g e H)
{w0 : C} (φ1 φ2: w --> w0) (H' : e · φ1 = e · φ2) : φ1 = φ2.
Show proof.
Lemma CoequalizerOutsEq {y z: C} {f g : y --> z} (E : Coequalizer f g)
{w : C} (φ1 φ2: C⟦E, w⟧)
(H' : (CoequalizerArrow E) · φ1 = (CoequalizerArrow E) · φ2) :
φ1 = φ2.
Show proof.
Lemma CoequalizerOutComp {y z : C} {f g : y --> z} (CE : Coequalizer f g) {w w' : C}
(h1 : z --> w) (h2 : w --> w')
(H1 : f · (h1 · h2) = g · (h1 · h2)) (H2 : f · h1 = g · h1) :
CoequalizerOut CE w' (h1 · h2) H1 = CoequalizerOut CE w h1 H2 · h2.
Show proof.
(w : C) (h : z --> w) (H : f · h = g · h) :
C⟦E, w⟧ := pr1 (pr1 (isCoequalizer_Coequalizer E w h H)).
Lemma CoequalizerCommutes {y z : C} {f g : y --> z} (E : Coequalizer f g)
(w : C) (h : z --> w) (H : f · h = g · h) :
(CoequalizerArrow E) · (CoequalizerOut E w h H) = h.
Show proof.
Lemma isCoequalizerOutsEq {y z w: C} {f g : y --> z} {e : z --> w}
{H : f · e = g · e} (E : isCoequalizer f g e H)
{w0 : C} (φ1 φ2: w --> w0) (H' : e · φ1 = e · φ2) : φ1 = φ2.
Show proof.
assert (H'1 : f · e · φ1 = g · e · φ1).
rewrite H. apply idpath.
set (E' := make_Coequalizer _ _ _ _ E).
repeat rewrite <- assoc in H'1.
set (E'ar := CoequalizerOut E' w0 (e · φ1) H'1).
intermediate_path E'ar.
apply isCoequalizerOutUnique. apply idpath.
apply pathsinv0. apply isCoequalizerOutUnique. apply pathsinv0. apply H'.
rewrite H. apply idpath.
set (E' := make_Coequalizer _ _ _ _ E).
repeat rewrite <- assoc in H'1.
set (E'ar := CoequalizerOut E' w0 (e · φ1) H'1).
intermediate_path E'ar.
apply isCoequalizerOutUnique. apply idpath.
apply pathsinv0. apply isCoequalizerOutUnique. apply pathsinv0. apply H'.
Lemma CoequalizerOutsEq {y z: C} {f g : y --> z} (E : Coequalizer f g)
{w : C} (φ1 φ2: C⟦E, w⟧)
(H' : (CoequalizerArrow E) · φ1 = (CoequalizerArrow E) · φ2) :
φ1 = φ2.
Show proof.
Lemma CoequalizerOutComp {y z : C} {f g : y --> z} (CE : Coequalizer f g) {w w' : C}
(h1 : z --> w) (h2 : w --> w')
(H1 : f · (h1 · h2) = g · (h1 · h2)) (H2 : f · h1 = g · h1) :
CoequalizerOut CE w' (h1 · h2) H1 = CoequalizerOut CE w h1 H2 · h2.
Show proof.
use CoequalizerOutsEq. rewrite CoequalizerCommutes. rewrite assoc.
rewrite CoequalizerCommutes. apply idpath.
rewrite CoequalizerCommutes. apply idpath.
Morphisms between coequalizer objects with the right commutativity
equalities.
Definition identity_is_CoequalizerOut {y z : C} {f g : y --> z}
(E : Coequalizer f g) :
∑ φ : C⟦E, E⟧, (CoequalizerArrow E) · φ = (CoequalizerArrow E).
Show proof.
Lemma CoequalizerEndo_is_identity {y z : C} {f g : y --> z}
{E : Coequalizer f g} (φ : C⟦E, E⟧)
(H : (CoequalizerArrow E) · φ = CoequalizerArrow E) :
identity E = φ.
Show proof.
Definition from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z}
(E E': Coequalizer f g) : C⟦E, E'⟧.
Show proof.
Lemma are_inverses_from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z}
{E E': Coequalizer f g} :
is_inverse_in_precat (from_Coequalizer_to_Coequalizer E E')
(from_Coequalizer_to_Coequalizer E' E).
Show proof.
Lemma isiso_from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z}
(E E' : Coequalizer f g) :
is_iso (from_Coequalizer_to_Coequalizer E E').
Show proof.
Definition iso_from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z}
(E E' : Coequalizer f g) : iso E E' :=
tpair _ _ (isiso_from_Coequalizer_to_Coequalizer E E').
(E : Coequalizer f g) :
∑ φ : C⟦E, E⟧, (CoequalizerArrow E) · φ = (CoequalizerArrow E).
Show proof.
Lemma CoequalizerEndo_is_identity {y z : C} {f g : y --> z}
{E : Coequalizer f g} (φ : C⟦E, E⟧)
(H : (CoequalizerArrow E) · φ = CoequalizerArrow E) :
identity E = φ.
Show proof.
set (H1 := tpair ((fun φ' : C⟦E, E⟧ => _ · φ' = _)) φ H).
assert (H2 : identity_is_CoequalizerOut E = H1).
- apply proofirrelevancecontr.
apply (isCoequalizer_Coequalizer E).
apply CoequalizerEqAr.
- apply (base_paths _ _ H2).
assert (H2 : identity_is_CoequalizerOut E = H1).
- apply proofirrelevancecontr.
apply (isCoequalizer_Coequalizer E).
apply CoequalizerEqAr.
- apply (base_paths _ _ H2).
Definition from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z}
(E E': Coequalizer f g) : C⟦E, E'⟧.
Show proof.
Lemma are_inverses_from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z}
{E E': Coequalizer f g} :
is_inverse_in_precat (from_Coequalizer_to_Coequalizer E E')
(from_Coequalizer_to_Coequalizer E' E).
Show proof.
split; apply pathsinv0; use CoequalizerEndo_is_identity;
rewrite assoc; unfold from_Coequalizer_to_Coequalizer;
repeat rewrite CoequalizerCommutes; apply idpath.
rewrite assoc; unfold from_Coequalizer_to_Coequalizer;
repeat rewrite CoequalizerCommutes; apply idpath.
Lemma isiso_from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z}
(E E' : Coequalizer f g) :
is_iso (from_Coequalizer_to_Coequalizer E E').
Show proof.
apply (is_iso_qinv _ (from_Coequalizer_to_Coequalizer E' E)).
apply are_inverses_from_Coequalizer_to_Coequalizer.
apply are_inverses_from_Coequalizer_to_Coequalizer.
Definition iso_from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z}
(E E' : Coequalizer f g) : iso E E' :=
tpair _ _ (isiso_from_Coequalizer_to_Coequalizer E E').
We prove that CoequalizerArrow is an epi.
Lemma CoequalizerArrowisEpi {y z : C} {f g : y --> z} (E : Coequalizer f g ) :
isEpi (CoequalizerArrow E).
Show proof.
Lemma CoequalizerArrowEpi {y z : C} {f g : y --> z} (E : Coequalizer f g ) :
Epi _ z E.
Show proof.
End def_coequalizers.
Definition Coequalizer_eq_ar
{C : category}
{x y c : C}
{f g : x --> y}
{e₁ e₂ : y --> c}
(p : e₁ = e₂)
(q₁ : f · e₁ = g · e₁)
(q₂ : f · e₂ = g · e₂)
(H : isCoequalizer f g e₁ q₁)
: isCoequalizer f g e₂ q₂.
Show proof.
Definition z_iso_to_Coequalizer
{C : category}
{x y c₂ : C}
{f g : x --> y}
(c₁ : Coequalizer f g)
(h : z_iso c₁ c₂)
: Coequalizer f g.
Show proof.
Definition z_iso_between_Coequalizer
{C : category}
{x y : C}
{f g : x --> y}
(c₁ c₂ : Coequalizer f g)
: z_iso c₁ c₂.
Show proof.
isEpi (CoequalizerArrow E).
Show proof.
Lemma CoequalizerArrowEpi {y z : C} {f g : y --> z} (E : Coequalizer f g ) :
Epi _ z E.
Show proof.
End def_coequalizers.
Definition Coequalizer_eq_ar
{C : category}
{x y c : C}
{f g : x --> y}
{e₁ e₂ : y --> c}
(p : e₁ = e₂)
(q₁ : f · e₁ = g · e₁)
(q₂ : f · e₂ = g · e₂)
(H : isCoequalizer f g e₁ q₁)
: isCoequalizer f g e₂ q₂.
Show proof.
Definition z_iso_to_Coequalizer
{C : category}
{x y c₂ : C}
{f g : x --> y}
(c₁ : Coequalizer f g)
(h : z_iso c₁ c₂)
: Coequalizer f g.
Show proof.
use make_Coequalizer.
- exact c₂.
- exact (CoequalizerArrow c₁ · h).
- abstract
(rewrite !assoc ;
rewrite CoequalizerEqAr ;
apply idpath).
- intros w k q.
use iscontraprop1.
+ abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
use subtypePath ; [ intro ; apply homset_property | ] ;
use (cancel_z_iso' h) ;
use (isCoequalizerOutsEq (pr22 c₁)) ;
rewrite !assoc ;
exact (pr2 φ₁ @ !(pr2 φ₂))).
+ refine (inv_from_z_iso h · CoequalizerOut c₁ w k q ,, _).
abstract
(rewrite !assoc' ;
rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)) ;
rewrite z_iso_inv_after_z_iso ;
rewrite id_left ;
rewrite CoequalizerCommutes ;
apply idpath).
- exact c₂.
- exact (CoequalizerArrow c₁ · h).
- abstract
(rewrite !assoc ;
rewrite CoequalizerEqAr ;
apply idpath).
- intros w k q.
use iscontraprop1.
+ abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
use subtypePath ; [ intro ; apply homset_property | ] ;
use (cancel_z_iso' h) ;
use (isCoequalizerOutsEq (pr22 c₁)) ;
rewrite !assoc ;
exact (pr2 φ₁ @ !(pr2 φ₂))).
+ refine (inv_from_z_iso h · CoequalizerOut c₁ w k q ,, _).
abstract
(rewrite !assoc' ;
rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)) ;
rewrite z_iso_inv_after_z_iso ;
rewrite id_left ;
rewrite CoequalizerCommutes ;
apply idpath).
Definition z_iso_between_Coequalizer
{C : category}
{x y : C}
{f g : x --> y}
(c₁ c₂ : Coequalizer f g)
: z_iso c₁ c₂.
Show proof.
use make_z_iso.
- exact (CoequalizerOut c₁ c₂ (CoequalizerArrow c₂) (CoequalizerEqAr c₂)).
- exact (CoequalizerOut c₂ c₁ (CoequalizerArrow c₁) (CoequalizerEqAr c₁)).
- split.
+ abstract
(use (isCoequalizerOutsEq (pr22 c₁)) ;
rewrite id_right ;
rewrite !assoc ;
rewrite !CoequalizerCommutes ;
apply idpath).
+ abstract
(use (isCoequalizerOutsEq (pr22 c₂)) ;
rewrite id_right ;
rewrite !assoc ;
rewrite !CoequalizerCommutes ;
apply idpath).
- exact (CoequalizerOut c₁ c₂ (CoequalizerArrow c₂) (CoequalizerEqAr c₂)).
- exact (CoequalizerOut c₂ c₁ (CoequalizerArrow c₁) (CoequalizerEqAr c₁)).
- split.
+ abstract
(use (isCoequalizerOutsEq (pr22 c₁)) ;
rewrite id_right ;
rewrite !assoc ;
rewrite !CoequalizerCommutes ;
apply idpath).
+ abstract
(use (isCoequalizerOutsEq (pr22 c₂)) ;
rewrite id_right ;
rewrite !assoc ;
rewrite !CoequalizerCommutes ;
apply idpath).
Make the C not implicit for Coequalizers
In univalent categories, equalizers are unique up to equality
Proposition isaprop_Coequalizer
{C : category}
(HC : is_univalent C)
{x y : C}
(f g : x --> y)
: isaprop (Coequalizer f g).
Show proof.
{C : category}
(HC : is_univalent C)
{x y : C}
(f g : x --> y)
: isaprop (Coequalizer f g).
Show proof.
use invproofirrelevance.
intros φ₁ φ₂.
use subtypePath.
{
intro.
use (isaprop_total2 (_ ,, _) (λ _, (_ ,, _))).
- apply homset_property.
- simpl.
repeat (use impred ; intro).
apply isapropiscontr.
}
use total2_paths_f.
- use (isotoid _ HC).
use z_iso_between_Coequalizer.
- rewrite transportf_isotoid' ; cbn.
apply CoequalizerCommutes.
intros φ₁ φ₂.
use subtypePath.
{
intro.
use (isaprop_total2 (_ ,, _) (λ _, (_ ,, _))).
- apply homset_property.
- simpl.
repeat (use impred ; intro).
apply isapropiscontr.
}
use total2_paths_f.
- use (isotoid _ HC).
use z_iso_between_Coequalizer.
- rewrite transportf_isotoid' ; cbn.
apply CoequalizerCommutes.
A reflexive coequalizer is a coequalizer of two morphisms that
have a common section. Reflexive coequalizers occur in the
study of colimits of the Eilenberg-Moore category. More
specifically, if a monad `M` preserves a class of colimits,
then the Eilenberg-Moore category has such colimits. However,
often monads do not preserve all colimits, but only reflexive
coequalizers. The nice thing about reflexive coequalizers is
that an Eilenberg-Moore category over a cocomplete category
is itself cocomplete if and only if it has reflexive
coequalizers. As such, it suffices to check whether a monad
preserves reflexive coequalizers in order to guarantee the
cocompleteness of the Eilenberg-Moore category.
Definition reflexive_coequalizers
(C : category)
: UU
:= ∏ (x y : C)
(f g : x --> y)
(h : y --> x)
(pf : h · f = identity _)
(pg : h · g = identity _),
Coequalizer f g.
(C : category)
: UU
:= ∏ (x y : C)
(f g : x --> y)
(h : y --> x)
(pf : h · f = identity _)
(pg : h · g = identity _),
Coequalizer f g.
If a category has both reflexive coequalizers and binary
coproducts, then it also has coequalizers.
Section CoequalizersFromReflexiveCoequalizers.
Context {C : category}
(RC : reflexive_coequalizers C)
(BCC : BinCoproducts C).
Section CoequalizersFromReflexive.
Context {x y : C}
(f g : x --> y).
Let xy : BinCoproduct x y := BCC x y.
Let ι₁ : x --> xy := BinCoproductIn1 xy.
Let ι₂ : y --> xy := BinCoproductIn2 xy.
Definition coequalizers_from_reflexive_left_map
: xy --> y
:= BinCoproductArrow xy f (identity _).
Definition coequalizers_from_reflexive_right_map
: xy --> y
:= BinCoproductArrow xy g (identity _).
Let ℓ : xy --> y := coequalizers_from_reflexive_left_map.
Let ρ : xy --> y := coequalizers_from_reflexive_right_map.
Lemma coequalizers_from_reflexive_left_map_eq
: ι₂ · ℓ = identity y.
Show proof.
Lemma coequalizers_from_reflexive_right_map_eq
: ι₂ · ρ = identity y.
Show proof.
Definition coequalizers_from_reflexive_ob
: Coequalizer ℓ ρ
:= RC _ _
ℓ ρ
ι₂
coequalizers_from_reflexive_left_map_eq
coequalizers_from_reflexive_right_map_eq.
Proposition coequalizers_from_reflexive_eq
: f · CoequalizerArrow coequalizers_from_reflexive_ob
=
g · CoequalizerArrow coequalizers_from_reflexive_ob.
Show proof.
Section UMP.
Context {z : C}
(h : y --> z)
(p : f · h = g · h).
Proposition coequalizer_from_reflexive_unique
: isaprop
(∑ φ, CoequalizerArrow coequalizers_from_reflexive_ob · φ = h).
Show proof.
Definition coequalizer_from_reflexive_ump
: coequalizers_from_reflexive_ob --> z.
Show proof.
Proposition coequalizer_from_reflexive_ump_eq
: CoequalizerArrow coequalizers_from_reflexive_ob
· coequalizer_from_reflexive_ump
=
h.
Show proof.
End UMP.
Definition coequalizer_from_reflexive
: Coequalizer f g.
Show proof.
Definition coequalizers_from_reflexive
: Coequalizers C
:= λ x y f g, coequalizer_from_reflexive f g.
End CoequalizersFromReflexiveCoequalizers.
Context {C : category}
(RC : reflexive_coequalizers C)
(BCC : BinCoproducts C).
Section CoequalizersFromReflexive.
Context {x y : C}
(f g : x --> y).
Let xy : BinCoproduct x y := BCC x y.
Let ι₁ : x --> xy := BinCoproductIn1 xy.
Let ι₂ : y --> xy := BinCoproductIn2 xy.
Definition coequalizers_from_reflexive_left_map
: xy --> y
:= BinCoproductArrow xy f (identity _).
Definition coequalizers_from_reflexive_right_map
: xy --> y
:= BinCoproductArrow xy g (identity _).
Let ℓ : xy --> y := coequalizers_from_reflexive_left_map.
Let ρ : xy --> y := coequalizers_from_reflexive_right_map.
Lemma coequalizers_from_reflexive_left_map_eq
: ι₂ · ℓ = identity y.
Show proof.
Lemma coequalizers_from_reflexive_right_map_eq
: ι₂ · ρ = identity y.
Show proof.
Definition coequalizers_from_reflexive_ob
: Coequalizer ℓ ρ
:= RC _ _
ℓ ρ
ι₂
coequalizers_from_reflexive_left_map_eq
coequalizers_from_reflexive_right_map_eq.
Proposition coequalizers_from_reflexive_eq
: f · CoequalizerArrow coequalizers_from_reflexive_ob
=
g · CoequalizerArrow coequalizers_from_reflexive_ob.
Show proof.
pose (maponpaths
(λ z, BinCoproductIn1 _ · z)
(CoequalizerEqAr coequalizers_from_reflexive_ob))
as p.
unfold ℓ, ρ in p.
unfold coequalizers_from_reflexive_left_map in p.
unfold coequalizers_from_reflexive_right_map in p.
rewrite !assoc in p.
rewrite !BinCoproductIn1Commutes in p.
exact p.
(λ z, BinCoproductIn1 _ · z)
(CoequalizerEqAr coequalizers_from_reflexive_ob))
as p.
unfold ℓ, ρ in p.
unfold coequalizers_from_reflexive_left_map in p.
unfold coequalizers_from_reflexive_right_map in p.
rewrite !assoc in p.
rewrite !BinCoproductIn1Commutes in p.
exact p.
Section UMP.
Context {z : C}
(h : y --> z)
(p : f · h = g · h).
Proposition coequalizer_from_reflexive_unique
: isaprop
(∑ φ, CoequalizerArrow coequalizers_from_reflexive_ob · φ = h).
Show proof.
use invproofirrelevance.
intros φ₁ φ₂.
use subtypePath.
{
intro.
apply homset_property.
}
use CoequalizerOutsEq.
exact (pr2 φ₁ @ !(pr2 φ₂)).
intros φ₁ φ₂.
use subtypePath.
{
intro.
apply homset_property.
}
use CoequalizerOutsEq.
exact (pr2 φ₁ @ !(pr2 φ₂)).
Definition coequalizer_from_reflexive_ump
: coequalizers_from_reflexive_ob --> z.
Show proof.
use (CoequalizerOut coequalizers_from_reflexive_ob z h).
abstract
(use BinCoproductArrowsEq ;
unfold ℓ, ρ ;
unfold coequalizers_from_reflexive_left_map ;
unfold coequalizers_from_reflexive_right_map ;
rewrite !assoc ;
rewrite ?BinCoproductIn1Commutes ;
rewrite ?BinCoproductIn2Commutes ;
[ exact p | apply idpath ]).
abstract
(use BinCoproductArrowsEq ;
unfold ℓ, ρ ;
unfold coequalizers_from_reflexive_left_map ;
unfold coequalizers_from_reflexive_right_map ;
rewrite !assoc ;
rewrite ?BinCoproductIn1Commutes ;
rewrite ?BinCoproductIn2Commutes ;
[ exact p | apply idpath ]).
Proposition coequalizer_from_reflexive_ump_eq
: CoequalizerArrow coequalizers_from_reflexive_ob
· coequalizer_from_reflexive_ump
=
h.
Show proof.
End UMP.
Definition coequalizer_from_reflexive
: Coequalizer f g.
Show proof.
use make_Coequalizer.
- exact coequalizers_from_reflexive_ob.
- exact (CoequalizerArrow coequalizers_from_reflexive_ob).
- exact coequalizers_from_reflexive_eq.
- intros z h p.
use iscontraprop1.
+ exact (coequalizer_from_reflexive_unique h).
+ simple refine (_ ,, _).
* exact (coequalizer_from_reflexive_ump h p).
* exact (coequalizer_from_reflexive_ump_eq h p).
End CoequalizersFromReflexive.- exact coequalizers_from_reflexive_ob.
- exact (CoequalizerArrow coequalizers_from_reflexive_ob).
- exact coequalizers_from_reflexive_eq.
- intros z h p.
use iscontraprop1.
+ exact (coequalizer_from_reflexive_unique h).
+ simple refine (_ ,, _).
* exact (coequalizer_from_reflexive_ump h p).
* exact (coequalizer_from_reflexive_ump_eq h p).
Definition coequalizers_from_reflexive
: Coequalizers C
:= λ x y f g, coequalizer_from_reflexive f g.
End CoequalizersFromReflexiveCoequalizers.