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.

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.
exact (pr2 (pr2 I _ ) _ ).

Lemma InitialEndo_is_identity {C : precategory} {O : Initial C} (f : O --> O) : f = identity O.
Show proof.
apply proofirrelevancecontr, (pr2 O O).

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

Definition make_Initial {C : precategory} (a : C) (H : isInitial a) : Initial C.
Show proof.
  exists a.
  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.
  exists (InitialArrow O' O).
  split; apply InitialEndo_is_identity.

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 {_} _ _.

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

Section Initial_Unique.

  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.

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

End Initial_and_EmptyCoprod.









Construction of initial object in a functor category

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

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.
apply make_isEpi; intros b g h H.
now apply InitialArrowEq.

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