Library UniMath.CategoryTheory.Limits.Zero
Direct definition of zero objects
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.
Require Import UniMath.CategoryTheory.opp_precat.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Section def_zero.
Variable C : category.
Definition isZero (b : C) : UU :=
(∏ a : C, iscontr (b --> a)) × (∏ a : C, iscontr (a --> b)).
Lemma isaprop_isZero (b : C) : isaprop (isZero b).
Show proof.
Definition Zero : UU := total2 (λ a, isZero a).
Definition ZeroObject (Z : Zero) : C := pr1 Z.
Coercion ZeroObject : Zero >-> ob.
Definition make_Zero (b : C) (H : isZero b) : Zero.
Show proof.
Definition make_isZero (b : C) (H : ∏ (a : C), iscontr (b --> a))
(H' : ∏ (a : C), iscontr (a --> b)) : isZero b.
Show proof.
Definition ZeroArrowFrom (Z : Zero) (b : C) : Z --> b := pr1 (pr1 (pr2 Z) b).
Definition ZeroArrowTo (Z : Zero) (b : C) : b --> Z := pr1 (pr2 (pr2 Z) b).
Lemma ArrowsToZero (Z : Zero) (b : C) (f g : b --> Z) : f = g.
Show proof.
Lemma ArrowsFromZero (Z : Zero) (b : C) (f g : Z --> b) : f = g.
Show proof.
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.
Require Import UniMath.CategoryTheory.opp_precat.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Section def_zero.
Variable C : category.
Definition isZero (b : C) : UU :=
(∏ a : C, iscontr (b --> a)) × (∏ a : C, iscontr (a --> b)).
Lemma isaprop_isZero (b : C) : isaprop (isZero b).
Show proof.
apply isapropdirprod.
- apply impred. intros t. apply isapropiscontr.
- apply impred. intros t. apply isapropiscontr.
- apply impred. intros t. apply isapropiscontr.
- apply impred. intros t. apply isapropiscontr.
Definition Zero : UU := total2 (λ a, isZero a).
Definition ZeroObject (Z : Zero) : C := pr1 Z.
Coercion ZeroObject : Zero >-> ob.
Definition make_Zero (b : C) (H : isZero b) : Zero.
Show proof.
exists b; exact H.
Definition make_isZero (b : C) (H : ∏ (a : C), iscontr (b --> a))
(H' : ∏ (a : C), iscontr (a --> b)) : isZero b.
Show proof.
Definition ZeroArrowFrom (Z : Zero) (b : C) : Z --> b := pr1 (pr1 (pr2 Z) b).
Definition ZeroArrowTo (Z : Zero) (b : C) : b --> Z := pr1 (pr2 (pr2 Z) b).
Lemma ArrowsToZero (Z : Zero) (b : C) (f g : b --> Z) : f = g.
Show proof.
Lemma ArrowsFromZero (Z : Zero) (b : C) (f g : Z --> b) : f = g.
Show proof.
For any pair of objects, there exists a unique arrow which factors
through the zero object
Definition ZeroArrow (Z : Zero) (a b : C) : C⟦a, b⟧ := (ZeroArrowTo Z a) · (ZeroArrowFrom Z b).
Lemma ZeroArrowEq (Z : Zero) (a b : C) (f1 : C⟦a, Z⟧) (g1 : C⟦Z, b⟧) :
f1 · g1 = ZeroArrow Z a b.
Show proof.
Lemma ZeroArrow_comp_left (Z : Zero) (a b c : C) (f : C⟦b, c⟧) :
ZeroArrow Z a b · f = ZeroArrow Z a c.
Show proof.
Lemma ZeroArrow_comp_right (Z : Zero) (a b c : C) (f : C⟦a, b⟧) :
f · ZeroArrow Z b c = ZeroArrow Z a c.
Show proof.
Lemma ZeroEndo_is_identity (Z : Zero) (f : Z --> Z) : identity Z = f.
Show proof.
Lemma isziso_from_Zero_to_Zero (Z Z' : Zero) :
is_z_isomorphism (ZeroArrowTo Z Z').
Show proof.
Definition z_iso_Zeros (Z Z' : Zero) : z_iso Z Z' :=
tpair _ (ZeroArrowTo Z' Z) (isziso_from_Zero_to_Zero Z' Z).
Lemma ZerosArrowEq (Z Z' : Zero) (a b : C) : ZeroArrow Z a b = ZeroArrow Z' a b.
Show proof.
Definition hasZero := ishinh Zero.
End def_zero.
Arguments isZero {_} _.
Arguments ZeroObject [C] _.
Arguments ZeroArrowTo [C]{Z} b.
Arguments ZeroArrowFrom [C]{Z} b.
Arguments ZeroArrow [C] _ _ _.
Arguments make_isZero {_} _ _ _ .
Arguments make_Zero {_} _ _ .
Section Zero_Unique.
Variable C : category.
Hypothesis H : is_univalent C.
Lemma isaprop_Zero : isaprop (Zero C).
Show proof.
End Zero_Unique.
Section facts.
Variable C : category.
Lemma ZeroIffInitialAndTerminal (b : C) :
isZero b <-> (isInitial C b) × (isTerminal C b).
Show proof.
Definition ZIsoToisZero {A : C} (Z : Zero C) (i : z_iso A Z) :
isZero A.
Show proof.
Lemma ZeroArrowEq (Z : Zero) (a b : C) (f1 : C⟦a, Z⟧) (g1 : C⟦Z, b⟧) :
f1 · g1 = ZeroArrow Z a b.
Show proof.
rewrite (ArrowsToZero Z a f1 (ZeroArrowTo Z a)).
rewrite (ArrowsFromZero Z b g1 (ZeroArrowFrom Z b)).
apply idpath.
rewrite (ArrowsFromZero Z b g1 (ZeroArrowFrom Z b)).
apply idpath.
Lemma ZeroArrow_comp_left (Z : Zero) (a b c : C) (f : C⟦b, c⟧) :
ZeroArrow Z a b · f = ZeroArrow Z a c.
Show proof.
Lemma ZeroArrow_comp_right (Z : Zero) (a b c : C) (f : C⟦a, b⟧) :
f · ZeroArrow Z b c = ZeroArrow Z a c.
Show proof.
Lemma ZeroEndo_is_identity (Z : Zero) (f : Z --> Z) : identity Z = f.
Show proof.
Lemma isziso_from_Zero_to_Zero (Z Z' : Zero) :
is_z_isomorphism (ZeroArrowTo Z Z').
Show proof.
Definition z_iso_Zeros (Z Z' : Zero) : z_iso Z Z' :=
tpair _ (ZeroArrowTo Z' Z) (isziso_from_Zero_to_Zero Z' Z).
Lemma ZerosArrowEq (Z Z' : Zero) (a b : C) : ZeroArrow Z a b = ZeroArrow Z' a b.
Show proof.
set (i := z_iso_Zeros Z Z').
unfold ZeroArrow.
assert (e : ZeroArrowTo Z a · identity _ = ZeroArrowTo Z a) by apply id_right.
rewrite <- e. clear e.
rewrite <- (z_iso_inv_after_z_iso i). rewrite assoc.
assert (e1 : ZeroArrowTo Z a · i = ZeroArrowTo Z' a) by apply ArrowsToZero.
rewrite e1. clear e1.
assert (e2 : inv_from_z_iso i · ZeroArrowFrom Z b = ZeroArrowFrom Z' b)
by apply ArrowsFromZero.
rewrite <- assoc. rewrite e2. clear e2.
apply idpath.
unfold ZeroArrow.
assert (e : ZeroArrowTo Z a · identity _ = ZeroArrowTo Z a) by apply id_right.
rewrite <- e. clear e.
rewrite <- (z_iso_inv_after_z_iso i). rewrite assoc.
assert (e1 : ZeroArrowTo Z a · i = ZeroArrowTo Z' a) by apply ArrowsToZero.
rewrite e1. clear e1.
assert (e2 : inv_from_z_iso i · ZeroArrowFrom Z b = ZeroArrowFrom Z' b)
by apply ArrowsFromZero.
rewrite <- assoc. rewrite e2. clear e2.
apply idpath.
Definition hasZero := ishinh Zero.
End def_zero.
Arguments isZero {_} _.
Arguments ZeroObject [C] _.
Arguments ZeroArrowTo [C]{Z} b.
Arguments ZeroArrowFrom [C]{Z} b.
Arguments ZeroArrow [C] _ _ _.
Arguments make_isZero {_} _ _ _ .
Arguments make_Zero {_} _ _ .
Section Zero_Unique.
Variable C : category.
Hypothesis H : is_univalent C.
Lemma isaprop_Zero : isaprop (Zero C).
Show proof.
apply invproofirrelevance.
intros Z Z'.
apply (total2_paths_f (isotoid _ H (z_iso_Zeros _ Z Z'))).
apply proofirrelevance.
unfold isZero.
apply isapropdirprod; apply impred; intros t; apply isapropiscontr.
intros Z Z'.
apply (total2_paths_f (isotoid _ H (z_iso_Zeros _ Z Z'))).
apply proofirrelevance.
unfold isZero.
apply isapropdirprod; apply impred; intros t; apply isapropiscontr.
End Zero_Unique.
Section facts.
Variable C : category.
Lemma ZeroIffInitialAndTerminal (b : C) :
isZero b <-> (isInitial C b) × (isTerminal C b).
Show proof.
Definition ZIsoToisZero {A : C} (Z : Zero C) (i : z_iso A Z) :
isZero A.
Show proof.
use make_isZero.
- intros a.
use tpair.
+ exact (i · (ZeroArrowFrom a)).
+ cbn. intros t.
apply (pre_comp_with_z_iso_is_inj (pr2 (z_iso_inv_from_z_iso i))).
rewrite assoc. cbn. rewrite (z_iso_after_z_iso_inv i). rewrite id_left.
apply ArrowsFromZero.
- intros a.
use tpair.
+ exact ((ZeroArrowTo a) · (z_iso_inv_from_z_iso i)).
+ cbn. intros t.
apply (post_comp_with_z_iso_is_inj (pr2 i)).
rewrite <- assoc. cbn.
etrans.
2: { apply maponpaths, pathsinv0, (z_iso_after_z_iso_inv i). }
rewrite id_right.
apply ArrowsToZero.
- intros a.
use tpair.
+ exact (i · (ZeroArrowFrom a)).
+ cbn. intros t.
apply (pre_comp_with_z_iso_is_inj (pr2 (z_iso_inv_from_z_iso i))).
rewrite assoc. cbn. rewrite (z_iso_after_z_iso_inv i). rewrite id_left.
apply ArrowsFromZero.
- intros a.
use tpair.
+ exact ((ZeroArrowTo a) · (z_iso_inv_from_z_iso i)).
+ cbn. intros t.
apply (post_comp_with_z_iso_is_inj (pr2 i)).
rewrite <- assoc. cbn.
etrans.
2: { apply maponpaths, pathsinv0, (z_iso_after_z_iso_inv i). }
rewrite id_right.
apply ArrowsToZero.
Lemma transport_target_ZeroArrow {a b c : C} (Z : Zero C) (e : b = c) :
transportf _ e (ZeroArrow Z a b) = ZeroArrow Z a c.
Show proof.
Lemma transport_source_ZeroArrow {a b c : C} (Z : Zero C) (e : b = a) :
transportf (λ (a' : ob C), precategory_morphisms a' c) e (ZeroArrow Z b c) = ZeroArrow Z a c.
Show proof.
Definition zero_lifts (M:category) {X:Type} (j : X -> ob M) := ∃ z, isZero (j z).
End facts.
transportf _ e (ZeroArrow Z a b) = ZeroArrow Z a c.
Show proof.
Lemma transport_source_ZeroArrow {a b c : C} (Z : Zero C) (e : b = a) :
transportf (λ (a' : ob C), precategory_morphisms a' c) e (ZeroArrow Z b c) = ZeroArrow Z a c.
Show proof.
Definition zero_lifts (M:category) {X:Type} (j : X -> ob M) := ∃ z, isZero (j z).
End facts.