Library UniMath.Bicategories.PseudoFunctors.PseudoFunctorLimits

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.FullyFaithful.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Require Import UniMath.Bicategories.Modifications.Modification.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Constant.
Import PseudoFunctor.Notations.
Require Import UniMath.Bicategories.Colimits.Final.
Require Import UniMath.Bicategories.Colimits.Initial.
Require Import UniMath.Bicategories.Colimits.Products.
Import Products.Notations.

Local Open Scope cat.

Section FixALocallyGrpd.
  Context (B₁ : bicat)
          {B₂ : bicat}
          (HB₂ : locally_groupoid B₂).

  Definition locally_groupoid_psfunctor_bicat
    : locally_groupoid (psfunctor_bicat B₁ B₂).
  Proof.
    intros F G α β m.
    use make_is_invertible_modification.
    intro x.
    apply HB₂.
  Defined.
End FixALocallyGrpd.

Section FixAFinal.
  Context (B₁ : bicat)
          {B₂ : bicat}
          {HB₂_2_1 : is_univalent_2_1 B₂}
          (f : BiFinal HB₂_2_1).

  Definition final_psfunctor
    : psfunctor_bicat B₁ B₂
    := constant _ (pr1 f).

  Definition final_psfunctor_1cell_data
             (F : psfunctor B₁ B₂)
    : pstrans_data F final_psfunctor.
  Proof.
    use make_pstrans_data.
    - exact (λ x, bifinal_1cell _ (pr2 f) (F x)).
    - intros x y g.
      apply (bifinal_2cell _ (pr2 f)).
  Defined.

  Definition final_psfunctor_1cell_is_pstrans
             (F : psfunctor B₁ B₂)
    : is_pstrans (final_psfunctor_1cell_data F).
  Proof.
    repeat split ; intros ; apply (bifinal_eq _ (pr2 f)).
  Qed.

  Definition final_psfunctor_1cell
             (F : psfunctor B₁ B₂)
    : pstrans F final_psfunctor.
  Proof.
    use make_pstrans.
    - exact (final_psfunctor_1cell_data F).
    - exact (final_psfunctor_1cell_is_pstrans F).
  Defined.

  Definition final_psfunctor_2cell_data
             {F : psfunctor B₁ B₂}
             (α β : pstrans F final_psfunctor)
    : invertible_modification_data α β
    := λ x, bifinal_2cell _ (pr2 f) (α x) (β x).

  Definition final_psfunctor_2cell_is_modification
             {F : psfunctor B₁ B₂}
             (α β : pstrans F final_psfunctor)
    : is_modification (final_psfunctor_2cell_data α β).
  Proof.
    intros x y g.
    apply (bifinal_eq _ (pr2 f)).
  Qed.

  Definition final_psfunctor_2cell
             {F : psfunctor B₁ B₂}
             (α β : pstrans F final_psfunctor)
    : invertible_modification α β.
  Proof.
    use make_invertible_modification.
    - exact (final_psfunctor_2cell_data α β).
    - exact (final_psfunctor_2cell_is_modification α β).
  Defined.

  Definition final_psfunctor_eq
             {F : psfunctor B₁ B₂}
             {α β : pstrans F final_psfunctor}
             (m₁ m₂ : modification α β)
    : m₁ = m₂.
  Proof.
    use modification_eq.
    intro.
    apply (bifinal_eq _ (pr2 f)).
  Qed.

  Definition psfunctor_bifinal
    : BiFinal (psfunctor_bicat_is_univalent_2_1 B₁ B₂ HB₂_2_1).
  Proof.
    simple refine (_ ,, _).
    - exact final_psfunctor.
    - use is_bifinal'_to_is_bifinal.
      use make_is_bifinal'.
      + exact final_psfunctor_1cell.
      + exact @final_psfunctor_2cell.
      + exact @final_psfunctor_eq.
  Defined.
End FixAFinal.

Section FixAnInitial.
  Context (B₁ : bicat)
          {B₂ : bicat}
          {HB₂_2_1 : is_univalent_2_1 B₂}
          (i : BiInitial HB₂_2_1).

  Definition initial_psfunctor
    : psfunctor_bicat B₁ B₂
    := constant _ (pr1 i).

  Definition initial_psfunctor_1cell_data
             (F : psfunctor B₁ B₂)
    : pstrans_data initial_psfunctor F.
  Proof.
    use make_pstrans_data.
    - exact (λ x, biinitial_1cell _ (pr2 i) (F x)).
    - intros x y g.
      apply (biinitial_2cell _ (pr2 i)).
  Defined.

  Definition initial_psfunctor_1cell_is_pstrans
             (F : psfunctor B₁ B₂)
    : is_pstrans (initial_psfunctor_1cell_data F).
  Proof.
    repeat split ; intros ; apply (biinitial_eq _ (pr2 i)).
  Qed.

  Definition initial_psfunctor_1cell
             (F : psfunctor B₁ B₂)
    : pstrans initial_psfunctor F.
  Proof.
    use make_pstrans.
    - exact (initial_psfunctor_1cell_data F).
    - exact (initial_psfunctor_1cell_is_pstrans F).
  Defined.

  Definition initial_psfunctor_2cell_data
             {F : psfunctor B₁ B₂}
             (α β : pstrans initial_psfunctor F)
    : invertible_modification_data α β
    := λ x, biinitial_2cell _ (pr2 i) (α x) (β x).

  Definition initial_psfunctor_2cell_is_modification
             {F : psfunctor B₁ B₂}
             (α β : pstrans initial_psfunctor F)
    : is_modification (initial_psfunctor_2cell_data α β).
  Proof.
    intros x y g.
    apply (biinitial_eq _ (pr2 i)).
  Qed.

  Definition initial_psfunctor_2cell
             {F : psfunctor B₁ B₂}
             (α β : pstrans initial_psfunctor F)
    : invertible_modification α β.
  Proof.
    use make_invertible_modification.
    - exact (initial_psfunctor_2cell_data α β).
    - exact (initial_psfunctor_2cell_is_modification α β).
  Defined.

  Definition initial_psfunctor_eq
             {F : psfunctor B₁ B₂}
             {α β : pstrans initial_psfunctor F}
             (m₁ m₂ : modification α β)
    : m₁ = m₂.
  Proof.
    use modification_eq.
    intro.
    apply (biinitial_eq _ (pr2 i)).
  Qed.

  Definition psfunctor_biinitial
    : BiInitial (psfunctor_bicat_is_univalent_2_1 B₁ B₂ HB₂_2_1).
  Proof.
    simple refine (_ ,, _).
    - exact initial_psfunctor.
    - use is_biinitial'_to_is_biinitial.
      use make_is_biinitial'.
      + exact initial_psfunctor_1cell.
      + exact @initial_psfunctor_2cell.
      + exact @initial_psfunctor_eq.
  Defined.
End FixAnInitial.