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.Morphisms.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.Initial.
Require Import UniMath.Bicategories.Limits.Final.
Require Import UniMath.Bicategories.Limits.Products.
Import Products.Notations.

Local Open Scope cat.

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

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

2. Final objects
Section FixAFinal.
  Context (B₁ : bicat)
          (B₂ : bicat)
          (f : bifinal_obj B₂).

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

  Definition final_psfunctor_1cell_data
             (F : psfunctor B₁ B₂)
    : pstrans_data F final_psfunctor.
  Show proof.
    use make_pstrans_data.
    - exact (λ x, is_bifinal_1cell_property (pr2 f) (F x)).
    - intros x y g.
      apply (is_bifinal_invertible_2cell_property (pr2 f)).

  Definition final_psfunctor_1cell_is_pstrans
             (F : psfunctor B₁ B₂)
    : is_pstrans (final_psfunctor_1cell_data F).
  Show proof.
    repeat split ; intros ; apply (is_bifinal_eq_property (pr2 f)).

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

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

  Definition final_psfunctor_2cell_is_modification
             {F : psfunctor B₁ B₂}
             (α β : pstrans F final_psfunctor)
    : is_modification (final_psfunctor_2cell_data α β).
  Show proof.
    intros x y g.
    apply (is_bifinal_eq_property (pr2 f)).

  Definition final_psfunctor_2cell
             {F : psfunctor B₁ B₂}
             (α β : pstrans F final_psfunctor)
    : modification α β.
  Show proof.
    use make_modification.
    - exact (final_psfunctor_2cell_data α β).
    - exact (final_psfunctor_2cell_is_modification α β).

  Definition final_psfunctor_eq
             {F : psfunctor B₁ B₂}
             {α β : pstrans F final_psfunctor}
             (m₁ m₂ : modification α β)
    : m₁ = m₂.
  Show proof.
    use modification_eq.
    intro.
    apply (is_bifinal_eq_property (pr2 f)).

  Definition psfunctor_bifinal
    : bifinal_obj (psfunctor_bicat B₁ B₂).
  Show proof.
    simple refine (_ ,, _).
    - exact final_psfunctor.
    - use make_is_bifinal.
      + exact final_psfunctor_1cell.
      + exact @final_psfunctor_2cell.
      + exact @final_psfunctor_eq.
End FixAFinal.

3. Initial objects
Section FixAnInitial.
  Context (B₁ : bicat)
          (B₂ : bicat)
          (i : biinitial_obj B₂).

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

  Definition initial_psfunctor_1cell_data
             (F : psfunctor B₁ B₂)
    : pstrans_data initial_psfunctor F.
  Show proof.
    use make_pstrans_data.
    - exact (λ x, is_biinitial_1cell_property (pr2 i) (F x)).
    - intros x y g.
      apply (is_biinitial_invertible_2cell_property (pr2 i)).

  Definition initial_psfunctor_1cell_is_pstrans
             (F : psfunctor B₁ B₂)
    : is_pstrans (initial_psfunctor_1cell_data F).
  Show proof.
    repeat split ; intros ; apply (is_biinitial_eq_property (pr2 i)).

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

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

  Definition initial_psfunctor_2cell_is_modification
             {F : psfunctor B₁ B₂}
             (α β : pstrans initial_psfunctor F)
    : is_modification (initial_psfunctor_2cell_data α β).
  Show proof.
    intros x y g.
    apply (is_biinitial_eq_property (pr2 i)).

  Definition initial_psfunctor_2cell
             {F : psfunctor B₁ B₂}
             (α β : pstrans initial_psfunctor F)
    : modification α β.
  Show proof.
    use make_modification.
    - exact (initial_psfunctor_2cell_data α β).
    - exact (initial_psfunctor_2cell_is_modification α β).

  Definition initial_psfunctor_eq
             {F : psfunctor B₁ B₂}
             {α β : pstrans initial_psfunctor F}
             (m₁ m₂ : modification α β)
    : m₁ = m₂.
  Show proof.
    use modification_eq.
    intro.
    apply (is_biinitial_eq_property (pr2 i)).

  Definition psfunctor_biinitial
    : biinitial_obj (psfunctor_bicat B₁ B₂).
  Show proof.
    simple refine (_ ,, _).
    - exact initial_psfunctor.
    - use make_is_biinitial.
      + exact initial_psfunctor_1cell.
      + exact @initial_psfunctor_2cell.
      + exact @initial_psfunctor_eq.
End FixAnInitial.