Library UniMath.CategoryTheory.limits.graphs.initial

Definition of initial object as a colimit

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) : 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.

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.

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.