Library UniMath.CategoryTheory.limits.initial

Direct definition of initial object together with:
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.

Context {C : precategory}.

Definition isInitial (a : C) : UU := ∏ b : C, iscontr (a --> b).

Definition Initial : UU := ∑ a, isInitial a.

Definition InitialObject (O : Initial) : C := pr1 O.
Coercion InitialObject : Initial >-> ob.

Definition InitialArrow (O : Initial) (b : C) : O --> b := pr1 (pr2 O b).

Lemma InitialArrowUnique {I : Initial} {a : C} (f : C⟦InitialObject I,a⟧) :
  f = InitialArrow I _.
Proof.
exact (pr2 (pr2 I _ ) _ ).
Defined.

Lemma InitialEndo_is_identity {O : Initial} (f : O --> O) : f = identity O.
Proof.
now apply proofirrelevance, isapropifcontr, (pr2 O O).
Qed.

Lemma InitialArrowEq {O : Initial} {a : C} (f g : O --> a) : f = g.
Proof.
now rewrite (InitialArrowUnique f), (InitialArrowUnique g).
Qed.

Definition make_Initial (a : C) (H : isInitial a) : Initial.
Proof.
  ∃ a.
  exact H.
Defined.

Definition make_isInitial (a : C) (H : ∏ (b : C), iscontr (a --> b)) :
  isInitial a.
Proof.
  exact H.
Defined.

Lemma isiso_from_Initial_to_Initial (O O' : Initial) :
   is_iso (InitialArrow O O').
Proof.
  apply (is_iso_qinv _ (InitialArrow O' O)).
  split; apply InitialEndo_is_identity.
Defined.

Definition iso_Initials (O O' : Initial) : iso O O' :=
   (InitialArrow O O',,isiso_from_Initial_to_Initial O O').

Definition hasInitial := ishinh Initial.

Being initial is a property in a (saturated/univalent) category

Section Initial_Unique.

Hypothesis H : is_univalent C.

Lemma isaprop_Initial : isaprop Initial.
Proof.
  apply invproofirrelevance.
  intros O O'.
  apply (total2_paths_f (isotoid _ H (iso_Initials O O')) ).
  apply proofirrelevance.
  unfold isInitial.
  apply impred.
  intro t ; apply isapropiscontr.
Qed.

End Initial_Unique.

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_and_EmptyCoprod.

Construct Initial from empty arbitrary coproduct.
  Definition initial_from_empty_coproduct (C : precategory):
    Coproduct empty C fromempty → Initial C.
  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)); intros t.
    apply CoproductArrowUnique; intros i; apply (fromempty i).
  Defined.

End Initial_and_EmptyCoprod.









Construction of initial object in a functor category

Section InitialFunctorCat.

Variables (C D : precategory) (ID : Initial D) (hsD : has_homsets D).

Definition Initial_functor_precat : Initial [C, D, hsD].
Proof.
use make_Initial.
- use make_functor.
  + use tpair.
    × intros c; apply (InitialObject ID).
    × simpl; intros a b f; apply (InitialArrow ID).
  + split.
    × intro a; apply InitialEndo_is_identity.
    × intros a b c f g; apply pathsinv0, InitialArrowUnique.
- intros F.
  use tpair.
  + use make_nat_trans; simpl.
    × intro a; apply InitialArrow.
    × intros a b f; simpl.
      rewrite (InitialEndo_is_identity (InitialArrow ID ID)), id_left.
      now apply pathsinv0, InitialArrowUnique.
  + abstract (intros α; apply (nat_trans_eq hsD); intro a; apply InitialArrowUnique).
Defined.

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 : C⟦a,IC⟧) : isEpi f.
Proof.
apply make_isEpi; intros b g h H.
now apply InitialArrowEq.
Qed.

End epis_initial.