Library UniMath.CategoryTheory.Limits.Equalizers
- Definition
- Proof that the equalizer arrow is monic (EqualizerArrowisMonic)
- Proof that the equalizer arrow of equal morphism is an isomorphism (z_iso_Equalizer_of_same_map)
- Alternative universal property
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
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.Monics.
Require Import UniMath.CategoryTheory.Retracts.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
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.Monics.
Require Import UniMath.CategoryTheory.Retracts.
Definition and construction of isEqualizer.
Definition isEqualizer {x y z : C} (f g : y --> z) (e : x --> y)
(H : e · f = e · g) : UU :=
∏ (w : C) (h : w --> y) (H : h · f = h · g),
∃! φ : w --> x, φ · e = h.
Definition make_isEqualizer {x y z : C} (f g : y --> z) (e : x --> y)
(H : e · f = e · g) :
(∏ (w : C) (h : w --> y) (H' : h · f = h · g),
∃! ψ : w --> x, ψ · e = h) -> isEqualizer f g e H.
Show proof.
Lemma isaprop_isEqualizer {x y z : C} (f g : y --> z) (e : x --> y)
(H : e · f = e · g) :
isaprop (isEqualizer f g e H).
Show proof.
Lemma isEqualizer_path {hs : has_homsets C} {x y z : C} {f g : y --> z} {e : x --> y}
{H H' : e · f = e · g} (iC : isEqualizer f g e H) :
isEqualizer f g e H'.
Show proof.
(H : e · f = e · g) : UU :=
∏ (w : C) (h : w --> y) (H : h · f = h · g),
∃! φ : w --> x, φ · e = h.
Definition make_isEqualizer {x y z : C} (f g : y --> z) (e : x --> y)
(H : e · f = e · g) :
(∏ (w : C) (h : w --> y) (H' : h · f = h · g),
∃! ψ : w --> x, ψ · e = h) -> isEqualizer f g e H.
Show proof.
Lemma isaprop_isEqualizer {x y z : C} (f g : y --> z) (e : x --> y)
(H : e · f = e · g) :
isaprop (isEqualizer f g e H).
Show proof.
Lemma isEqualizer_path {hs : has_homsets C} {x y z : C} {f g : y --> z} {e : x --> y}
{H H' : e · f = e · g} (iC : isEqualizer f g e H) :
isEqualizer f g e H'.
Show proof.
use make_isEqualizer.
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 to the equalizer object with the right
commutativity property is unique.
Lemma isEqualizerInUnique {x y z : C} (f g : y --> z) (e : x --> y)
(H : e · f = e · g) (E : isEqualizer f g e H)
(w : C) (h : w --> y) (H' : h · f = h · g)
(φ : w --> x) (H'' : φ · e = h) :
φ = (pr1 (pr1 (E w h H'))).
Show proof.
(H : e · f = e · g) (E : isEqualizer f g e H)
(w : C) (h : w --> y) (H' : h · f = h · g)
(φ : w --> x) (H'' : φ · e = h) :
φ = (pr1 (pr1 (E w h H'))).
Show proof.
set (T := tpair (fun ψ : w --> x => ψ · e = h) φ H'').
set (T' := pr2 (E w h H') T).
apply (base_paths _ _ T').
set (T' := pr2 (E w h H') T).
apply (base_paths _ _ T').
Definition and construction of equalizers.
Definition Equalizer {y z : C} (f g : y --> z) : UU :=
∑ e : (∑ w : C, w --> y),
(∑ H : (pr2 e) · f = (pr2 e) · g, isEqualizer f g (pr2 e) H).
Definition make_Equalizer {x y z : C} (f g : y --> z) (e : x --> y)
(H : e · f = e · g) (isE : isEqualizer f g e H) :
Equalizer f g.
Show proof.
∑ e : (∑ w : C, w --> y),
(∑ H : (pr2 e) · f = (pr2 e) · g, isEqualizer f g (pr2 e) H).
Definition make_Equalizer {x y z : C} (f g : y --> z) (e : x --> y)
(H : e · f = e · g) (isE : isEqualizer f g e H) :
Equalizer f g.
Show proof.
Equalizers in precategories.
Definition Equalizers : UU := ∏ (y z : C) (f g : y --> z), Equalizer f g.
Definition hasEqualizers : UU := ∏ (y z : C) (f g : y --> z),
ishinh (Equalizer f g).
Definition hasEqualizers : UU := ∏ (y z : C) (f g : y --> z),
ishinh (Equalizer f g).
Returns the equalizer object.
Definition EqualizerObject {y z : C} {f g : y --> z} (E : Equalizer f g) :
C := pr1 (pr1 E).
Coercion EqualizerObject : Equalizer >-> ob.
C := pr1 (pr1 E).
Coercion EqualizerObject : Equalizer >-> ob.
Returns the equalizer arrow.
The equality on morphisms that equalizers must satisfy.
Definition EqualizerEqAr {y z : C} {f g : y --> z} (E : Equalizer f g) :
EqualizerArrow E · f = EqualizerArrow E · g := pr1 (pr2 E).
EqualizerArrow E · f = EqualizerArrow E · g := pr1 (pr2 E).
Returns the property isEqualizer from Equalizer.
Definition isEqualizer_Equalizer {y z : C} {f g : y --> z}
(E : Equalizer f g) :
isEqualizer f g (EqualizerArrow E) (EqualizerEqAr E) := pr2 (pr2 E).
(E : Equalizer f g) :
isEqualizer f g (EqualizerArrow E) (EqualizerEqAr E) := pr2 (pr2 E).
Every morphism which satisfy the equalizer equality on morphism factors
uniquely through the EqualizerArrow.
Definition EqualizerIn {y z : C} {f g : y --> z} (E : Equalizer f g)
(w : C) (h : w --> y) (H : h · f = h · g) :
C⟦w, E⟧ := pr1 (pr1 (isEqualizer_Equalizer E w h H)).
Lemma EqualizerCommutes {y z : C} {f g : y --> z} (E : Equalizer f g)
(w : C) (h : w --> y) (H : h · f = h · g) :
(EqualizerIn E w h H) · (EqualizerArrow E) = h.
Show proof.
Lemma isEqualizerInsEq {x y z: C} {f g : y --> z} {e : x --> y}
{H : e · f = e · g} (E : isEqualizer f g e H)
{w : C} (φ1 φ2: w --> x) (H' : φ1 · e = φ2 · e) : φ1 = φ2.
Show proof.
Lemma EqualizerInsEq {y z: C} {f g : y --> z} (E : Equalizer f g)
{w : C} (φ1 φ2: C⟦w, E⟧)
(H' : φ1 · (EqualizerArrow E) = φ2 · (EqualizerArrow E)) : φ1 = φ2.
Show proof.
Lemma EqualizerInComp {y z : C} {f g : y --> z} (E : Equalizer f g) {x x' : C}
(h1 : x --> x') (h2 : x' --> y)
(H1 : h1 · h2 · f = h1 · h2 · g) (H2 : h2 · f = h2 · g) :
EqualizerIn E x (h1 · h2) H1 = h1 · EqualizerIn E x' h2 H2.
Show proof.
(w : C) (h : w --> y) (H : h · f = h · g) :
C⟦w, E⟧ := pr1 (pr1 (isEqualizer_Equalizer E w h H)).
Lemma EqualizerCommutes {y z : C} {f g : y --> z} (E : Equalizer f g)
(w : C) (h : w --> y) (H : h · f = h · g) :
(EqualizerIn E w h H) · (EqualizerArrow E) = h.
Show proof.
Lemma isEqualizerInsEq {x y z: C} {f g : y --> z} {e : x --> y}
{H : e · f = e · g} (E : isEqualizer f g e H)
{w : C} (φ1 φ2: w --> x) (H' : φ1 · e = φ2 · e) : φ1 = φ2.
Show proof.
assert (H'1 : φ1 · e · f = φ1 · e · g).
rewrite <- assoc. rewrite H. rewrite assoc. apply idpath.
set (E' := make_Equalizer _ _ _ _ E).
set (E'ar := EqualizerIn E' w (φ1 · e) H'1).
intermediate_path E'ar.
apply isEqualizerInUnique. apply idpath.
apply pathsinv0. apply isEqualizerInUnique. apply pathsinv0. apply H'.
rewrite <- assoc. rewrite H. rewrite assoc. apply idpath.
set (E' := make_Equalizer _ _ _ _ E).
set (E'ar := EqualizerIn E' w (φ1 · e) H'1).
intermediate_path E'ar.
apply isEqualizerInUnique. apply idpath.
apply pathsinv0. apply isEqualizerInUnique. apply pathsinv0. apply H'.
Lemma EqualizerInsEq {y z: C} {f g : y --> z} (E : Equalizer f g)
{w : C} (φ1 φ2: C⟦w, E⟧)
(H' : φ1 · (EqualizerArrow E) = φ2 · (EqualizerArrow E)) : φ1 = φ2.
Show proof.
Lemma EqualizerInComp {y z : C} {f g : y --> z} (E : Equalizer f g) {x x' : C}
(h1 : x --> x') (h2 : x' --> y)
(H1 : h1 · h2 · f = h1 · h2 · g) (H2 : h2 · f = h2 · g) :
EqualizerIn E x (h1 · h2) H1 = h1 · EqualizerIn E x' h2 H2.
Show proof.
use EqualizerInsEq. rewrite EqualizerCommutes.
rewrite <- assoc. rewrite EqualizerCommutes.
apply idpath.
rewrite <- assoc. rewrite EqualizerCommutes.
apply idpath.
Morphisms between equalizer objects with the right commutativity
equalities.
Definition identity_is_EqualizerIn {y z : C} {f g : y --> z}
(E : Equalizer f g) :
∑ φ : C⟦E, E⟧, φ · (EqualizerArrow E) = (EqualizerArrow E).
Show proof.
Lemma EqualizerEndo_is_identity {y z : C} {f g : y --> z} {E : Equalizer f g}
(φ : C⟦E, E⟧) (H : φ · (EqualizerArrow E) = EqualizerArrow E) :
identity E = φ.
Show proof.
Definition from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
(E E': Equalizer f g) : C⟦E, E'⟧.
Show proof.
Lemma are_inverses_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
{E E': Equalizer f g} :
is_inverse_in_precat (from_Equalizer_to_Equalizer E E')
(from_Equalizer_to_Equalizer E' E).
Show proof.
Lemma isiso_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
(E E' : Equalizer f g) :
is_iso (from_Equalizer_to_Equalizer E E').
Show proof.
Definition iso_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
(E E' : Equalizer f g) : iso E E' :=
tpair _ _ (isiso_from_Equalizer_to_Equalizer E E').
Lemma z_iso_from_Equalizer_to_Equalizer_inverses {y z : C} {f g : y --> z}
(E E' : Equalizer f g) :
is_inverse_in_precat (from_Equalizer_to_Equalizer E E') (from_Equalizer_to_Equalizer E' E).
Show proof.
Definition z_iso_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
(E E' : Equalizer f g) : z_iso E E'.
Show proof.
(E : Equalizer f g) :
∑ φ : C⟦E, E⟧, φ · (EqualizerArrow E) = (EqualizerArrow E).
Show proof.
Lemma EqualizerEndo_is_identity {y z : C} {f g : y --> z} {E : Equalizer f g}
(φ : C⟦E, E⟧) (H : φ · (EqualizerArrow E) = EqualizerArrow E) :
identity E = φ.
Show proof.
set (H1 := tpair ((fun φ' : C⟦E, E⟧ => φ' · _ = _)) φ H).
assert (H2 : identity_is_EqualizerIn E = H1).
- apply proofirrelevancecontr.
apply (isEqualizer_Equalizer E).
apply EqualizerEqAr.
- apply (base_paths _ _ H2).
assert (H2 : identity_is_EqualizerIn E = H1).
- apply proofirrelevancecontr.
apply (isEqualizer_Equalizer E).
apply EqualizerEqAr.
- apply (base_paths _ _ H2).
Definition from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
(E E': Equalizer f g) : C⟦E, E'⟧.
Show proof.
Lemma are_inverses_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
{E E': Equalizer f g} :
is_inverse_in_precat (from_Equalizer_to_Equalizer E E')
(from_Equalizer_to_Equalizer E' E).
Show proof.
split; apply pathsinv0; use EqualizerEndo_is_identity;
rewrite <- assoc; unfold from_Equalizer_to_Equalizer;
repeat rewrite EqualizerCommutes; apply idpath.
rewrite <- assoc; unfold from_Equalizer_to_Equalizer;
repeat rewrite EqualizerCommutes; apply idpath.
Lemma isiso_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
(E E' : Equalizer f g) :
is_iso (from_Equalizer_to_Equalizer E E').
Show proof.
apply (is_iso_qinv _ (from_Equalizer_to_Equalizer E' E)).
apply are_inverses_from_Equalizer_to_Equalizer.
apply are_inverses_from_Equalizer_to_Equalizer.
Definition iso_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
(E E' : Equalizer f g) : iso E E' :=
tpair _ _ (isiso_from_Equalizer_to_Equalizer E E').
Lemma z_iso_from_Equalizer_to_Equalizer_inverses {y z : C} {f g : y --> z}
(E E' : Equalizer f g) :
is_inverse_in_precat (from_Equalizer_to_Equalizer E E') (from_Equalizer_to_Equalizer E' E).
Show proof.
use make_is_inverse_in_precat.
- apply pathsinv0. use EqualizerEndo_is_identity.
rewrite <- assoc. unfold from_Equalizer_to_Equalizer. rewrite EqualizerCommutes.
rewrite EqualizerCommutes. apply idpath.
- apply pathsinv0. use EqualizerEndo_is_identity.
rewrite <- assoc. unfold from_Equalizer_to_Equalizer. rewrite EqualizerCommutes.
rewrite EqualizerCommutes. apply idpath.
- apply pathsinv0. use EqualizerEndo_is_identity.
rewrite <- assoc. unfold from_Equalizer_to_Equalizer. rewrite EqualizerCommutes.
rewrite EqualizerCommutes. apply idpath.
- apply pathsinv0. use EqualizerEndo_is_identity.
rewrite <- assoc. unfold from_Equalizer_to_Equalizer. rewrite EqualizerCommutes.
rewrite EqualizerCommutes. apply idpath.
Definition z_iso_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
(E E' : Equalizer f g) : z_iso E E'.
Show proof.
use make_z_iso.
- exact (from_Equalizer_to_Equalizer E E').
- exact (from_Equalizer_to_Equalizer E' E).
- exact (z_iso_from_Equalizer_to_Equalizer_inverses E E').
- exact (from_Equalizer_to_Equalizer E E').
- exact (from_Equalizer_to_Equalizer E' E).
- exact (z_iso_from_Equalizer_to_Equalizer_inverses E E').
Proof that the equalizer arrow is monic (EqualizerArrowisMonic)
Lemma EqualizerArrowisMonic {y z : C} {f g : y --> z} (E : Equalizer f g ) :
isMonic (EqualizerArrow E).
Show proof.
Lemma EqualizerArrowMonic {y z : C} {f g : y --> z} (E : Equalizer f g ) :
Monic _ E y.
Show proof.
Definition identity_asEqualizer {y z : C} (f : y --> z) : (Equalizer f f).
Show proof.
Lemma z_iso_Equalizer_of_same_map {y z : C} {f g : y --> z} (E : Equalizer f g) (p:f = g) : is_z_isomorphism (EqualizerArrow E).
Show proof.
End def_equalizers.
isMonic (EqualizerArrow E).
Show proof.
Lemma EqualizerArrowMonic {y z : C} {f g : y --> z} (E : Equalizer f g ) :
Monic _ E y.
Show proof.
Definition identity_asEqualizer {y z : C} (f : y --> z) : (Equalizer f f).
Show proof.
use make_Equalizer.
+ exact y.
+ exact (identity y).
+ apply idpath.
+ use make_isEqualizer.
intros x h p.
use unique_exists.
- exact h.
- use id_right.
- intro.
use homset_property.
- intros t t_tri.
rewrite <-(id_right t).
exact t_tri.
+ exact y.
+ exact (identity y).
+ apply idpath.
+ use make_isEqualizer.
intros x h p.
use unique_exists.
- exact h.
- use id_right.
- intro.
use homset_property.
- intros t t_tri.
rewrite <-(id_right t).
exact t_tri.
Lemma z_iso_Equalizer_of_same_map {y z : C} {f g : y --> z} (E : Equalizer f g) (p:f = g) : is_z_isomorphism (EqualizerArrow E).
Show proof.
induction p.
use (make_is_z_isomorphism _ (from_Equalizer_to_Equalizer (identity_asEqualizer f) E)).
use z_iso_from_Equalizer_to_Equalizer_inverses.
use (make_is_z_isomorphism _ (from_Equalizer_to_Equalizer (identity_asEqualizer f) E)).
use z_iso_from_Equalizer_to_Equalizer_inverses.
End def_equalizers.
Make the C not implicit for Equalizers
Section Equalizers'.
Context {C : category} {c d : ob C} (f g : C⟦c, d⟧).
Context (E : ob C) (h : E --> c) (H : h · f = h · g).
A map into an equalizer can be turned into a map into c
such that its composites with f and g are equal.
Definition postcomp_with_equalizer_mor (a : ob C) (j : a --> E) :
∑ (k : a --> c), (k · f = k · g).
Show proof.
Definition isEqualizer' : UU :=
∏ (a : ob C), isweq (postcomp_with_equalizer_mor a).
Definition isEqualizer'_weq (is : isEqualizer') :
∏ a, (a --> E) ≃ (∑ k : a --> c, (k · f = k · g)) :=
λ a, make_weq (postcomp_with_equalizer_mor a) (is a).
Lemma isaprop_isEqualizer' : isaprop isEqualizer'.
Show proof.
∑ (k : a --> c), (k · f = k · g).
Show proof.
Definition isEqualizer' : UU :=
∏ (a : ob C), isweq (postcomp_with_equalizer_mor a).
Definition isEqualizer'_weq (is : isEqualizer') :
∏ a, (a --> E) ≃ (∑ k : a --> c, (k · f = k · g)) :=
λ a, make_weq (postcomp_with_equalizer_mor a) (is a).
Lemma isaprop_isEqualizer' : isaprop isEqualizer'.
Show proof.
Can isEqualizer'_to_isEqualizer be generalized to arbitrary precategories?
Compare to isBinProduct'_to_isBinProduct.
Lemma isEqualizer'_to_isEqualizer :
isEqualizer' -> isEqualizer f g h H.
Show proof.
Lemma isEqualizer_to_isEqualizer' :
isEqualizer f g h H -> isEqualizer'.
Show proof.
Lemma isEqualizer'_weq_isEqualizer :
isEqualizer f g h H ≃ isEqualizer'.
Show proof.
End Equalizers'.
Definition isEqualizer_eq
{C : category}
{e x y : C}
{f g f' g' : x --> y}
{i i' : e --> x}
(p : i · f = i · g)
(q : i' · f' = i' · g')
(s₁ : f = f')
(s₂ : g = g')
(s₃ : i = i')
(He : isEqualizer f g i p)
: isEqualizer f' g' i' q.
Show proof.
isEqualizer' -> isEqualizer f g h H.
Show proof.
intros isEq' E' h' H'.
apply (@iscontrweqf (hfiber (isEqualizer'_weq isEq' _) (h',, H'))).
- cbn; unfold hfiber.
use weqfibtototal; intros j; cbn.
unfold postcomp_with_equalizer_mor.
apply subtypeInjectivity.
intro; apply C.
- apply weqproperty.
apply (@iscontrweqf (hfiber (isEqualizer'_weq isEq' _) (h',, H'))).
- cbn; unfold hfiber.
use weqfibtototal; intros j; cbn.
unfold postcomp_with_equalizer_mor.
apply subtypeInjectivity.
intro; apply C.
- apply weqproperty.
Lemma isEqualizer_to_isEqualizer' :
isEqualizer f g h H -> isEqualizer'.
Show proof.
intros isEq E'.
unfold postcomp_with_equalizer_mor.
unfold isweq, hfiber.
intros hH'.
apply (@iscontrweqf (∑ u : C ⟦ E', E ⟧, u · h = pr1 hH')).
- use weqfibtototal; intro; cbn.
apply invweq.
use subtypeInjectivity.
intro; apply C.
- exact (isEq E' (pr1 hH') (pr2 hH')).
unfold postcomp_with_equalizer_mor.
unfold isweq, hfiber.
intros hH'.
apply (@iscontrweqf (∑ u : C ⟦ E', E ⟧, u · h = pr1 hH')).
- use weqfibtototal; intro; cbn.
apply invweq.
use subtypeInjectivity.
intro; apply C.
- exact (isEq E' (pr1 hH') (pr2 hH')).
Lemma isEqualizer'_weq_isEqualizer :
isEqualizer f g h H ≃ isEqualizer'.
Show proof.
apply weqimplimpl.
- apply isEqualizer_to_isEqualizer'; assumption.
- apply isEqualizer'_to_isEqualizer; assumption.
- apply isaprop_isEqualizer.
- apply isaprop_isEqualizer'.
- apply isEqualizer_to_isEqualizer'; assumption.
- apply isEqualizer'_to_isEqualizer; assumption.
- apply isaprop_isEqualizer.
- apply isaprop_isEqualizer'.
End Equalizers'.
Definition isEqualizer_eq
{C : category}
{e x y : C}
{f g f' g' : x --> y}
{i i' : e --> x}
(p : i · f = i · g)
(q : i' · f' = i' · g')
(s₁ : f = f')
(s₂ : g = g')
(s₃ : i = i')
(He : isEqualizer f g i p)
: isEqualizer f' g' i' q.
Show proof.
intros w h r.
use iscontraprop1.
- abstract
(induction s₁, s₂, s₃ ;
apply (isapropifcontr (He w h r))).
- simple refine (_ ,, _).
+ refine (EqualizerIn (make_Equalizer _ _ _ _ He) _ h _).
abstract
(induction s₁, s₂ ;
exact r).
+ abstract
(cbn ;
induction s₁, s₂, s₃ ;
apply (EqualizerCommutes (make_Equalizer _ _ _ _ He))).
use iscontraprop1.
- abstract
(induction s₁, s₂, s₃ ;
apply (isapropifcontr (He w h r))).
- simple refine (_ ,, _).
+ refine (EqualizerIn (make_Equalizer _ _ _ _ He) _ h _).
abstract
(induction s₁, s₂ ;
exact r).
+ abstract
(cbn ;
induction s₁, s₂, s₃ ;
apply (EqualizerCommutes (make_Equalizer _ _ _ _ He))).
Equalizers are closed under iso
Definition isEqualizer_z_iso
{C : category}
{e₁ e₂ x y : C}
{f g : x --> y}
{p₁ : e₁ --> x}
{q₁ : p₁ · f = p₁ · g}
{p₂ : e₂ --> x}
{q₂ : p₂ · f = p₂ · g}
(H : isEqualizer f g p₁ q₁)
(h : z_iso e₂ e₁)
(r : p₂ = h · p₁)
: isEqualizer f g p₂ q₂.
Show proof.
{C : category}
{e₁ e₂ x y : C}
{f g : x --> y}
{p₁ : e₁ --> x}
{q₁ : p₁ · f = p₁ · g}
{p₂ : e₂ --> x}
{q₂ : p₂ · f = p₂ · g}
(H : isEqualizer f g p₁ q₁)
(h : z_iso e₂ e₁)
(r : p₂ = h · p₁)
: isEqualizer f g p₂ q₂.
Show proof.
intros a k s.
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
use subtypePath ; [ intro ; apply homset_property | ] ;
use (cancel_z_iso _ _ h) ;
use (isEqualizerInsEq H) ;
rewrite !assoc' ;
rewrite <- !r ;
exact (pr2 φ₁ @ !(pr2 φ₂))).
- refine (EqualizerIn (make_Equalizer _ _ _ _ H) _ k s · inv_from_z_iso h ,, _).
abstract
(rewrite r ;
rewrite !assoc' ;
rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)) ;
refine (maponpaths (λ z, _ · (z · _)) (z_iso_after_z_iso_inv h) @ _) ;
rewrite id_left ;
apply (EqualizerCommutes (make_Equalizer _ _ _ _ H))).
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
use subtypePath ; [ intro ; apply homset_property | ] ;
use (cancel_z_iso _ _ h) ;
use (isEqualizerInsEq H) ;
rewrite !assoc' ;
rewrite <- !r ;
exact (pr2 φ₁ @ !(pr2 φ₂))).
- refine (EqualizerIn (make_Equalizer _ _ _ _ H) _ k s · inv_from_z_iso h ,, _).
abstract
(rewrite r ;
rewrite !assoc' ;
rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)) ;
refine (maponpaths (λ z, _ · (z · _)) (z_iso_after_z_iso_inv h) @ _) ;
rewrite id_left ;
apply (EqualizerCommutes (make_Equalizer _ _ _ _ H))).
In univalent categories, equalizers are unique up to equality
Proposition isaprop_Equalizer
{C : category}
(HC : is_univalent C)
{x y : C}
(f g : x --> y)
: isaprop (Equalizer f g).
Show proof.
Lemma retract_is_equalizer
{C : category}
{a b : C}
(f : retraction b a)
: Equalizer (f · retraction_section f) (identity a).
Show proof.
{C : category}
(HC : is_univalent C)
{x y : C}
(f g : x --> y)
: isaprop (Equalizer 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_from_Equalizer_to_Equalizer.
- rewrite transportf_isotoid ; cbn.
apply EqualizerCommutes.
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_from_Equalizer_to_Equalizer.
- rewrite transportf_isotoid ; cbn.
apply EqualizerCommutes.
Lemma retract_is_equalizer
{C : category}
{a b : C}
(f : retraction b a)
: Equalizer (f · retraction_section f) (identity a).
Show proof.
use make_Equalizer.
- exact b.
- exact (retraction_section f).
- abstract (
refine (_ @ !id_right _);
refine (assoc _ _ _ @ _);
refine (maponpaths (λ x, x · _) (retraction_is_retraction f) @ _);
apply id_left
).
- apply make_isEqualizer.
intros d f' Hf'.
use unique_exists.
+ exact (f' · f).
+ abstract exact (assoc' _ _ _ @ Hf' @ id_right _).
+ abstract (
intro y;
apply homset_property
).
+ abstract (
intros g' Hg';
refine (!id_right _ @ _);
refine (!maponpaths _ (retraction_is_retraction f) @ _);
refine (assoc _ _ _ @ _);
apply (maponpaths (λ x, x · _));
exact Hg'
).
- exact b.
- exact (retraction_section f).
- abstract (
refine (_ @ !id_right _);
refine (assoc _ _ _ @ _);
refine (maponpaths (λ x, x · _) (retraction_is_retraction f) @ _);
apply id_left
).
- apply make_isEqualizer.
intros d f' Hf'.
use unique_exists.
+ exact (f' · f).
+ abstract exact (assoc' _ _ _ @ Hf' @ id_right _).
+ abstract (
intro y;
apply homset_property
).
+ abstract (
intros g' Hg';
refine (!id_right _ @ _);
refine (!maponpaths _ (retraction_is_retraction f) @ _);
refine (assoc _ _ _ @ _);
apply (maponpaths (λ x, x · _));
exact Hg'
).