Library UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell

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.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Import DispBicat.Notations.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions.
Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma.

Local Open Scope cat.

1. Subbicategory by selecting 1-cells
Section Sub1CellBicategory.
  Context (B : bicat)
          (P : ∏ (x y : B), x --> y -> UU)
          (Pid : ∏ (x : B), P _ _ (id₁ x))
          (Pcomp : ∏ (x y z : B) (f : x --> y) (g : y --> z),
                   P _ _ f → P _ _ g → P _ _ (f · g)).

  Definition disp_sub1cell_disp_cat
    : disp_cat_ob_mor B.
  Show proof.
    use make_disp_cat_ob_mor.
    - exact (λ _, unit).
    - exact (λ _ _ _ _ f, P _ _ f).

  Definition disp_sub1cell_disp_cat_id_comp
    : disp_cat_id_comp _ disp_sub1cell_disp_cat.
  Show proof.
    use tpair.
    - exact (λ _ _, Pid _).
    - exact (λ _ _ _ _ _ _ _ _ p q, Pcomp _ _ _ _ _ p q).

  Definition disp_sub1cell_disp_cat_data
    : disp_cat_data B.
  Show proof.
    use tpair.
    - exact disp_sub1cell_disp_cat.
    - exact disp_sub1cell_disp_cat_id_comp.

  Definition disp_sub1cell_prebicat : disp_prebicat B
    := disp_cell_unit_bicat disp_sub1cell_disp_cat_data.

  Definition disp_sub1cell_bicat : disp_bicat B
    := disp_cell_unit_bicat disp_sub1cell_disp_cat_data.

  Definition disp_2cells_isaprop_sub1cell_bicat : disp_2cells_isaprop disp_sub1cell_bicat.
  Show proof.
    apply disp_2cells_isaprop_cell_unit_bicat.

  Definition disp_locally_groupoid_sub1cell_bicat
    : disp_locally_groupoid disp_sub1cell_bicat.
  Show proof.
    apply disp_locally_groupoid_cell_unit_bicat.

  Definition disp_sub1cell_univalent_2_1
             (HP : ∏ (x y : B) (f : x --> y), isaprop (P _ _ f))
    : disp_univalent_2_1 disp_sub1cell_bicat.
  Show proof.
    use disp_cell_unit_bicat_univalent_2_1.
    intros.
    apply HP.

  Definition disp_sub1cell_univalent_2_0
             (HB : is_univalent_2_1 B)
             (HP : ∏ (x y : B) (f : x --> y), isaprop (P _ _ f))
    : disp_univalent_2_0 disp_sub1cell_bicat.
  Show proof.
    use disp_cell_unit_bicat_univalent_2_0.
    - exact HB.
    - intros ; apply HP.
    - simpl ; intro.
      apply isasetunit.
    - simpl.
      intros.
      apply isapropunit.

  Definition disp_sub1cell_univalent_2
             (HB : is_univalent_2_1 B)
             (HP : ∏ (x y : B) (f : x --> y), isaprop (P _ _ f))
    : disp_univalent_2 disp_sub1cell_bicat.
  Show proof.
    split.
    - use disp_sub1cell_univalent_2_0.
      + exact HB.
      + exact HP.
    - use disp_sub1cell_univalent_2_1.
      exact HP.

  Definition sub1cell_bicat
    : bicat
    := total_bicat disp_sub1cell_bicat.

  Definition is_univalent_2_1_sub1cell_bicat
             (HB : is_univalent_2_1 B)
             (HP : ∏ (x y : B) (f : x --> y), isaprop (P _ _ f))
    : is_univalent_2_1 sub1cell_bicat.
  Show proof.
    use total_is_univalent_2_1.
    - exact HB.
    - use disp_sub1cell_univalent_2_1.
      exact HP.

  Definition is_univalent_2_0_sub1cell_bicat
             (HB : is_univalent_2 B)
             (HP : ∏ (x y : B) (f : x --> y), isaprop (P _ _ f))
    : is_univalent_2_0 sub1cell_bicat.
  Show proof.
    use total_is_univalent_2_0.
    - exact (pr1 HB).
    - use disp_sub1cell_univalent_2_0.
      + exact (pr2 HB).
      + exact HP.

  Definition is_univalent_2_sub1cell_bicat
             (HB : is_univalent_2 B)
             (HP : ∏ (x y : B) (f : x --> y), isaprop (P _ _ f))
    : is_univalent_2 sub1cell_bicat.
  Show proof.
    split.
    - use is_univalent_2_0_sub1cell_bicat.
      + exact HB.
      + exact HP.
    - use is_univalent_2_1_sub1cell_bicat.
      + exact (pr2 HB).
      + exact HP.
