Library UniMath.Bicategories.ComprehensionCat.LocalProperty.LocalProperties

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.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Preservation.
Require Import UniMath.CategoryTheory.Limits.PreservationProperties.
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.DisplayedCats.Codomain.CodLimits.
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.ComprehensionCat.BicatOfCompCat.
Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat.

Local Open Scope cat.

1. Properties of categories

Definition cat_property_data
  : UU
  := ∑ (P₀ : univ_cat_with_finlim → UU),
     ∏ (C₁ C₂ : univ_cat_with_finlim),
     P₀ C₁ → P₀ C₂ → functor_finlim C₁ C₂ → UU.

Definition make_cat_property_data
           (P₀ : univ_cat_with_finlim → UU)
           (P₁ : ∏ (C₁ C₂ : univ_cat_with_finlim),
                 P₀ C₁ → P₀ C₂ → functor_finlim C₁ C₂ → UU)
  : cat_property_data
  := P₀ ,, P₁.

Definition cat_property_ob
           (P : cat_property_data)
           (C : univ_cat_with_finlim)
  : UU
  := pr1 P C.

Coercion cat_property_ob : cat_property_data >-> Funclass.

Definition cat_property_functor
           (P : cat_property_data)
           {C₁ C₂ : univ_cat_with_finlim}
           (H₁ : P C₁)
           (H₂ : P C₂)
           (F : functor_finlim C₁ C₂)
  : UU
  := pr2 P C₁ C₂ H₁ H₂ F.

Definition cat_property_laws
           (P : cat_property_data)
  : UU
  := (∏ (C : univ_cat_with_finlim),
      isaprop (P C))
     ×
     (∏ (C₁ C₂ : univ_cat_with_finlim)
        (H₁ : P C₁)
        (H₂ : P C₂)
        (F : functor_finlim C₁ C₂),
      isaprop (cat_property_functor P H₁ H₂ F))
     ×
     (∏ (C : univ_cat_with_finlim)
        (H : P C),
      cat_property_functor P H H (identity C))
     ×
     (∏ (C₁ C₂ C₃ : univ_cat_with_finlim)
        (H₁ : P C₁)
        (H₂ : P C₂)
        (H₃ : P C₃)
        (F : functor_finlim C₁ C₂)
        (G : functor_finlim C₂ C₃),
      cat_property_functor P H₁ H₂ F
      →
      cat_property_functor P H₂ H₃ G
      →
      cat_property_functor P H₁ H₃ (F · G)).

Definition cat_property
  : UU
  := ∑ (P : cat_property_data), cat_property_laws P.

Definition make_cat_property
           (P : cat_property_data)
           (H : cat_property_laws P)
  : cat_property
  := P ,, H.

Coercion cat_property_to_data
         (P : cat_property)
  : cat_property_data.
Show proof.
  exact (pr1 P).

