# 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 : CInitialObject 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, Cfromempty 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 : Ca,IC) : isEpi f.
Proof.
apply make_isEpi; intros b g h H.
now apply InitialArrowEq.
Qed.

End epis_initial.