Library UniMath.Bicategories.ComprehensionCat.Biequivalence.LocalProperty

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.Core.Examples.StructuredCategories.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Import DispBicat.Notations.
Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions.
Require Import UniMath.Bicategories.DisplayedBicats.DispBiequivalence.
Require Import UniMath.Bicategories.DisplayedBicats.DispBuilders.
Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor.
Require Import UniMath.Bicategories.DisplayedBicats.DispTransformation.
Require Import UniMath.Bicategories.DisplayedBicats.DispModification.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence.
Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.
Require Import UniMath.Bicategories.ComprehensionCat.CompCatNotations.
Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat.
Require Import UniMath.Bicategories.ComprehensionCat.ComprehensionEso.
Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.FinLimToDFLCompCat.
Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.DFLCompCatToFinLim.
Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.Unit.
Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.Counit.
Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.Biequiv.
Require Import UniMath.Bicategories.ComprehensionCat.LocalProperty.LocalProperties.
Require Import UniMath.Bicategories.ComprehensionCat.LocalProperty.DFLCompCatWithProp.
Require Import UniMath.Bicategories.ComprehensionCat.LocalProperty.CatWithProp.

Local Open Scope cat.
Local Open Scope comp_cat.

Section LocalPropertyBiequiv.
  Context (P : local_property).

1. The extended pseudofunctor from categories to comprehension categories

  Definition local_property_in_cod
             (C : univ_cat_with_finlim)
             (H : P C)
    : fiberwise_cat_property P (finlim_to_dfl_comp_cat C).
  Show proof.
    use make_fiberwise_cat_property.
    - intro Γ.
      use (cat_property_ob_adj_equiv_f' P _ _ (local_property_slice P C Γ H)).
      + apply functor_identity.
      + apply identity_functor_is_adj_equivalence.
    - intros Γ₁ Γ₂ s ; cbn.
      use (cat_property_functor_nat_z_iso_adj_equiv_f'
             P
             _ _
             _ _
             _
             (local_property_pb P H s)).
      + apply functor_identity.
      + apply functor_identity.
      + apply identity_functor_is_adj_equivalence.
      + apply identity_functor_is_adj_equivalence.
      + exact (nat_z_iso_id (slice_univ_cat_pb_finlim s)).

  Proposition local_property_in_cod_functor
              {C₁ C₂ : univ_cat_with_finlim}
              {F : functor_finlim C₁ C₂}
              {H₁ : P C₁}
              {H₂ : P C₂}
              (HF : cat_property_functor P H₁ H₂ F)
    : fiberwise_cat_property_functor
        (finlim_to_dfl_comp_cat_functor F)
        (local_property_in_cod _ H₁)
        (local_property_in_cod _ H₂).
  Show proof.
    intro Γ.
    use (cat_property_functor_nat_z_iso_adj_equiv_f'
           P
           _ _
           _ _
           _
           (local_property_fiber_functor P _ _ _ HF Γ)).
    - apply functor_identity.
    - apply functor_identity.
    - apply identity_functor_is_adj_equivalence.
    - apply identity_functor_is_adj_equivalence.
    - exact (nat_z_iso_id (slice_univ_cat_fiber F Γ)).

  Definition finlim_biequiv_dfl_comp_cat_disp_psfunctor_local_property
    : disp_psfunctor
        (disp_bicat_of_univ_cat_with_cat_property P)
        (disp_bicat_of_cat_property_dfl_full_comp_cat P)
        finlim_biequiv_dfl_comp_cat_psfunctor.
  Show proof.
    use make_disp_psfunctor_contr.
    - apply disp_2cells_iscontr_disp_bicat_of_cat_property_dfl_full_comp_cat.
    - exact (λ C H, local_property_in_cod C (pr1 H) ,, tt).
    - exact (λ _ _ _ _ _ HF, tt ,, local_property_in_cod_functor (pr2 HF)).

2. The extended pseudofunctor from comprehension categories to categories

  Definition local_property_in_dfl_comp_cat
             (C : dfl_full_comp_cat)
             (H : fiberwise_cat_property P C)
    : P (dfl_full_comp_cat_to_finlim C).
  Show proof.
    refine (cat_property_ob_adj_equiv_f' P _ _ (H _)).
    apply (dfl_full_comp_cat_adjequiv_base C).

  Definition local_property_in_dfl_comp_cat_functor
             {C₁ C₂ : dfl_full_comp_cat}
             {F : dfl_full_comp_cat_functor C₁ C₂}
             {H₁ : fiberwise_cat_property P C₁}
             {H₂ : fiberwise_cat_property P C₂}
             (HF : fiberwise_cat_property_functor F H₁ H₂)
    : cat_property_functor
        P
        (local_property_in_dfl_comp_cat C₁ H₁)
        (local_property_in_dfl_comp_cat C₂ H₂)
        (dfl_functor_comp_cat_to_finlim_functor F).
  Show proof.
    refine (cat_property_functor_nat_z_iso_adj_equiv_f'
              P
              _ _
              _ _
              _
              (HF [])).
    - refine (comp_adj_equivalence_of_cats _ _).
      + apply dfl_full_comp_cat_adjequiv_empty.
      + apply cod_fib_terminal.
    - pose (T := make_Terminal _ (comp_cat_functor_terminal F [] (pr2 []))).
      refine (comp_adj_equivalence_of_cats _ _).
      + exact (dfl_full_comp_cat_adjequiv_terminal C₂ T).
      + exact (cod_fib_terminal T).
    - apply (dfl_functor_nat_z_iso F).

  Definition dfl_comp_cat_to_finlim_disp_psfunctor_local_property
    : disp_psfunctor
        (disp_bicat_of_cat_property_dfl_full_comp_cat P)
        (disp_bicat_of_univ_cat_with_cat_property P)
        dfl_comp_cat_to_finlim_psfunctor.
  Show proof.
    use make_disp_psfunctor_contr.
    - apply disp_2cells_iscontr_disp_bicat_of_univ_cat_with_cat_property.
    - exact (λ C H, local_property_in_dfl_comp_cat C (pr1 H) ,, tt).
    - refine (λ _ _ _ _ _ HF, tt ,, local_property_in_dfl_comp_cat_functor _).
      exact (pr2 HF).

3. The unit

  Definition finlim_dfl_comp_cat_unit_local_property
    : disp_pstrans
        (disp_pseudo_comp
           _ _ _ _ _
           finlim_biequiv_dfl_comp_cat_disp_psfunctor_local_property
           dfl_comp_cat_to_finlim_disp_psfunctor_local_property)
        (disp_pseudo_id _)
        finlim_dfl_comp_cat_unit.
  Show proof.
    use make_disp_pstrans_contr.
    - apply disp_2cells_iscontr_disp_bicat_of_univ_cat_with_cat_property.
    - intros C H.
      refine (tt ,, _).
      use cat_property_adj_equivalence_of_cats ; cbn.
      apply identity_functor_is_adj_equivalence.

  Definition finlim_dfl_comp_cat_unit_local_property_pointwise_adjequiv
             {C : univ_cat_with_finlim}
             (HC : disp_bicat_of_univ_cat_with_cat_property P C)
    : disp_left_adjoint_equivalence
        (finlim_dfl_comp_cat_unit_pointwise_equiv C)
        (finlim_dfl_comp_cat_unit_local_property C HC).
  Show proof.
    use disp_adjoint_equiv_disp_bicat_of_univ_cat_with_cat_property.

  Definition finlim_dfl_comp_cat_unit_inv_local_property
    : disp_pstrans
        (disp_pseudo_id _)
        (disp_pseudo_comp
           _ _ _ _ _
           finlim_biequiv_dfl_comp_cat_disp_psfunctor_local_property
           dfl_comp_cat_to_finlim_disp_psfunctor_local_property)
        finlim_dfl_comp_cat_unit_inv.
  Show proof.
    use make_disp_pstrans_inv_contr.
    - apply disp_2cells_iscontr_disp_bicat_of_univ_cat_with_cat_property.
    - apply finlim_dfl_comp_cat_unit_local_property.
    - intros.
      apply finlim_dfl_comp_cat_unit_local_property_pointwise_adjequiv.

4. The counit

  Definition finlim_dfl_comp_cat_counit_local_property
    : disp_pstrans
        (disp_pseudo_id _)
        (disp_pseudo_comp
           _ _ _ _ _
           dfl_comp_cat_to_finlim_disp_psfunctor_local_property
           finlim_biequiv_dfl_comp_cat_disp_psfunctor_local_property)
        finlim_dfl_comp_cat_counit.
  Show proof.
    use make_disp_pstrans_contr.
    - apply disp_2cells_iscontr_disp_bicat_of_cat_property_dfl_full_comp_cat.
    - refine (λ C H, tt ,, _).
      intro x ; cbn.
      use (cat_property_adj_equivalence_of_cats' P).
      exact (fiber_functor_comprehension_adj_equiv C x).

  Definition finlim_dfl_comp_cat_counit_local_property_pointwise_adjequiv
             {C : dfl_full_comp_cat}
             (HC : disp_bicat_of_cat_property_dfl_full_comp_cat P C)
    : disp_left_adjoint_equivalence
        (finlim_dfl_comp_cat_counit_pointwise_equiv C)
        (finlim_dfl_comp_cat_counit_local_property C HC).
  Show proof.
    use disp_adjoint_equiv_disp_bicat_of_cat_property_dfl_full_comp_cat.

  Definition finlim_dfl_comp_cat_counit_inv_local_property
    : disp_pstrans
        (disp_pseudo_comp
           _ _ _ _ _
           dfl_comp_cat_to_finlim_disp_psfunctor_local_property
           finlim_biequiv_dfl_comp_cat_disp_psfunctor_local_property)
        (disp_pseudo_id _)
        finlim_dfl_comp_cat_counit_inv.
  Show proof.
    use make_disp_pstrans_inv_contr.
    - apply disp_2cells_iscontr_disp_bicat_of_cat_property_dfl_full_comp_cat.
    - apply finlim_dfl_comp_cat_counit_local_property.
    - intros.
      apply finlim_dfl_comp_cat_counit_local_property_pointwise_adjequiv.

5. The displayed biequivalence

  Definition finlim_dfl_comp_cat_biequivalence_unit_counit_local_property
    : is_disp_biequivalence_unit_counit
        _ _
        finlim_dfl_comp_cat_biequivalence_unit_counit
        finlim_biequiv_dfl_comp_cat_disp_psfunctor_local_property
        dfl_comp_cat_to_finlim_disp_psfunctor_local_property.
  Show proof.
    simple refine (_ ,, _).
    - exact finlim_dfl_comp_cat_unit_local_property.
    - exact finlim_dfl_comp_cat_counit_inv_local_property.

  Definition finlim_biequiv_dfl_comp_cat_psfunctor_local_property
    : disp_is_biequivalence_data
        _
        _
        finlim_dfl_comp_cat_biequivalence_adjoints
        finlim_dfl_comp_cat_biequivalence_unit_counit_local_property.
  Show proof.
    simple refine (_ ,, _ ,, (_ ,, _) ,, (_ ,, _)).
    - exact finlim_dfl_comp_cat_unit_inv_local_property.
    - exact finlim_dfl_comp_cat_counit_local_property.
    - use make_disp_invmodification_contr.
      apply disp_2cells_iscontr_disp_bicat_of_univ_cat_with_cat_property.
    - use make_disp_invmodification_contr.
      apply disp_2cells_iscontr_disp_bicat_of_univ_cat_with_cat_property.
    - use make_disp_invmodification_contr.
      apply disp_2cells_iscontr_disp_bicat_of_cat_property_dfl_full_comp_cat.
    - use make_disp_invmodification_contr.
      apply disp_2cells_iscontr_disp_bicat_of_cat_property_dfl_full_comp_cat.
End LocalPropertyBiequiv.