Section CatPropertyLaws.
  Context (P : cat_property).

  Proposition isaprop_cat_property_ob
              (C : univ_cat_with_finlim)
    : isaprop (P C).
  Show proof.
    exact (pr1 (pr2 P) C).

  Proposition isaprop_cat_property_functor
              {C₁ C₂ : univ_cat_with_finlim}
              (H₁ : P C₁)
              (H₂ : P C₂)
              (F : functor_finlim C₁ C₂)
    : isaprop (cat_property_functor P H₁ H₂ F).
  Show proof.
    exact (pr12 (pr2 P) C₁ C₂ H₁ H₂ F).

  Proposition cat_property_id_functor
              {C : univ_cat_with_finlim}
              (H : P C)
    : cat_property_functor P H H (identity C).
  Show proof.
    exact (pr122 (pr2 P) C H).

  Proposition cat_property_id_functor'
              {C : univ_cat_with_finlim}
              (H H' : P C)
    : cat_property_functor P H H' (identity C).
  Show proof.
    assert (H = H') as p.
    {
      apply isaprop_cat_property_ob.
    }
    induction p.
    apply cat_property_id_functor.

  Proposition cat_property_comp_functor
              {C₁ C₂ C₃ : univ_cat_with_finlim}
              {H₁ : P C₁}
              {H₂ : P C₂}
              {H₃ : P C₃}
              {F : functor_finlim C₁ C₂}
              {G : functor_finlim C₂ C₃}
              (HF : cat_property_functor P H₁ H₂ F)
              (HG : cat_property_functor P H₂ H₃ G)
    : cat_property_functor P H₁ H₃ (F · G).
  Show proof.
    exact (pr222 (pr2 P) C₁ C₂ C₃ H₁ H₂ H₃ F G HF HG).

  Proposition cat_property_adj_equiv
              {C₁ C₂ : univ_cat_with_finlim}
              (F : adjoint_equivalence C₁ C₂)
              (H₁ : P C₁)
              (H₂ : P C₂)
    : cat_property_functor P H₁ H₂ (pr1 F).
  Show proof.
    revert C₁ C₂ F H₁ H₂.
    use J_2_0.
    {
      exact is_univalent_2_0_bicat_of_univ_cat_with_finlim.
    }
    intros C H₁ H₂.
    apply cat_property_id_functor'.

  Proposition cat_property_adj_equivalence_of_cats
              {C₁ C₂ : univ_cat_with_finlim}
              (F : functor_finlim C₁ C₂)
              (HF : adj_equivalence_of_cats (pr1 F))
              (H₁ : P C₁)
              (H₂ : P C₂)
    : cat_property_functor P H₁ H₂ F.
  Show proof.
    refine (cat_property_adj_equiv (F ,, _) H₁ H₂).
    use left_adjoint_equivalence_univ_cat_with_finlim.
    exact HF.

  Proposition cat_property_adj_equivalence_of_cats'
              {C₁ C₂ : univ_cat_with_finlim}
              (F : functor_finlim C₁ C₂)
              (HF : adj_equivalence_of_cats (pr1 F))
              (H₁ : P C₁)
              (H₂ : P C₂)
    : cat_property_functor P H₁ H₂ F.
  Show proof.
    exact (@cat_property_adj_equivalence_of_cats
              _ _
              F
              HF
              H₁
              H₂).

  Proposition cat_property_ob_adj_equiv_f_help
              {C₁ C₂ : univ_cat_with_finlim}
              (F : adjoint_equivalence C₁ C₂)
              (H : P C₁)
    : P C₂.
  Show proof.
    revert C₁ C₂ F H.
    use J_2_0.
    {
      exact is_univalent_2_0_bicat_of_univ_cat_with_finlim.
    }
    intros C H.
    exact H.

  Proposition cat_property_ob_left_adjoint_equivalence_f
              {C₁ C₂ : univ_cat_with_finlim}
              (F : functor_finlim C₁ C₂)
              (HF : left_adjoint_equivalence F)
              (H : P C₁)
    : P C₂.
  Show proof.
    use (cat_property_ob_adj_equiv_f_help _ H).
    exact (F ,, HF).

  Proposition cat_property_ob_adj_equiv_f
              {C₁ C₂ : univ_cat_with_finlim}
              (F : functor_finlim C₁ C₂)
              (HF : adj_equivalence_of_cats (pr1 F))
              (H : P C₁)
    : P C₂.
  Show proof.
    use (cat_property_ob_left_adjoint_equivalence_f _ _ H).
    - exact F.
    - use left_adjoint_equivalence_univ_cat_with_finlim.
      exact HF.

  Proposition cat_property_ob_adj_equiv_f'
              {C₁ C₂ : univ_cat_with_finlim}
              (F : (C₁ : category) ⟶ C₂)
              (HF : adj_equivalence_of_cats F)
              (H : P C₁)
    : P C₂.
  Show proof.
    use (cat_property_ob_left_adjoint_equivalence_f _ _ H).
    - exact (make_functor_finlim_adjequiv F HF).
    - use left_adjoint_equivalence_univ_cat_with_finlim.
      exact HF.

  Proposition cat_property_functor_nat_z_iso_f_help
              {C₁ C₂ : univ_cat_with_finlim}
              {H₁ : P C₁}
              {H₂ : P C₂}
              {F G : functor_finlim C₁ C₂}
              (τ : invertible_2cell F G)
              (HF : cat_property_functor P H₁ H₂ F)
    : cat_property_functor P H₁ H₂ G.
  Show proof.
    revert C₁ C₂ F G τ H₁ H₂ HF.
    use J_2_1.
    {
      exact is_univalent_2_1_bicat_of_univ_cat_with_finlim.
    }
    intros C₁ C₂ F H₁ H₂ HF.
    exact HF.

  Proposition cat_property_functor_nat_z_iso_f
              {C₁ C₂ : univ_cat_with_finlim}
              {H₁ : P C₁}
              {H₂ : P C₂}
              {F G : functor_finlim C₁ C₂}
              (τ : nat_z_iso (pr1 F) (pr1 G))
              (HF : cat_property_functor P H₁ H₂ F)
    : cat_property_functor P H₁ H₂ G.
  Show proof.
    use (cat_property_functor_nat_z_iso_f_help _ HF).
    use invertible_2cell_cat_with_finlim.
    exact τ.

  Proposition cat_property_functor_nat_z_iso_adj_equiv_f_help
              {C₁ C₂ D₁ D₂ : univ_cat_with_finlim}
              {HC₁ : P C₁}
              {HC₂ : P C₂}
              {HD₁ : P D₁}
              {HD₂ : P D₂}
              (EC : adjoint_equivalence C₁ C₂)
              (ED : adjoint_equivalence D₁ D₂)
              (F : functor_finlim C₁ D₁)
              (G : functor_finlim C₂ D₂)
              (τ : nat_z_iso (pr1 F ∙ pr11 ED) (pr11 EC ∙ pr1 G))
              (HF : cat_property_functor P HC₁ HD₁ F)
    : cat_property_functor P HC₂ HD₂ G.
  Show proof.
    revert C₁ C₂ EC D₁ D₂ ED HC₁ HC₂ HD₁ HD₂ F G τ HF.
    use J_2_0.
    {
      exact is_univalent_2_0_bicat_of_univ_cat_with_finlim.
    }
    intros C.
    use J_2_0.
    {
      exact is_univalent_2_0_bicat_of_univ_cat_with_finlim.
    }
    intros D HC₁ HC₂ HD₁ HD₂ F G τ HF.
    assert (HC₁ = HC₂) as p.
    {
      apply isaprop_cat_property_ob.
    }
    induction p.
    assert (HD₁ = HD₂) as p.
    {
      apply isaprop_cat_property_ob.
    }
    induction p.
    use (cat_property_functor_nat_z_iso_f τ).
    cbn.
    refine (transportf _ _ HF).
    apply idpath.

  Proposition cat_property_functor_nat_z_iso_adj_equiv_f
              {C₁ C₂ D₁ D₂ : univ_cat_with_finlim}
              {HC₁ : P C₁}
              {HC₂ : P C₂}
              {HD₁ : P D₁}
              {HD₂ : P D₂}
              {EC : functor_finlim C₁ C₂} {ED : functor_finlim D₁ D₂}
              (HEC : adj_equivalence_of_cats (pr1 EC))
              (HED : adj_equivalence_of_cats (pr1 ED))
              (F : functor_finlim C₁ D₁)
              (G : functor_finlim C₂ D₂)
              (τ : nat_z_iso (pr1 F ∙ pr1 ED) (pr1 EC ∙ pr1 G))
              (HF : cat_property_functor P HC₁ HD₁ F)
    : cat_property_functor P HC₂ HD₂ G.
  Show proof.
    refine (cat_property_functor_nat_z_iso_adj_equiv_f_help (EC ,, _) (ED ,, _) _ _ τ HF).
    - use left_adjoint_equivalence_univ_cat_with_finlim.
      exact HEC.
    - use left_adjoint_equivalence_univ_cat_with_finlim.
      exact HED.

  Proposition cat_property_functor_nat_z_iso_adj_equiv_f'
              {C₁ C₂ D₁ D₂ : univ_cat_with_finlim}
              {HC₁ : P C₁}
              {HC₂ : P C₂}
              {HD₁ : P D₁}
              {HD₂ : P D₂}
              {EC : functor C₁ C₂} {ED : functor D₁ D₂}
              (HEC : adj_equivalence_of_cats EC)
              (HED : adj_equivalence_of_cats ED)
              (F : functor_finlim C₁ D₁)
              (G : functor_finlim C₂ D₂)
              (τ : nat_z_iso (pr1 F ∙ ED) (EC ∙ pr1 G))
              (HF : cat_property_functor P HC₁ HD₁ F)
    : cat_property_functor P HC₂ HD₂ G.
  Show proof.
    exact (cat_property_functor_nat_z_iso_adj_equiv_f
             (EC := make_functor_finlim_adjequiv _ HEC)
             (ED := make_functor_finlim_adjequiv _ HED)
             HEC HED
             F G
             τ
             HF).
End CatPropertyLaws.

2. Fiberwise versions of properties

Definition fiberwise_cat_property
           (P : cat_property)
           (C : dfl_full_comp_cat)
  : UU
  := ∑ (H : ∏ (Γ : C), P (dfl_full_comp_cat_fiber Γ)),
     ∏ (Γ₁ Γ₂ : C)
       (s : Γ₁ --> Γ₂),
     cat_property_functor P (H Γ₂) (H Γ₁) (dfl_full_comp_cat_fiber_functor s).

Definition make_fiberwise_cat_property
           (P : cat_property)
           (C : dfl_full_comp_cat)
           (H : ∏ (Γ : C), P (dfl_full_comp_cat_fiber Γ))
           (H' : ∏ (Γ₁ Γ₂ : C)
                   (s : Γ₁ --> Γ₂),
                 cat_property_functor
                   P
                   (H Γ₂) (H Γ₁)
                   (dfl_full_comp_cat_fiber_functor s))
  : fiberwise_cat_property P C
  := H ,, H'.

Definition fiberwise_cat_property_ob
           {P : cat_property}
           {C : dfl_full_comp_cat}
           (H : fiberwise_cat_property P C)
           (Γ : C)
  : P (dfl_full_comp_cat_fiber Γ)
  := pr1 H Γ.

Coercion fiberwise_cat_property_ob : fiberwise_cat_property >-> Funclass.

Definition fiberwise_cat_property_mor
           {P : cat_property}
           {C : dfl_full_comp_cat}
           (H : fiberwise_cat_property P C)
           {Γ₁ Γ₂ : C}
           (s : Γ₁ --> Γ₂)
  : cat_property_functor
      P
      (H Γ₂) (H Γ₁)
      (dfl_full_comp_cat_fiber_functor s).
Show proof.
  exact (pr2 H Γ₁ Γ₂ s).

Proposition isaprop_fiberwise_cat_property
            {P : cat_property}
            (C : dfl_full_comp_cat)
  : isaprop (fiberwise_cat_property P C).
Show proof.
  use isaproptotal2.
  - intro H.
    do 3 (use impred ; intro).
    apply isaprop_cat_property_functor.
  - intros.
    use funextsec ; intro.
    apply (isaprop_cat_property_ob P).

Proposition cat_property_fiber_functor_id
            (P : cat_property)
            (C : dfl_full_comp_cat)
            (Γ : C)
            (p : P (dfl_full_comp_cat_fiber Γ))
  : cat_property_functor P p p (identity _).
Show proof.
  use (cat_property_functor_nat_z_iso_f
         P
         _
         (cat_property_id_functor P _)).
  apply fiber_functor_identity.

Proposition cat_property_fiber_functor_id'
            (P : cat_property)
            (C : dfl_full_comp_cat)
            (Γ : C)
            (p : P (dfl_full_comp_cat_fiber Γ))
  : cat_property_functor
      P
      p p
      (dfl_full_comp_cat_functor_fiber_functor (identity C) Γ).
Show proof.
  refine (transportf
            (cat_property_functor P p p)
            _
            (cat_property_fiber_functor_id P C Γ p)).
  use subtypePath.
  {
    intro ; simpl.
    repeat (use isapropdirprod).
    - apply isapropunit.
    - apply isaprop_preserves_terminal.
    - apply isapropunit.
    - apply isaprop_preserves_pullback.
  }
  use subtypePath.
  {
    intro.
    apply isaprop_is_functor.
    apply homset_property.
  }
  apply idpath.

Proposition cat_property_fiber_functor_comp
            (P : cat_property)
            {C₁ C₂ C₃ : dfl_full_comp_cat}
            {F : dfl_full_comp_cat_functor C₁ C₂}
            {G : dfl_full_comp_cat_functor C₂ C₃}
            {Γ : C₁}
            {p₁ : P (dfl_full_comp_cat_fiber Γ)}
            {p₂ : P (dfl_full_comp_cat_fiber (F Γ))}
            {p₃ : P (dfl_full_comp_cat_fiber (G(F Γ)))}
            (HF : cat_property_functor P p₁ p₂ (dfl_full_comp_cat_functor_fiber_functor F Γ))
            (HG : cat_property_functor P p₂ p₃ (dfl_full_comp_cat_functor_fiber_functor G (F Γ)))
  : cat_property_functor P p₁ p₃ (dfl_full_comp_cat_functor_fiber_functor (F · G) Γ).
Show proof.
  use (cat_property_functor_nat_z_iso_f
         P
         _
         (cat_property_comp_functor P HF HG)).
  apply fiber_functor_comp_nat_z_iso.

Definition fiberwise_cat_property_functor
           {P : cat_property}
           {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₂)
  : UU
  := ∏ (Γ : C₁),
     cat_property_functor
       P
       (H₁ Γ) (H₂ (F Γ))
       (dfl_full_comp_cat_functor_fiber_functor F Γ).

3. Local properties

Definition slice_univ_cat_with_finlim
           {C : univ_cat_with_finlim}
           (x : C)
  : univ_cat_with_finlim.
Show proof.
  use make_univ_cat_with_finlim.
  - refine (C/x ,, _).
    apply is_univalent_cod_slice.
  - apply codomain_fib_terminal.
  - use codomain_fiberwise_pullbacks.
    exact (pullbacks_univ_cat_with_finlim C).

Definition slice_univ_cat_pb_finlim
           {C : univ_cat_with_finlim}
           {x y : C}
           (f : x --> y)
  : functor_finlim
      (slice_univ_cat_with_finlim y)
      (slice_univ_cat_with_finlim x).
Show proof.
  use make_functor_finlim.
  - exact (cod_pb (pullbacks_univ_cat_with_finlim C) f).
  - apply codomain_fib_preserves_terminal.
  - use preserves_pullback_from_binproduct_equalizer.
    + use codomain_fib_binproducts.
      apply pullbacks_univ_cat_with_finlim.
    + use codomain_fib_equalizer.
      apply equalizers_univ_cat_with_finlim.
    + apply codomain_fib_preserves_binproduct.
    + apply codomain_fib_preserves_equalizer.

Definition slice_univ_cat_fiber
           {C₁ C₂ : univ_cat_with_finlim}
           (F : functor_finlim C₁ C₂)
           (x : C₁)
  : functor_finlim
      (slice_univ_cat_with_finlim x)
      (slice_univ_cat_with_finlim (F x)).
Show proof.
  use make_functor_finlim.
  - exact (fiber_functor (disp_codomain_functor F) x).
  - apply preserves_terminal_fiber_disp_codomain_functor.
  - use preserves_pullback_from_binproduct_equalizer.
    + use codomain_fib_binproducts.
      apply pullbacks_univ_cat_with_finlim.
    + use codomain_fib_equalizer.
      apply equalizers_univ_cat_with_finlim.
    + apply preserves_binproduct_fiber_disp_codomain_functor.
      exact (functor_finlim_preserves_pullback F).
    + use preserves_equalizer_fiber_disp_codomain_functor.
      apply functor_finlim_preserves_equalizer.

Definition is_local_property
           (P : cat_property)
  : UU
  := ∑ (H : ∏ (C : univ_cat_with_finlim) (x : C),
            P C → P (slice_univ_cat_with_finlim x)),
     (∏ (C : univ_cat_with_finlim)
        (p : P C)
        (x y : C)
        (f : x --> y),
      cat_property_functor
        P
        (H C y p) (H C x p)
        (slice_univ_cat_pb_finlim f))
     ×
     (∏ (C₁ C₂ : univ_cat_with_finlim)
        (p₁ : P C₁)
        (p₂ : P C₂)
        (F : functor_finlim C₁ C₂)
        (HF : cat_property_functor P p₁ p₂ F)
        (x : C₁),
      cat_property_functor
        P
        (H C₁ x p₁) (H C₂ (F x) p₂)
        (slice_univ_cat_fiber F x)).

Definition make_is_local_property
           {P : cat_property}
           (H : ∏ (C : univ_cat_with_finlim) (x : C),
                P C → P (slice_univ_cat_with_finlim x))
           (Hpb : ∏ (C : univ_cat_with_finlim)
                    (p : P C)
                    (x y : C)
                    (f : x --> y),
                  cat_property_functor
                    P
                    (H C y p) (H C x p)
                    (slice_univ_cat_pb_finlim f))
           (Hfib : ∏ (C₁ C₂ : univ_cat_with_finlim)
                     (p₁ : P C₁)
                     (p₂ : P C₂)
                     (F : functor_finlim C₁ C₂)
                     (HF : cat_property_functor P p₁ p₂ F)
                     (x : C₁),
                   cat_property_functor
                     P
                     (H C₁ x p₁) (H C₂ (F x) p₂)
                     (slice_univ_cat_fiber F x))
  : is_local_property P
  := H ,, Hpb ,, Hfib.

Definition local_property
  : UU
  := ∑ (P : cat_property), is_local_property P.

Definition make_local_property
           (P : cat_property)
           (H : is_local_property P)
  : local_property
  := P ,, H.

Coercion local_property_to_cat_property
         (P : local_property)
  : cat_property.
Show proof.
  exact (pr1 P).

Section LocalPropertyLaws.
  Context (P : local_property).

  Definition local_property_slice
             (C : univ_cat_with_finlim)
             (x : C)
             (H : P C)
    : P (slice_univ_cat_with_finlim x).
  Show proof.
    exact (pr12 P C x H).

  Definition local_property_pb
             {C : univ_cat_with_finlim}
             (p : P C)
             {x y : C}
             (f : x --> y)
    : cat_property_functor
        P
        (local_property_slice C y p) (local_property_slice C x p)
        (slice_univ_cat_pb_finlim f).
  Show proof.
    exact (pr122 P C p x y f).

  Definition local_property_fiber_functor
             {C₁ C₂ : univ_cat_with_finlim}
             (p₁ : P C₁)
             (p₂ : P C₂)
             (F : functor_finlim C₁ C₂)
             (HF : cat_property_functor P p₁ p₂ F)
             (x : C₁)
    : cat_property_functor
        P
        (local_property_slice C₁ x p₁) (local_property_slice C₂ (F x) p₂)
        (slice_univ_cat_fiber F x).
  Show proof.
    exact (pr222 P C₁ C₂ p₁ p₂ F HF x).
End LocalPropertyLaws.