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.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag.
Require Import UniMath.CategoryTheory.Limits.Initial.

Local Open Scope cat.

Section def_initial.

Context {C : category}.

Definition empty_graph : graph.
Show proof.
  exists empty.
  exact (λ _ _, empty).

Definition initDiagram : diagram empty_graph C.
Show proof.
exists fromempty.
intros u; induction u.

All diagrams over the empty graph are equal
Lemma empty_graph_eq_diag (d d' : diagram empty_graph C) :
  eq_diag d d'.
Show proof.
  use tpair; use empty_rect.

Definition initCocone (c : C) : cocone initDiagram c.
Show proof.
use make_cocone; intro v; induction v.

Definition isInitial (a : C) :=
  isColimCocone initDiagram a (initCocone a).

Definition make_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 subtypePath; simpl;
    [intro; apply impred; intro v; induction v|].
  apply (pr2 (H b)).

Definition Initial : UU := ColimCocone initDiagram.

Definition make_Initial (a : C) (H : isInitial a) : Initial.
Show proof.
use (make_ColimCocone _ a (initCocone a)).
apply make_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) : CInitialObject O,b :=
  colimArrow _ _ (initCocone b).

Lemma InitialArrowUnique (I : Initial) (a : C)
  (f : CInitialObject I,a) : f = InitialArrow I _.
Show proof.
now apply colimArrowUnique; intro v; induction v.

Lemma ArrowsFromInitial (I : Initial) (a : C) (f g : CInitialObject I,a) : f = g.
Show proof.

Lemma InitialEndo_is_identity (O : Initial) (f : CInitialObject 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.

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 make_isInitial.
  intros b.
  use tpair.
  - exact (InitialArrow I b).
  - intros t. use (InitialArrowUnique I).

Maps between initial as special colimit and direct definition

Lemma equiv_isInitial1 (c : C) :
  Limits.Initial.isInitial C c -> isInitial c.
Show proof.
  intros X.
  use make_isInitial.
  intros b.
  apply (X b).

Lemma equiv_isInitial2 (c : C) :
  Limits.Initial.isInitial C c <- isInitial c.
Show proof.
  intros X.
  set (XI := make_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 make_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.make_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 : category) :
  Colims_of_shape empty_graph C -> Initial C.
Show proof.
now intros H; apply H.