End Sub1CellBicategory.

2. Subbicategory by selecting both 0-cells and 1-cells
Section SubBicategory.
  Context {B : bicat}
          (P₀ : B → UU)
          (P₁ : ∏ (x y : B), P₀ x → P₀ y → x --> y -> UU)
          (P₁id : ∏ (x : B) (Px : P₀ x), P₁ _ _ Px Px (id₁ x))
          (P₁comp : ∏ (x y z : B)
                      (Px : P₀ x)
                      (Py : P₀ y)
                      (Pz : P₀ z)
                      (f : x --> y) (g : y --> z),
              P₁ _ _ Px Py f
              → P₁ _ _ Py Pz g
              → P₁ _ _ Px Pz (f · g)).

  Definition disp_subbicat : disp_bicat B
    := sigma_bicat
         _
         _
         (disp_sub1cell_bicat
            (total_bicat (disp_fullsubbicat B P₀))
            (λ x y f, P₁ (pr1 x) (pr1 y) (pr2 x) (pr2 y) (pr1 f))
            (λ x, P₁id (pr1 x) (pr2 x))
            (λ x y z f g Pf Pg, P₁comp _ _ _ _ _ _ _ _ Pf Pg)).

  Definition disp_2cells_isaprop_subbicat
    : disp_2cells_isaprop disp_subbicat.
  Show proof.
    apply disp_2cells_isaprop_sigma.
    - apply disp_2cells_isaprop_fullsubbicat.
    - apply disp_2cells_isaprop_sub1cell_bicat.

  Definition disp_locally_groupoid_subbicat
             (HB : is_univalent_2 B)
    : disp_locally_groupoid disp_subbicat.
  Show proof.
    use disp_locally_groupoid_sigma.
    - exact HB.
    - apply disp_2cells_isaprop_fullsubbicat.
    - apply disp_2cells_isaprop_sub1cell_bicat.
    - apply disp_locally_groupoid_fullsubbicat.
    - apply disp_locally_groupoid_sub1cell_bicat.

  Definition disp_subbicat_univalent_2_1
             (HP₁ : ∏ (x y : B)
                      (Px : P₀ x)
                      (Py : P₀ y)
                      (f : x --> y),
                    isaprop (P₁ x y Px Py f))
    : disp_univalent_2_1 disp_subbicat.
  Show proof.
    use sigma_disp_univalent_2_1_with_props.
    - apply disp_2cells_isaprop_fullsubbicat.
    - apply disp_2cells_isaprop_sub1cell_bicat.
    - apply disp_fullsubbicat_univalent_2_1.
    - apply disp_sub1cell_univalent_2_1.
      intros.
      apply HP₁.

  Definition disp_subbicat_univalent_2_0
             (HB : is_univalent_2 B)
             (HP₀ : ∏ (x : B), isaprop (P₀ x))
             (HP₁ : ∏ (x y : B)
                      (Px : P₀ x)
                      (Py : P₀ y)
                      (f : x --> y),
                    isaprop (P₁ x y Px Py f))
    : disp_univalent_2_0 disp_subbicat.
  Show proof.
    use sigma_disp_univalent_2_0_with_props.
    - exact HB.
    - apply disp_2cells_isaprop_fullsubbicat.
    - apply disp_2cells_isaprop_sub1cell_bicat.
    - apply disp_fullsubbicat_univalent_2_1.
    - apply disp_sub1cell_univalent_2_1.
      intros.
      apply HP₁.
    - apply disp_locally_groupoid_fullsubbicat.
    - apply disp_locally_groupoid_sub1cell_bicat.
    - use disp_univalent_2_0_fullsubbicat.
      + exact HB.
      + exact HP₀.
    - apply disp_sub1cell_univalent_2_0.
      + use total_is_univalent_2_1.
        * apply HB.
        * apply disp_fullsubbicat_univalent_2_1.
      + intros.
        apply HP₁.

  Definition subbicat
    : bicat
    := total_bicat disp_subbicat.

  Definition eq_2cell_subbicat
             {x y : subbicat}
             {f g : x --> y}
             {α β : f ==> g}
             (p : pr1 α = pr1 β)
    : α = β.
  Show proof.
    use subtypePath.
    {
      intro.
      simpl.
      apply isapropdirprod ; apply isapropunit.
    }
    exact p.

  Definition is_invertible_2cell_subbicat
             {x y : subbicat}
             {f g : x --> y}
             (α : f ==> g)
             (Hα : is_invertible_2cell (pr1 α))
    : is_invertible_2cell α.
  Show proof.
    use make_is_invertible_2cell.
    - exact (Hα^-1 ,, tt ,, tt).
    - abstract
        (use eq_2cell_subbicat ;
         apply vcomp_rinv).
    - abstract
        (use eq_2cell_subbicat ;
         apply vcomp_linv).

  Definition invertible_2cell_subbicat
             {x y : subbicat}
             {f g : x --> y}
             (Hα : invertible_2cell (pr1 f) (pr1 g))
    : invertible_2cell f g.
  Show proof.
    use make_invertible_2cell.
    - exact (pr1 Hα ,, tt ,, tt).
    - use is_invertible_2cell_subbicat.
      exact Hα.

  Definition from_is_invertible_2cell_subbicat
             {x y : subbicat}
             {f g : x --> y}
             (α : f ==> g)
             (Hα : is_invertible_2cell α)
    : is_invertible_2cell (pr1 α).
  Show proof.
    use make_is_invertible_2cell.
    - exact (pr1 (Hα^-1)).
    - abstract
        (exact (maponpaths pr1 (vcomp_rinv Hα))).
    - abstract
        (exact (maponpaths pr1 (vcomp_linv Hα))).

  Definition from_invertible_2cell_subbicat
             {x y : subbicat}
             {f g : x --> y}
             (Hα : invertible_2cell f g)
    : invertible_2cell (pr1 f) (pr1 g).
  Show proof.
    use make_invertible_2cell.
    - exact (pr11 Hα).
    - use from_is_invertible_2cell_subbicat.
      exact Hα.

  Definition is_univalent_2_1_subbicat
             (HB : is_univalent_2_1 B)
             (HP₁ : ∏ (x y : B)
                      (Px : P₀ x)
                      (Py : P₀ y)
                      (f : x --> y),
                    isaprop (P₁ x y Px Py f))
    : is_univalent_2_1 subbicat.
  Show proof.
    use total_is_univalent_2_1.
    - exact HB.
    - use disp_subbicat_univalent_2_1.
      exact HP₁.

  Definition is_univalent_2_0_subbicat
             (HB : is_univalent_2 B)
             (HP₀ : ∏ (x : B), isaprop (P₀ x))
             (HP₁ : ∏ (x y : B)
                      (Px : P₀ x)
                      (Py : P₀ y)
                      (f : x --> y),
                    isaprop (P₁ x y Px Py f))
    : is_univalent_2_0 subbicat.
  Show proof.
    use total_is_univalent_2_0.
    - exact (pr1 HB).
    - use disp_subbicat_univalent_2_0.
      + exact HB.
      + exact HP₀.
      + exact HP₁.

  Definition is_univalent_2_subbicat
             (HB : is_univalent_2 B)
             (HP₀ : ∏ (x : B), isaprop (P₀ x))
             (HP₁ : ∏ (x y : B)
                      (Px : P₀ x)
                      (Py : P₀ y)
                      (f : x --> y),
                    isaprop (P₁ x y Px Py f))
    : is_univalent_2 subbicat.
  Show proof.
    split.
    - use is_univalent_2_0_subbicat.
      + exact HB.
      + exact HP₀.
      + exact HP₁.
    - use is_univalent_2_1_subbicat.
      + exact (pr2 HB).
      + exact HP₁.
End SubBicategory.