Library UniMath.CategoryTheory.Limits.Initial
- A proof that initial object is a property in a (saturated/univalent) category (isaprop_Initial)
- Construction of initial from the empty coproduct (initial_from_empty_coproduct)
- Initial element in a functor precategory (Initial_functor_precat)
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Local Open Scope cat.
Section def_initial.
Definition isInitial {C : precategory} (a : C) : UU := ∏ b : C, iscontr (a --> b).
Definition Initial (C : precategory) : UU := ∑ a, @isInitial C a.
Definition InitialObject {C : precategory} (O : Initial C) : C := pr1 O.
Coercion InitialObject : Initial >-> ob.
Definition InitialArrow {C : precategory} (O : Initial C) (b : C) : O --> b := pr1 (pr2 O b).
Lemma InitialArrowUnique {C : precategory} {I : Initial C} {a : C} (f : C⟦InitialObject I,a⟧) :
f = InitialArrow I _.
Show proof.
Lemma InitialEndo_is_identity {C : precategory} {O : Initial C} (f : O --> O) : f = identity O.
Show proof.
Lemma InitialArrowEq {C : precategory} {O : Initial C} {a : C} (f g : O --> a) : f = g.
Show proof.
Definition make_Initial {C : precategory} (a : C) (H : isInitial a) : Initial C.
Show proof.
Definition make_isInitial {C : precategory} (a : C) (H : ∏ (b : C), iscontr (a --> b)) :
isInitial a.
Show proof.
Lemma isziso_from_Initial_to_Initial {C : precategory} (O O' : Initial C) :
is_z_isomorphism (InitialArrow O O').
Show proof.
Definition ziso_Initials {C : precategory} (O O' : Initial C) : z_iso O O' :=
InitialArrow O O',,isziso_from_Initial_to_Initial O O'.
Definition hasInitial {C : precategory} : UU := ishinh (Initial C).
End def_initial.
Arguments Initial : clear implicits.
Arguments isInitial : clear implicits.
Arguments InitialObject {_} _.
Arguments InitialArrow {_} _ _.
Arguments InitialArrowUnique {_} _ _ _.
Arguments make_isInitial {_} _ _ _.
Arguments make_Initial {_} _ _.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Local Open Scope cat.
Section def_initial.
Definition isInitial {C : precategory} (a : C) : UU := ∏ b : C, iscontr (a --> b).
Definition Initial (C : precategory) : UU := ∑ a, @isInitial C a.
Definition InitialObject {C : precategory} (O : Initial C) : C := pr1 O.
Coercion InitialObject : Initial >-> ob.
Definition InitialArrow {C : precategory} (O : Initial C) (b : C) : O --> b := pr1 (pr2 O b).
Lemma InitialArrowUnique {C : precategory} {I : Initial C} {a : C} (f : C⟦InitialObject I,a⟧) :
f = InitialArrow I _.
Show proof.
Lemma InitialEndo_is_identity {C : precategory} {O : Initial C} (f : O --> O) : f = identity O.
Show proof.
Lemma InitialArrowEq {C : precategory} {O : Initial C} {a : C} (f g : O --> a) : f = g.
Show proof.
Definition make_Initial {C : precategory} (a : C) (H : isInitial a) : Initial C.
Show proof.
exists a.
exact H.
exact H.
Definition make_isInitial {C : precategory} (a : C) (H : ∏ (b : C), iscontr (a --> b)) :
isInitial a.
Show proof.
exact H.
Lemma isziso_from_Initial_to_Initial {C : precategory} (O O' : Initial C) :
is_z_isomorphism (InitialArrow O O').
Show proof.
Definition ziso_Initials {C : precategory} (O O' : Initial C) : z_iso O O' :=
InitialArrow O O',,isziso_from_Initial_to_Initial O O'.
Definition hasInitial {C : precategory} : UU := ishinh (Initial C).
End def_initial.
Arguments Initial : clear implicits.
Arguments isInitial : clear implicits.
Arguments InitialObject {_} _.
Arguments InitialArrow {_} _ _.
Arguments InitialArrowUnique {_} _ _ _.
Arguments make_isInitial {_} _ _ _.
Arguments make_Initial {_} _ _.
Section Initial_Unique.
Context (C : category) (H : is_univalent C).
Lemma isaprop_Initial : isaprop (Initial C).
Show proof.
End Initial_Unique.
Section Initial_and_EmptyCoprod.
Context (C : category) (H : is_univalent C).
Lemma isaprop_Initial : isaprop (Initial C).
Show proof.
apply invproofirrelevance.
intros O O'.
apply (total2_paths_f (isotoid _ H (ziso_Initials O O')) ).
apply proofirrelevance.
unfold isInitial.
apply impred.
intro t ; apply isapropiscontr.
intros O O'.
apply (total2_paths_f (isotoid _ H (ziso_Initials O O')) ).
apply proofirrelevance.
unfold isInitial.
apply impred.
intro t ; apply isapropiscontr.
End Initial_Unique.
Section Initial_and_EmptyCoprod.
Construct Initial from empty arbitrary coproduct.
Definition initial_from_empty_coproduct (C : category):
Coproduct empty C fromempty -> Initial C.
Show proof.
End Initial_and_EmptyCoprod.
Coproduct empty C fromempty -> Initial C.
Show proof.
intros X.
use (make_Initial (CoproductObject _ _ X)).
use make_isInitial.
intros b.
assert (H : ∏ i : empty, C⟦fromempty i, b⟧) by
(intros i; apply (fromempty i)).
apply (make_iscontr (CoproductArrow _ _ X H)).
abstract (intros t; apply CoproductArrowUnique; intros i; apply (fromempty i)).
use (make_Initial (CoproductObject _ _ X)).
use make_isInitial.
intros b.
assert (H : ∏ i : empty, C⟦fromempty i, b⟧) by
(intros i; apply (fromempty i)).
apply (make_iscontr (CoproductArrow _ _ X H)).
abstract (intros t; apply CoproductArrowUnique; intros i; apply (fromempty i)).
End Initial_and_EmptyCoprod.
Section InitialFunctorCat.
Context (C D : category) (ID : Initial D).
Definition Initial_functor_precat : Initial [C, D].
Show proof.
End InitialFunctorCat.
Context (C D : category) (ID : Initial D).
Definition Initial_functor_precat : Initial [C, D].
Show proof.
use make_Initial.
- exact (constant_functor _ _ ID).
- intros F.
use tpair.
+ use make_nat_trans.
* intro a; apply InitialArrow.
* abstract (intros a b f; apply InitialArrowEq).
+ abstract (intros α; apply (nat_trans_eq D); intro a; apply InitialArrowUnique).
- exact (constant_functor _ _ ID).
- intros F.
use tpair.
+ use make_nat_trans.
* intro a; apply InitialArrow.
* abstract (intros a b f; apply InitialArrowEq).
+ abstract (intros α; apply (nat_trans_eq D); intro a; apply InitialArrowUnique).
End InitialFunctorCat.
Morphisms to the initial object are epis
Section epis_initial.
Context {C : precategory} (IC : Initial C).
Lemma to_initial_isEpi (a : C) (f : a --> IC) : isEpi f.
Show proof.
End epis_initial.
Definition iso_to_Initial
{C : category}
(I : Initial C)
(x : C)
(i : z_iso I x)
: isInitial C x.
Show proof.
Context {C : precategory} (IC : Initial C).
Lemma to_initial_isEpi (a : C) (f : a --> IC) : isEpi f.
Show proof.
End epis_initial.
Definition iso_to_Initial
{C : category}
(I : Initial C)
(x : C)
(i : z_iso I x)
: isInitial C x.
Show proof.
intros w.
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
refine (!(id_left _) @ _ @ id_left _) ;
rewrite <- !(z_iso_after_z_iso_inv i) ;
rewrite !assoc' ;
apply maponpaths ;
apply InitialArrowEq).
- exact (z_iso_inv i · InitialArrow I w).
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
refine (!(id_left _) @ _ @ id_left _) ;
rewrite <- !(z_iso_after_z_iso_inv i) ;
rewrite !assoc' ;
apply maponpaths ;
apply InitialArrowEq).
- exact (z_iso_inv i · InitialArrow I w).