Library UniMath.CategoryTheory.Limits.StrictInitial

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Preservation.

Local Open Scope cat.

1. Strict initial objects

Definition is_strict_initial
           {C : category}
           (I : Initial C)
  : UU
  := ∏ (x : C)
       (f : x --> I),
     is_z_isomorphism f.

Proposition isaprop_is_strict_initial
            {C : category}
            (I : Initial C)
  : isaprop (is_strict_initial I).
Show proof.
  do 2 (use impred ; intro).
  apply isaprop_is_z_isomorphism.

Definition strict_initial_object
           (C : category)
  : UU
  := ∑ (I : Initial C),
     is_strict_initial I.

Proposition isaprop_strict_initial_object
            (C : univalent_category)
  : isaprop (strict_initial_object C).
Show proof.
  use isaproptotal2.
  - intro.
    apply isaprop_is_strict_initial.
  - intros.
    apply (isaprop_Initial C (univalent_category_is_univalent C)).

Definition make_strict_initial
           {C : category}
           (I : Initial C)
           (H : is_strict_initial I)
  : strict_initial_object C
  := I ,, H.

Coercion strict_initial_to_initial
         {C : category}
         (I : strict_initial_object C)
  : Initial C.
Show proof.
  exact (pr1 I).

Proposition is_strict_initial_strict_initial
            {C : category}
            (I : strict_initial_object C)
  : is_strict_initial I.
Show proof.
  exact (pr2 I).

Proposition is_initial_mor_to_strict_initial
            {C : category}
            (I : strict_initial_object C)
            (x : C)
            (f : x --> I)
  : isInitial _ x.
Show proof.
  use (iso_to_Initial I).
  pose (f_iso := f ,, is_strict_initial_strict_initial I x f : z_iso x I).
  exact (z_iso_inv f_iso).

2. Strictness is preserved under isomorphism

Definition strict_initial_z_iso
           {C : category}
           (I : strict_initial_object C)
           (I' : Initial C)
           (f : z_iso I I')
  : is_strict_initial I'.
Show proof.
  intros x g.
  pose (H := is_strict_initial_strict_initial I x (g · inv_from_z_iso f)).
  pose (h := (_ ,, H) : z_iso x I).
  use make_is_z_isomorphism.
  - exact (inv_from_z_iso f · inv_from_z_iso h).
  - split.
    + abstract
        (rewrite !assoc ;
         exact (z_iso_inv_after_z_iso h)).
    + abstract
        (apply InitialArrowEq).

Definition all_initial_strict
           {C : category}
           (I : strict_initial_object C)
           (I' : Initial C)
  : is_strict_initial I'.
Show proof.
  use (strict_initial_z_iso I I').
  apply ziso_Initials.

3. Stability of strict initial objects

Definition stict_initial_stable
           {C : category}
           (HC : Pullbacks C)
           (I : strict_initial_object C)
           {x y : C}
           (f : x --> y)
  : preserves_initial (cod_pb HC f).
Show proof.
  use preserves_initial_if_preserves_chosen.
  {
    exact (initial_cod_fib y I).
  }
  unfold preserves_chosen_initial.
  use to_initial_slice ; cbn.
  use (is_initial_mor_to_strict_initial I).
  apply PullbackPr1.

4. Monics from strict initial objects

Definition monic_from_strict_initial
           {C : category}
           (I : Initial C)
           (HI : is_strict_initial I)
           (y : C)
  : Monic C I y.
Show proof.
  use make_Monic.
  - apply InitialArrow.
  - abstract
      (intros x g h p ;
       use (InitialArrowEq (O := make_Initial x _)) ;
       use (iso_to_Initial I) ;
       use z_iso_inv ;
       exact (g ,, HI _ _)).