Library UniMath.Bicategories.DisplayedBicats.Examples.DispDepProd

Dependent product of diplayed bicategories. If we have a type `J` and a family indexed by `J` of displayed bicategories on `J`, then we can assemble this into a displayed bicategory whose objects are dependent functions.
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.DisplayedBicats.DispUnivalence.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Core.Univalence.

Local Open Scope cat.
Local Open Scope mor_disp.

Section DispDepprod.
  Context {B : bicat}
          (I : UU)
          (D : I → disp_bicat B).

  Definition disp_depprod_cat_ob_mor : disp_cat_ob_mor B.
  Show proof.
    use tpair.
    - exact (λ x, ∏ (i : I), D i x).
    - exact (λ x y xx yy f, ∏ (i : I), xx i -->[ f ] yy i).

  Definition disp_depprod_cat_data : disp_cat_data B.
  Show proof.
    use tpair.
    - exact disp_depprod_cat_ob_mor.
    - split.
      + exact (λ x xx i, id_disp (xx i)).
      + exact (λ x y z f g xx yy zz ff gg i, ff i;;gg i).

  Definition disp_depprod_disp_2cell_struct
    : disp_2cell_struct disp_depprod_cat_ob_mor
    := λ x y f g α xx yy ff gg, ∏ (i : I), ff i ==>[ α ] gg i.

  Definition disp_depprod_disp_prebicat_ops
    : disp_prebicat_ops (disp_depprod_cat_data,, disp_depprod_disp_2cell_struct).
  Show proof.
    repeat split.
    - exact (λ a b f aa bb ff i, disp_id2 (ff i)).
    - exact (λ a b f aa bb ff i, disp_lunitor (ff i)).
    - exact (λ a b f aa bb ff i, disp_runitor (ff i)).
    - exact (λ a b f aa bb ff i, disp_linvunitor (ff i)).
    - exact (λ a b f aa bb ff i, disp_rinvunitor (ff i)).
    - exact (λ a b c d f g h aa bb cc dd ff gg hh i,
             disp_rassociator (ff i) (gg i) (hh i)).
    - exact (λ a b c d f g h aa bb cc dd ff gg hh i,
             disp_lassociator (ff i) (gg i) (hh i)).
    - exact (λ a b f g h x y aa bb ff gg hh xx yy i, xx i •• yy i).
    - exact (λ a b c f g1 g2 x aa bb cc ff gg1 gg2 xx i, ff i ◃◃ xx i).
    - exact (λ a b c f1 f2 g x aa bb cc ff1 ff2 gg xx i, xx i ▹▹ gg i).

  Definition disp_depprod_prebicat_data : disp_prebicat_data B.
  Show proof.
    use tpair.
    - use tpair.
      + exact disp_depprod_cat_data.
      + exact disp_depprod_disp_2cell_struct.
    - exact disp_depprod_disp_prebicat_ops.

  Definition disp_depprod_prebicat_laws_help
             {a b : B}
             {f g : a --> b}
             {x y : f ==> g}
             {aa : ∏ (i : I), D i a} {bb : ∏ (i : I), D i b}
             {ff : ∏ (i : I), aa i -->[ f ] bb i}
             {gg : ∏ (i : I), aa i -->[ g ] bb i}
             (xx : ∏ (i : I), ff i ==>[ y ] gg i)
             (p : x = y)
             (i : I)
    : transportb (λ α : f ==> g, ff i ==>[ α ] gg i) p (xx i)
      =
      transportb (λ α : f ==> g, ∏ (i : I), ff i ==>[ α ] gg i) p xx i.
  Show proof.
    induction p.
    apply idpath.

  Definition disp_depprod_prebicat_laws
    : disp_prebicat_laws disp_depprod_prebicat_data.
  Show proof.
    repeat split
    ; intro ; intros
    ; use funextsec ; intro
    ; refine (_ @ disp_depprod_prebicat_laws_help _ _ _).
    - apply disp_id2_left.
    - apply disp_id2_right.
    - apply disp_vassocr.
    - apply disp_lwhisker_id2.
    - apply disp_id2_rwhisker.
    - apply disp_lwhisker_vcomp.
    - apply disp_rwhisker_vcomp.
    - apply disp_vcomp_lunitor.
    - apply disp_vcomp_runitor.
    - apply disp_lwhisker_lwhisker.
    - apply disp_rwhisker_lwhisker.
    - apply disp_rwhisker_rwhisker.
    - apply disp_vcomp_whisker.
    - apply disp_lunitor_linvunitor.
    - apply disp_linvunitor_lunitor.
    - apply disp_runitor_rinvunitor.
    - apply disp_rinvunitor_runitor.
    - apply disp_lassociator_rassociator.
    - apply disp_rassociator_lassociator.
    - apply disp_runitor_rwhisker.
    - apply disp_lassociator_lassociator.

  Definition disp_depprod_prebicat : disp_prebicat B.
  Show proof.
    use tpair.
    - exact disp_depprod_prebicat_data.
    - exact disp_depprod_prebicat_laws.

  Definition disp_depprod_bicat : disp_bicat B.
  Show proof.
    use tpair.
    - exact disp_depprod_prebicat.
    - intros a b f g x aa bb ff gg.
      use impred_isaset.
      intro i.
      apply (D i).

  Definition disp_2cells_isaprop_depprod
             (HD : ∏ (i : I), disp_2cells_isaprop (D i))
    : disp_2cells_isaprop disp_depprod_bicat.
  Show proof.
    intro; intros.
    use impred.
    intro i.
    apply HD.

  Definition disp_depprod_bicat_disp_is_invertible_2cell_map
             {a b : B}
             {f g : B ⟦ a, b ⟧}
             {x : f ==> g}
             {xinv : is_invertible_2cell x}
             {aa : disp_depprod_bicat a}
             {bb : disp_depprod_bicat b}
             {ff : aa -->[ f] bb}
             {gg : aa -->[ g ] bb}
             (xx : ff ==>[ x ] gg)
             (Hx : ∏ (i : I), is_disp_invertible_2cell xinv (xx i))
    : is_disp_invertible_2cell xinv xx.
  Show proof.
    use tpair.
    - exact (λ i, pr1 (Hx i)).
    - split.
      + use funextsec.
        intro i.
        refine (_ @ disp_depprod_prebicat_laws_help _ _ _).
        exact (disp_vcomp_rinv ((xx i ,, Hx i) : disp_invertible_2cell (x ,, xinv) _ _)).
      + use funextsec.
        intro i.
        refine (_ @ disp_depprod_prebicat_laws_help _ _ _).
        exact (disp_vcomp_linv ((xx i ,, Hx i) : disp_invertible_2cell (x ,, xinv) _ _)).

  Definition disp_locally_groupoid_depprod
             (HD : ∏ (i : I), disp_locally_groupoid (D i))
    : disp_locally_groupoid disp_depprod_bicat.
  Show proof.
    intros a b f g x aa bb ff gg xx.
    apply disp_depprod_bicat_disp_is_invertible_2cell_map.
    intro i.
    apply HD.

  Definition disp_depprod_bicat_disp_invertible_2cell_map
             {a b : B}
             {f : B ⟦ a, b ⟧}
             {aa : disp_depprod_bicat a}
             {bb : disp_depprod_bicat b}
             (ff : aa -->[ f] bb)
             (gg : aa -->[ f] bb)
    : (∏ (i : I), disp_invertible_2cell (id2_invertible_2cell f) (ff i) (gg i))
        →
        disp_invertible_2cell (id2_invertible_2cell f) ff gg.
  Show proof.
    intros x.
    use tpair.
    - exact (λ i, x i).
    - apply disp_depprod_bicat_disp_is_invertible_2cell_map.
      exact (λ i, pr2 (x i)).

  Definition disp_depprod_bicat_disp_is_invertible_2cell_pr
             {a b : B}
             {f g : B ⟦ a, b ⟧}
             {x : f ==> g}
             {xinv : is_invertible_2cell x}
             {aa : disp_depprod_bicat a}
             {bb : disp_depprod_bicat b}
             {ff : aa -->[ f] bb}
             {gg : aa -->[ g ] bb}
             (xx : ff ==>[ x ] gg)
             (Hx : is_disp_invertible_2cell xinv xx)
    : ∏ (i : I), is_disp_invertible_2cell xinv (xx i).
  Show proof.
    intro i.
    use tpair.
    - exact (pr1 Hx i).
    - split.
      + refine (_ @ !(disp_depprod_prebicat_laws_help (disp_id2 ff) _ _)).
        exact (eqtohomot (disp_vcomp_rinv
                            ((xx ,, Hx) : disp_invertible_2cell (x ,, xinv) _ _)) i).
      + refine (_ @ !(disp_depprod_prebicat_laws_help (disp_id2 gg) _ _)).
        exact (eqtohomot (disp_vcomp_linv
                            ((xx ,, Hx) : disp_invertible_2cell (x ,, xinv) _ _)) i).

  Definition disp_depprod_bicat_disp_invertible_2cell_inv_map
             {a b : B}
             {f : B ⟦ a, b ⟧}
             {aa : disp_depprod_bicat a}
             {bb : disp_depprod_bicat b}
             (ff : aa -->[ f] bb)
             (gg : aa -->[ f] bb)
    : disp_invertible_2cell (id2_invertible_2cell f) ff gg
      →
      (∏ (i : I), disp_invertible_2cell (id2_invertible_2cell f) (ff i) (gg i)).
  Show proof.
    intros x i.
    use tpair.
    - exact (pr1 x i).
    - exact (disp_depprod_bicat_disp_is_invertible_2cell_pr _ (pr2 x) i).

  Definition disp_depprod_bicat_disp_invertible_2cell_weq
             {a b : B}
             {f : B ⟦ a, b ⟧}
             {aa : disp_depprod_bicat a}
             {bb : disp_depprod_bicat b}
             (ff : aa -->[ f] bb)
             (gg : aa -->[ f] bb)
    : (∏ (i : I), disp_invertible_2cell (id2_invertible_2cell f) (ff i) (gg i))
        ≃
        disp_invertible_2cell (id2_invertible_2cell f) ff gg.
  Show proof.
    use make_weq.
    - exact (disp_depprod_bicat_disp_invertible_2cell_map ff gg).
    - use isweq_iso.
      + exact (disp_depprod_bicat_disp_invertible_2cell_inv_map ff gg).
      + intros x.
        use funextsec.
        intro i.
        use subtypePath.
        { intro ; apply isaprop_is_disp_invertible_2cell. }
        apply idpath.
      + intros x.
        use subtypePath.
        { intro ; apply isaprop_is_disp_invertible_2cell. }
        apply idpath.

  Section DepProdBicatDispLocallyUnivalent.
    Variable (HD_2_1 : ∏ (i : I), disp_univalent_2_1 (D i)).

    Definition disp_depprod_bicat_idtotiso_2_1
               {a b : B}
               {f : B ⟦ a, b ⟧}
               {aa : disp_depprod_bicat a}
               {bb : disp_depprod_bicat b}
               (ff : aa -->[ f] bb)
               (gg : aa -->[ f] bb)
      : ff = gg ≃ disp_invertible_2cell (id2_invertible_2cell f) ff gg
      := ((disp_depprod_bicat_disp_invertible_2cell_weq ff gg)
            ∘ weqonsecfibers
            _ _ (λ i, make_weq _ (HD_2_1 i _ _ _ _ (idpath _) _ _ (ff i) (gg i)))
            ∘ invweq (weqfunextsec _ _ _))%weq.

    Definition disp_depprod_univalent_2_1
      : disp_univalent_2_1 disp_depprod_bicat.
    Show proof.
      apply fiberwise_local_univalent_is_univalent_2_1.
      intros a b f aa bb ff gg.
      use weqhomot.
      - exact (disp_depprod_bicat_idtotiso_2_1 ff gg).
      - intros p.
        induction p.
        use subtypePath.
        { intro ; apply isaprop_is_disp_invertible_2cell. }
        apply idpath.
  End DepProdBicatDispLocallyUnivalent.

  Definition disp_depprod_bicat_disp_adjequiv_map
             {a : B}
             (aa bb : disp_depprod_bicat a)
    : (∏ (i : I), disp_adjoint_equivalence
                    (internal_adjoint_equivalence_identity a)
                    (aa i) (bb i))
      → disp_adjoint_equivalence (internal_adjoint_equivalence_identity a) aa bb.
  Show proof.
    intros f.
    use tpair.
    - exact (λ i, f i).
    - use tpair.
      + use tpair.
        * exact (λ i, disp_left_adjoint_right_adjoint _ (f i)).
        * split.
          ** exact (λ i, disp_left_adjoint_unit _ (f i)).
          ** exact (λ i, disp_left_adjoint_counit _ (f i)).
      + split.
        * split.
          ** abstract
               (use funextsec ;
                intro i ;
                refine (pr1 (pr122 (f i)) @ _) ;
                refine ((disp_depprod_prebicat_laws_help _ _ _))).
          ** abstract
               (use funextsec ;
                intro i ;
                refine (pr2 (pr122 (f i)) @ _) ;
                refine ((disp_depprod_prebicat_laws_help _ _ _))).
        * split.
          ** apply disp_depprod_bicat_disp_is_invertible_2cell_map.
             exact (λ i, pr1 (pr222 (f i))).
          ** apply disp_depprod_bicat_disp_is_invertible_2cell_map.
             exact (λ i, pr2 (pr222 (f i))).

  Definition disp_depprod_bicat_disp_adjequiv_inv
             {a : B}
             (aa bb : disp_depprod_bicat a)
    : disp_adjoint_equivalence (internal_adjoint_equivalence_identity a) aa bb
      → (∏ (i : I), disp_adjoint_equivalence
                    (internal_adjoint_equivalence_identity a)
                    (aa i) (bb i)).
  Show proof.
    intros f i.
    use tpair.
    - exact (pr1 f i).
    - use tpair.
      + use tpair.
        * exact (disp_left_adjoint_right_adjoint _ f i).
        * split.
          ** exact (disp_left_adjoint_unit _ f i).
          ** exact (disp_left_adjoint_counit _ f i).
      + split.
        * split.
          ** abstract
               (refine (eqtohomot (pr1 (pr122 f)) i @ _) ;
                refine (!(disp_depprod_prebicat_laws_help _ _ _))).
          ** abstract
               (refine (eqtohomot (pr2 (pr122 f)) i @ _) ;
                refine (!(disp_depprod_prebicat_laws_help _ _ _))).
        * split.
          ** exact (disp_depprod_bicat_disp_is_invertible_2cell_pr
                      _ (pr1 (pr222 f)) i).
          ** exact (disp_depprod_bicat_disp_is_invertible_2cell_pr
                      _ (pr2 (pr222 f)) i).

  Variable (HB : is_univalent_2_1 B)
           (HD_2_1 : ∏ (i : I), disp_univalent_2_1 (D i)).

  Definition disp_depprod_bicat_disp_adjequiv_weq
             {a : B}
             (aa bb : disp_depprod_bicat a)
    : (∏ x : I, disp_adjoint_equivalence
                  (internal_adjoint_equivalence_identity a)
                  (aa x) (bb x))
        ≃ disp_adjoint_equivalence (internal_adjoint_equivalence_identity a) aa bb.
  Show proof.
    use make_weq.
    - exact (disp_depprod_bicat_disp_adjequiv_map aa bb).
    - use isweq_iso.
      + exact (disp_depprod_bicat_disp_adjequiv_inv aa bb).
      + intros f.
        use funextsec.
        intros i.
        use subtypePath.
        { intro ; apply isaprop_disp_left_adjoint_equivalence
          ; [ exact HB | exact (HD_2_1 i) ].
        }
        apply idpath.
      + intros f.
        use subtypePath.
        { intro ; apply isaprop_disp_left_adjoint_equivalence
          ; [ exact HB | exact (disp_depprod_univalent_2_1 HD_2_1) ].
        }
        apply idpath.

  Section DepProdBicatDispGloballyUnivalent.
    Variable (HD_2_0 : ∏ (i : I), disp_univalent_2_0 (D i)).

    Definition disp_depprod_bicat_idtotiso_2_0
               {a : B}
               (aa bb : disp_depprod_bicat a)
      : (aa = bb)
          ≃
          disp_adjoint_equivalence (internal_adjoint_equivalence_identity a) aa bb
      := ((disp_depprod_bicat_disp_adjequiv_weq aa bb)
            ∘ weqonsecfibers
              _ _ (λ i, make_weq _ (HD_2_0 i _ _ (idpath a) _ _))
            ∘ invweq (weqfunextsec _ _ _))%weq.

    Definition disp_depprod_univalent_2_0
      : disp_univalent_2_0 disp_depprod_bicat.
    Show proof.
      apply fiberwise_univalent_2_0_to_disp_univalent_2_0.
      intros a aa bb.
      use weqhomot.
      - exact (disp_depprod_bicat_idtotiso_2_0 aa bb).
      - intros p.
        induction p.
        use subtypePath.
        { intro ; apply isaprop_disp_left_adjoint_equivalence
          ; [ exact HB | exact (disp_depprod_univalent_2_1 HD_2_1) ].
        }
        apply idpath.
  End DepProdBicatDispGloballyUnivalent.
End DispDepprod.