Library UniMath.Bicategories.Morphisms.Properties.FromInitial

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Examples.OpCellBicat.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Morphisms.FullyFaithful.
Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms.
Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration.
Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration.
Require Import UniMath.Bicategories.Colimits.Initial.

Local Open Scope cat.

Section FromInitial.
  Context {B : bicat}
          {x y : B}
          (Hx : is_biinitial x)
          (Sx : biinitial_is_strict_biinitial_obj Hx)
          (f : x --> y).

1. Faithfulness
  Definition from_biinitial_faithful_1cell
    : faithful_1cell f.
  Show proof.
    intros z g₁ g₂ α₁ α₂ p.
    enough (Hz : is_biinitial z).
    {
      apply (is_biinitial_eq_property Hz).
    }
    exact (equiv_to_biinitial Hx (Sx z g₁)).

2. Fully faithfulness
  Definition from_biinitial_fully_faithful_1cell
    : fully_faithful_1cell f.
  Show proof.
    use make_fully_faithful.
    - exact from_biinitial_faithful_1cell.
    - intros z g₁ g₂ αf.
      assert(Hz : is_biinitial z).
      {
        exact (equiv_to_biinitial Hx (Sx z g₁)).
      }
      simple refine (_ ,, _).
      + apply (is_biinitial_2cell_property Hz).
      + apply (is_biinitial_eq_property Hz).

3. Pseudomonic
  Definition from_biinitial_pseudomonic_1cell
    : pseudomonic_1cell f.
  Show proof.
    use make_pseudomonic.
    - exact from_biinitial_faithful_1cell.
    - intros z g₁ g₂ αf Hαf.
      assert(Hz : is_biinitial z).
      {
        exact (equiv_to_biinitial Hx (Sx z g₁)).
      }
      simple refine (_ ,, _ ,, _).
      + apply (is_biinitial_2cell_property Hz).
      + use make_is_invertible_2cell.
        * apply (is_biinitial_2cell_property Hz).
        * apply (is_biinitial_eq_property Hz).
        * apply (is_biinitial_eq_property Hz).
      + apply (is_biinitial_eq_property Hz).

4. Conservativity
  Definition from_biinitial_conservative_1cell
    : conservative_1cell f.
  Show proof.
    intros z g₁ g₂ α Hα.
    assert(Hz : is_biinitial z).
    {
      exact (equiv_to_biinitial Hx (Sx z g₁)).
    }
    use make_is_invertible_2cell.
    - apply (is_biinitial_2cell_property Hz).
    - apply (is_biinitial_eq_property Hz).
    - apply (is_biinitial_eq_property Hz).

5. Discreteness
  Definition from_biinitial_discrete_1cell
    : discrete_1cell f.
  Show proof.
    split.
    - exact from_biinitial_faithful_1cell.
    - exact from_biinitial_conservative_1cell.

6. It's an internal Street fibration
  Definition from_biinitial_is_cartesian_2cell_sfib
             {z : B}
             {g₁ g₂ : z --> x}
             (α : g₁ ==> g₂)
    : is_cartesian_2cell_sfib f α.
  Show proof.
    assert(Hz : is_biinitial z).
    {
      exact (equiv_to_biinitial Hx (Sx z g₁)).
    }
    intros w γ δp p.
    use iscontraprop1.
    - abstract
        (use invproofirrelevance ;
         intros φ₁ φ₂ ;
         use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
         apply (is_biinitial_eq_property Hz)).
    - simple refine (_ ,, _ ,, _).
      + apply (is_biinitial_2cell_property Hz).
      + apply (is_biinitial_eq_property Hz).
      + apply (is_biinitial_eq_property Hz).

  Definition from_biinitial_internal_sfib_cleaving
    : internal_sfib_cleaving f.
  Show proof.
    intros z g h α.
    assert(Hz : is_biinitial z).
    {
      exact (equiv_to_biinitial Hx (Sx z h)).
    }
    simple refine (_ ,, _ ,, _ ,, _ ,, _).
    - exact h.
    - apply id2.
    - use make_invertible_2cell.
      + apply (is_biinitial_2cell_property Hz).
      + use make_is_invertible_2cell.
        * apply (is_biinitial_2cell_property Hz).
        * apply (is_biinitial_eq_property Hz).
        * apply (is_biinitial_eq_property Hz).
    - apply id_is_cartesian_2cell_sfib.
    - apply (is_biinitial_eq_property Hz).

  Definition from_biinitial_lwhisker_is_cartesian
    : lwhisker_is_cartesian f.
  Show proof.
    intro ; intros.
    apply from_biinitial_is_cartesian_2cell_sfib.

  Definition from_biinitial_internal_sfib
    : internal_sfib f.
  Show proof.
    split.
    - exact from_biinitial_internal_sfib_cleaving.
    - exact from_biinitial_lwhisker_is_cartesian.

