Library UniMath.CategoryTheory.limits.graphs.initial
Definition of initial object as a colimit
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.total2_paths.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.initial.
Local Open Scope cat.
Section def_initial.
Context {C : precategory}.
Definition empty_graph : graph.
Show proof.
exists empty.
exact (λ _ _, empty).
exact (λ _ _, empty).
Definition initDiagram : diagram empty_graph C.
Show proof.
exists fromempty.
intros u; induction u.
intros u; induction u.
Definition initCocone (c : C) : cocone initDiagram c.
Show proof.
use mk_cocone; intro v; induction v.
Definition isInitial (a : C) :=
isColimCocone initDiagram a (initCocone a).
Definition mk_isInitial (a : C) (H : ∏ (b : C), iscontr (a --> b)) :
isInitial a.
Show proof.
intros b cb.
use tpair.
- exists (pr1 (H b)); intro v; induction v.
- intro t.
apply subtypeEquality; simpl;
[intro; apply impred; intro v; induction v|].
apply (pr2 (H b)).
use tpair.
- exists (pr1 (H b)); intro v; induction v.
- intro t.
apply subtypeEquality; simpl;
[intro; apply impred; intro v; induction v|].
apply (pr2 (H b)).
Definition Initial : UU := ColimCocone initDiagram.
Definition mk_Initial (a : C) (H : isInitial a) : Initial.
Show proof.
use (mk_ColimCocone _ a (initCocone a)).
apply mk_isInitial.
intro b.
set (x := H b (initCocone b)).
use tpair.
- apply (pr1 x).
- simpl; intro f; apply path_to_ctr; intro v; induction v.
apply mk_isInitial.
intro b.
set (x := H b (initCocone b)).
use tpair.
- apply (pr1 x).
- simpl; intro f; apply path_to_ctr; intro v; induction v.
Definition InitialObject (O : Initial) : C := colim O.
Definition InitialArrow (O : Initial) (b : C) : C⟦InitialObject O,b⟧ :=
colimArrow _ _ (initCocone b).
Lemma InitialArrowUnique (I : Initial) (a : C)
(f : C⟦InitialObject I,a⟧) : f = InitialArrow I _.
Show proof.
now apply colimArrowUnique; intro v; induction v.
Lemma ArrowsFromInitial (I : Initial) (a : C) (f g : C⟦InitialObject I,a⟧) : f = g.
Show proof.
eapply pathscomp0.
apply InitialArrowUnique.
now apply pathsinv0, InitialArrowUnique.
apply InitialArrowUnique.
now apply pathsinv0, InitialArrowUnique.
Lemma InitialEndo_is_identity (O : Initial) (f : C⟦InitialObject O,InitialObject O⟧) :
identity (InitialObject O) = f.
Show proof.
now apply colim_endo_is_identity; intro u; induction u.
Lemma isiso_from_Initial_to_Initial (O O' : Initial) :
is_iso (InitialArrow O (InitialObject O')).
Show proof.
apply (is_iso_qinv _ (InitialArrow O' (InitialObject O))).
split; apply pathsinv0, InitialEndo_is_identity.
split; apply pathsinv0, InitialEndo_is_identity.
Definition iso_Initials (O O' : Initial) : iso (InitialObject O) (InitialObject O') :=
tpair _ (InitialArrow O (InitialObject O')) (isiso_from_Initial_to_Initial O O') .
Definition hasInitial := ishinh Initial.
Lemma isInitial_Initial (I : Initial) :
isInitial (InitialObject I).
Show proof.
use mk_isInitial.
intros b.
use tpair.
- exact (InitialArrow I b).
- intros t. use (InitialArrowUnique I).
intros b.
use tpair.
- exact (InitialArrow I b).
- intros t. use (InitialArrowUnique I).
Lemma equiv_isInitial1 (c : C) :
limits.initial.isInitial C c -> isInitial c.
Show proof.
Lemma equiv_isInitial2 (c : C) :
limits.initial.isInitial C c <- isInitial c.
Show proof.
Definition equiv_Initial1 (c : C) :
limits.initial.Initial C -> Initial.
Show proof.
Definition equiv_Initial2 (c : C) :
limits.initial.Initial C <- Initial.
Show proof.
End def_initial.
Arguments Initial : clear implicits.
Arguments isInitial : clear implicits.
Lemma Initial_from_Colims (C : precategory) :
Colims_of_shape empty_graph C -> Initial C.
Show proof.
limits.initial.isInitial C c -> isInitial c.
Show proof.
intros X.
use mk_isInitial.
intros b.
apply (X b).
use mk_isInitial.
intros b.
apply (X b).
Lemma equiv_isInitial2 (c : C) :
limits.initial.isInitial C c <- isInitial c.
Show proof.
intros X.
set (XI := mk_Initial c X).
intros b.
use tpair.
- exact (InitialArrow XI b).
- intros t. use (InitialArrowUnique XI b).
set (XI := mk_Initial c X).
intros b.
use tpair.
- exact (InitialArrow XI b).
- intros t. use (InitialArrowUnique XI b).
Definition equiv_Initial1 (c : C) :
limits.initial.Initial C -> Initial.
Show proof.
intros I.
use mk_Initial.
- exact I.
- use equiv_isInitial1.
exact (pr2 I).
use mk_Initial.
- exact I.
- use equiv_isInitial1.
exact (pr2 I).
Definition equiv_Initial2 (c : C) :
limits.initial.Initial C <- Initial.
Show proof.
intros I.
use limits.initial.mk_Initial.
- exact (InitialObject I).
- use equiv_isInitial2.
use (isInitial_Initial I).
use limits.initial.mk_Initial.
- exact (InitialObject I).
- use equiv_isInitial2.
use (isInitial_Initial I).
End def_initial.
Arguments Initial : clear implicits.
Arguments isInitial : clear implicits.
Lemma Initial_from_Colims (C : precategory) :
Colims_of_shape empty_graph C -> Initial C.
Show proof.
now intros H; apply H.