7. Preservation of cartesian cells
  Definition from_biinitial_mor_preserves_cartesian
             {x' y' : B}
             (f' : x' --> y')
    : mor_preserves_cartesian
        f
        f'
        (is_biinitial_1cell_property Hx x').
  Show proof.
    intros z h₁ h₂ γ Hγ.
    assert(Hz : is_biinitial z).
    {
      exact (equiv_to_biinitial Hx (Sx z h₁)).
    }
    intros w ζ δp p.
    use iscontraprop1.
    - abstract
        (use invproofirrelevance ;
         intros φ₁ φ₂ ;
         use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
         apply (is_biinitial_eq_property Hz)).
    - simple refine (_ ,, _ ,, _).
      + apply (is_biinitial_2cell_property Hz).
      + apply (is_biinitial_eq_property Hz).
      + apply (is_biinitial_eq_property Hz).

8. It's an internal Street opfibration
  Definition from_biinitial_is_opcartesian_2cell_sopfib
             {z : B}
             {g₁ g₂ : z --> x}
             (α : g₁ ==> g₂)
    : is_opcartesian_2cell_sopfib f α.
  Show proof.
    assert(Hz : is_biinitial z).
    {
      exact (equiv_to_biinitial Hx (Sx z g₁)).
    }
    intros w γ δp p.
    use iscontraprop1.
    - abstract
        (use invproofirrelevance ;
         intros φ₁ φ₂ ;
         use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
         apply (is_biinitial_eq_property Hz)).
    - simple refine (_ ,, _ ,, _).
      + apply (is_biinitial_2cell_property Hz).
      + apply (is_biinitial_eq_property Hz).
      + apply (is_biinitial_eq_property Hz).

  Definition from_biinitial_internal_sopfib_cleaving
    : internal_sopfib_opcleaving f.
  Show proof.
    intros z g h α.
    assert(Hz : is_biinitial z).
    {
      exact (equiv_to_biinitial Hx (Sx z g)).
    }
    simple refine (_ ,, _ ,, _ ,, _ ,, _).
    - exact g.
    - apply id2.
    - use make_invertible_2cell.
      + apply (is_biinitial_2cell_property Hz).
      + use make_is_invertible_2cell.
        * apply (is_biinitial_2cell_property Hz).
        * apply (is_biinitial_eq_property Hz).
        * apply (is_biinitial_eq_property Hz).
    - apply id_is_opcartesian_2cell_sopfib.
    - apply (is_biinitial_eq_property Hz).

  Definition from_biinitial_lwhisker_is_opcartesian
    : lwhisker_is_opcartesian f.
  Show proof.
    intro ; intros.
    apply from_biinitial_is_opcartesian_2cell_sopfib.

  Definition from_biinitial_internal_sopfib
    : internal_sopfib f.
  Show proof.
    split.
    - exact from_biinitial_internal_sopfib_cleaving.
    - exact from_biinitial_lwhisker_is_opcartesian.

9. Preservation of opcartesian cells
  Definition from_biinitial_mor_preserves_opcartesian
             {x' y' : B}
             (f' : x' --> y')
    : mor_preserves_opcartesian
        f
        f'
        (is_biinitial_1cell_property Hx x').
  Show proof.
    intros z h₁ h₂ γ Hγ.
    assert(Hz : is_biinitial z).
    {
      exact (equiv_to_biinitial Hx (Sx z h₁)).
    }
    intros w ζ δp p.
    use iscontraprop1.
    - abstract
        (use invproofirrelevance ;
         intros φ₁ φ₂ ;
         use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
         apply (is_biinitial_eq_property Hz)).
    - simple refine (_ ,, _ ,, _).
      + apply (is_biinitial_2cell_property Hz).
      + apply (is_biinitial_eq_property Hz).
      + apply (is_biinitial_eq_property Hz).
End FromInitial.