Library UniMath.Bicategories.DisplayedBicats.DispBicat

Displayed bicategories

Benedikt Ahrens, Marco Maggesi February 2018
This file develops displayed bicategories analogous to displayed (1-)categories as presented in Benedikt Ahrens and Peter LeFanu Lumsdaine, Displayed categories http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.5
*********************************************************************************

Displayed bicategories.


Transport of displayed cells.

Transport of displayed cells is used pervasively, to make the code more terse and ease certain proofs we define some ad hoc functions and theorems.
TODO: These definitions are not used yet.

Definition of displayed bicategories.


Definition disp_2cell_struct {C : prebicat_1_id_comp_cells} (D : disp_cat_ob_mor C) : UU
  := (c c' : C) (f g : Cc,c') (x : f ==> g)
       (d : D c) (d' : D c') (f' : d -->[f] d') (g' : d -->[g] d'), UU.

Definition disp_prebicat_1_id_comp_cells (C : prebicat_1_id_comp_cells) : UU
  := D : disp_cat_data C, disp_2cell_struct D.

Coercion disp_cat_data_from_disp_prebicat_1_id_comp_cells
         {C : prebicat_1_id_comp_cells} (D : disp_prebicat_1_id_comp_cells C)
  : disp_cat_data C
  := pr1 D.

Definition disp_2cells {C : prebicat_1_id_comp_cells}
           {D : disp_prebicat_1_id_comp_cells C}
           {c c' : C} {f g : Cc,c'} (x : f ==> g)
           {d : D c} {d' : D c'} (f' : d -->[f] d') (g' : d -->[g] d')
  : UU
  := pr2 D c c' f g x d d' f' g'.

Section Cell_Transport.

Context {C : bicat} {D : disp_prebicat_1_id_comp_cells C}.

Notation "f' ==>[ x ] g'" := (disp_2cells x f' g') (at level 60).

Definition cell_transportf
           {a b : C} {f g : Ca,b}
           {α β : f ==> g}
           (e : α = β)
           {aa : D a} {bb : D b}
           {ff : aa -->[f] bb}
           {gg : aa -->[g] bb}
           (αα : ff ==>[α] gg)
  : ff ==>[β] gg
  := transportf (λ x : f ==> g, ff ==>[x] gg) e αα.

Definition cell_transportb
           {a b : C} {f g : Ca,b}
           {α β : f ==> g}
           (e : α = β)
           {aa : D a} {bb : D b}
           {ff : aa -->[f] bb}
           {gg : aa -->[g] bb}
           (ββ : ff ==>[β] gg)
  : ff ==>[α] gg
  := transportb (λ x : f ==> g, ff ==>[x] gg) e ββ.

Lemma cell_transportf_pathsinv0
      {a b : C} {f g : Ca,b}
      {α β : f ==> g}
      (e : α = β)
      {aa : D a} {bb : D b}
      {ff : aa -->[f] bb}
      {gg : aa -->[g] bb}
      {αα : ff ==>[α] gg}
      {ββ : ff ==>[β] gg}
      (ee : cell_transportf (!e) ββ = αα)
  : cell_transportf e αα = ββ.
Show proof.
  unfold cell_transportf.
  apply (transportf_pathsinv0 (λ x : f ==> g, ff ==>[x] gg)).
  exact ee.

Lemma cell_transportb_to_f
      {a b : C} {f g : Ca,b}
      {α β : f ==> g}
      {e : α = β}
      {aa : D a} {bb : D b}
      {ff : aa -->[f] bb}
      {gg : aa -->[g] bb}
      {αα : ff ==>[α] gg}
      {ββ : ff ==>[β] gg}
      (ee : αα = cell_transportb e ββ)
  : cell_transportf e αα = ββ.
Show proof.
  apply cell_transportf_pathsinv0.
  apply pathsinv0.
  exact ee.

Lemma cell_transportf_to_b
      {a b : C} {f g : Ca,b}
      {α β : f ==> g}
      {e : α = β}
      {aa : D a} {bb : D b}
      {ff : aa -->[f] bb}
      {gg : aa -->[g] bb}
      {αα : ff ==>[α] gg}
      {ββ : ff ==>[β] gg}
      (ee : cell_transportf e αα = ββ)
  : αα = cell_transportb e ββ.
Show proof.
  apply pathsinv0.
  apply (transportf_pathsinv0 (λ x : f ==> g, ff ==>[ x] gg)).
  etrans.
  { apply maponpaths_2.
    apply pathsinv0inv0. }
  exact ee.

End Cell_Transport.

Operations on bicategories


Section disp_prebicat.

Context {C : bicat}.

Local Notation "f' ==>[ x ] g'" := (disp_2cells x f' g') (at level 60).
Local Notation "f' <==[ x ] g'" := (disp_2cells x g' f') (at level 60, only parsing).

Definition disp_prebicat_ops (D : disp_prebicat_1_id_comp_cells C) : UU
  := ( (a b : C) (f : Ca,b) (x : D a) (y : D b) (f' : x -->[f] y),
        f' ==>[id2 _] f')
     × ( (a b : C) (f : Ca,b) (x : D a) (y : D b) (f' : x -->[f] y),
        id_disp x ;; f' ==>[lunitor _] f')
     × ( (a b : C) (f : Ca,b) (x : D a) (y : D b) (f' : x -->[f] y),
        f' ;; id_disp y ==>[runitor _] f')
     × ( (a b : C) (f : Ca,b) (x : D a) (y : D b) (f' : x -->[f] y),
        id_disp x ;; f' <==[linvunitor _] f')
     × ( (a b : C) (f : Ca,b) (x : D a) (y : D b) (f' : x -->[f] y),
        f' ;; id_disp y <==[rinvunitor _] f')
     × ( (a b c d : C) (f : Ca,b) (g : Cb,c) (h : Cc,d)
          (w : D a) (x : D b) (y : D c) (z : D d)
          (ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z),
        (ff ;; gg) ;; hh ==>[rassociator _ _ _] ff ;; (gg ;; hh))
     × ( (a b c d : C) (f : Ca,b) (g : Cb,c) (h : Cc,d)
          (w : D a) (x : D b) (y : D c) (z : D d)
          (ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z),
        ff ;; (gg ;; hh) ==>[lassociator _ _ _] (ff ;; gg) ;; hh)
     × ( (a b : C) (f g h : Ca,b) (r : f ==> g) (s : g ==> h)
          (x : D a) (y : D b) (ff : x -->[f] y) (gg : x -->[g] y) (hh : x -->[h] y),
        ff ==>[r] gg gg ==>[s] hh ff ==>[r s] hh)
     × ( (a b c : C) (f : Ca,b) (g1 g2 : Cb,c)
          (r : g1 ==> g2) (x : D a) (y : D b) (z : D c)
          (ff : x -->[f] y) (gg1 : y -->[g1] z) (gg2 : y -->[g2] z),
        gg1 ==>[r] gg2 ff ;; gg1 ==>[f r] ff ;; gg2)
     × ( (a b c : C) (f1 f2 : Ca,b) (g : Cb,c)
          (r : f1 ==> f2) (x : D a) (y : D b) (z : D c)
          (ff1 : x -->[f1] y) (ff2 : x -->[f2] y) (gg : y -->[g] z),
        ff1 ==>[r] ff2 ff1 ;; gg ==>[r g] ff2 ;; gg).

Definition disp_prebicat_data : UU
  := D : disp_prebicat_1_id_comp_cells C, disp_prebicat_ops D.

Coercion disp_prebicat_ob_mor_cells_1_id_comp_from_disp_prebicat_data
         (D : disp_prebicat_data)
  : disp_prebicat_1_id_comp_cells C
  := pr1 D.

Coercion disp_prebicat_ops_from_disp_prebicat_data (D : disp_prebicat_data)
  : disp_prebicat_ops D
  := pr2 D.

Data projections


Section disp_prebicat_ops_projections.

Context {D : disp_prebicat_data}.

Definition disp_id2 {a b : C} {f : Ca,b} {x : D a} {y : D b} (f' : x -->[f] y)
  : f' ==>[id2 _] f'
  := pr1 (pr2 D) a b f x y f'.

Definition disp_lunitor {a b : C} {f : Ca,b} {x : D a} {y : D b} (f' : x -->[f] y)
  : id_disp x ;; f' ==>[lunitor _] f'
  := pr1 (pr2 (pr2 D)) a b f x y f'.

Definition disp_runitor {a b : C} {f : Ca,b} {x : D a} {y : D b} (f' : x -->[f] y)
  : f' ;; id_disp y ==>[runitor _] f'
  := pr1 (pr2 (pr2 (pr2 D))) _ _ f _ _ f'.

Definition disp_linvunitor
           {a b : C} {f : Ca,b} {x : D a} {y : D b} (f' : x -->[f] y)
  : id_disp x ;; f' <==[linvunitor _] f'
  := pr1 (pr2 (pr2 (pr2 (pr2 D)))) _ _ f _ _ f'.

Definition disp_rinvunitor
           {a b : C} {f : Ca,b} {x : D a} {y : D b} (f' : x -->[f] y)
  : f' ;; id_disp y <==[rinvunitor _] f'
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 D))))) _ _ f _ _ f'.

Definition disp_rassociator
           {a b c d : C} {f : Ca,b} {g : Cb,c} {h : Cc,d}
       {w : D a} {x : D b} {y : D c} {z : D d}
       (ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z)
  : (ff ;; gg) ;; hh ==>[rassociator _ _ _] ff ;; (gg ;; hh)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))) _ _ _ _ _ _ _ w _ _ _ ff gg hh.

Definition disp_lassociator
           {a b c d : C} {f : Ca,b} {g : Cb,c} {h : Cc,d}
           {w : D a} {x : D b} {y : D c} {z : D d}
           (ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z)
  : ff ;; (gg ;; hh) ==>[lassociator _ _ _] (ff ;; gg) ;; hh
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))) _ _ _ _ _ _ _ w _ _ _ ff gg hh.

Definition disp_vcomp2
           {a b : C} {f g h : Ca,b}
           {r : f ==> g} {s : g ==> h}
           {x : D a} {y : D b}
           {ff : x -->[f] y} {gg : x -->[g] y} {hh : x -->[h] y}
  : ff ==>[r] gg gg ==>[s] hh ff ==>[r s] hh
  := λ rr ss, pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))
                   _ _ _ _ _ _ _ _ _ _ _ _ rr ss.

Definition disp_lwhisker
           {a b c : C} {f : Ca,b} {g1 g2 : Cb,c}
           {r : g1 ==> g2}
           {x : D a} {y : D b} {z : D c}
           (ff : x -->[f] y) {gg1 : y -->[g1] z} {gg2 : y -->[g2] z}
  : gg1 ==>[r] gg2 ff ;; gg1 ==>[f r] ff ;; gg2
  := λ rr, pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))))))
               _ _ _ _ _ _ _ _ _ _ _ _ _ rr.

Definition disp_rwhisker
           {a b c : C} {f1 f2 : Ca,b} {g : Cb,c}
           {r : f1 ==> f2}
           {x : D a} {y : D b} {z : D c}
           {ff1 : x -->[f1] y} {ff2 : x -->[f2] y} (gg : y -->[g] z)
  : ff1 ==>[r] ff2 ff1 ;; gg ==>[r g] ff2 ;; gg
  := λ rr, pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))))))
               _ _ _ _ _ _ _ _ _ _ _ _ _ rr.

End disp_prebicat_ops_projections.

Local Notation "rr •• ss" := (disp_vcomp2 rr ss) (at level 60).
Local Notation "ff ◃◃ rr" := (disp_lwhisker ff rr) (at level 60).
Local Notation "rr ▹▹ gg" := (disp_rwhisker gg rr) (at level 60).

Section disp_prebicat_laws.

Context (D : disp_prebicat_data).

Definition disp_id2_left_law : UU
  := (a b : C) (f g : Ca,b) (η : f ==> g)
       (x : D a) (y : D b) (ff : x -->[f] y) (gg : x -->[g] y)
       (ηη : ff ==>[η] gg),
     disp_id2 _ •• ηη = transportb (λ α, _ ==>[α] _) (id2_left _) ηη.

Definition disp_id2_right_law : UU
  := (a b : C) (f g : Ca,b) (η : f ==> g)
       (x : D a) (y : D b) (ff : x -->[f] y) (gg : x -->[g] y)
       (ηη : ff ==>[η] gg),
     ηη •• disp_id2 _ = transportb (λ α, _ ==>[α] _) (id2_right _) ηη.

Definition disp_vassocr_law : UU
  := (a b : C) (f g h k : Ca,b) (η : f ==> g) (φ : g ==> h) (ψ : h ==> k)
       (x : D a) (y : D b)
       (ff : x -->[f] y) (gg : x -->[g] y) (hh : x -->[h] y) (kk : x -->[k] y)
       (ηη : ff ==>[η] gg) (φφ : gg ==>[φ] hh) (ψψ : hh ==>[ψ] kk),
     ηη •• (φφ •• ψψ) =
     transportb (λ α, _ ==>[α] _) (vassocr _ _ _) ((ηη •• φφ) •• ψψ).

Definition disp_lwhisker_id2_law : UU
  := (a b c : C) (f : Ca,b) (g : Cb,c)
       (x : D a) (y : D b) (z : D c) (ff : x -->[f] y) (gg : y -->[g] z),
     ff ◃◃ disp_id2 gg =
     transportb (λ α, _ ==>[α] _) (lwhisker_id2 _ _) (disp_id2 (ff ;; gg)).

Definition disp_id2_rwhisker_law : UU
  := (a b c : C) (f : Ca,b) (g : Cb,c)
       (x : D a) (y : D b) (z : D c) (ff : x -->[f] y) (gg : y -->[g] z),
     disp_id2 ff ▹▹ gg =
     transportb (λ α, _ ==>[α] _) (id2_rwhisker _ _) (disp_id2 (ff ;; gg)).

Definition disp_lwhisker_vcomp_law : UU
  := (a b c : C) (f : Ca,b) (g h i : Cb,c)
      (η : g ==> h) (φ : h ==> i)
      (x : D a) (y : D b) (z : D c) (ff : x -->[f] y)
      (gg : y -->[g] z) (hh : y -->[h] z) (ii : y -->[i] z)
      (ηη : gg ==>[η] hh) (φφ : hh ==>[φ] ii),
     (ff ◃◃ ηη) •• (ff ◃◃ φφ) =
     transportb (λ α, _ ==>[α] _) (lwhisker_vcomp _ _ _) (ff ◃◃ (ηη •• φφ)).

Definition disp_rwhisker_vcomp_law : UU
  := (a b c : C) (f g h : Ca,b) (i : Cb,c) (η : f ==> g) (φ : g ==> h)
       (x : D a) (y : D b) (z : D c)
       (ff : x -->[f] y) (gg : x -->[g] y) (hh : x -->[h] y)
       (ii : y -->[i] z)
       (ηη : ff ==>[η] gg) (φφ : gg ==>[φ] hh),
     (ηη ▹▹ ii) •• (φφ ▹▹ ii) =
     transportb (λ α, _ ==>[α] _) (rwhisker_vcomp _ _ _) ((ηη •• φφ) ▹▹ ii).

Definition disp_vcomp_lunitor_law : UU
  := (a b : C) (f g : Ca,b) (η : f ==> g)
       (x : D a) (y : D b) (ff : x -->[f] y) (gg : x -->[g] y)
       (ηη : ff ==>[η] gg),
     (id_disp _ ◃◃ ηη) •• disp_lunitor gg =
     transportb (λ α, _ ==>[α] _) (vcomp_lunitor _ _ _) (disp_lunitor ff •• ηη).

Definition disp_vcomp_runitor_law : UU
  := (a b : C) (f g : Ca,b) (η : f ==> g)
       (x : D a) (y : D b) (ff : x -->[f] y) (gg : x -->[g] y)
       (ηη : ff ==>[η] gg),
     (ηη ▹▹ id_disp _) •• disp_runitor gg =
     transportb (λ α, _ ==>[α] _) (vcomp_runitor _ _ _) (disp_runitor ff •• ηη).

Definition disp_lwhisker_lwhisker_law : UU
  := (a b c d : C) (f : Ca,b) (g : Cb,c) (h i : c --> d) (η : h ==> i)
       (w : D a) (x : D b) (y : D c) (z : D d)
       (ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z) (ii : y -->[i] z)
       (ηη : hh ==>[η] ii),
     ff ◃◃ (gg ◃◃ ηη) •• disp_lassociator _ _ _ =
     transportb (λ α, _ ==>[α] _) (lwhisker_lwhisker _ _ _)
                (disp_lassociator _ _ _ •• (ff ;; gg ◃◃ ηη)).

Definition disp_rwhisker_lwhisker_law : UU
  := (a b c d : C) (f : Ca,b) (g h : Cb,c) (i : c --> d) (η : g ==> h)
       (w : D a) (x : D b) (y : D c) (z : D d)
       (ff : w -->[f] x) (gg : x -->[g] y) (hh : x -->[h] y) (ii : y -->[i] z)
       (ηη : gg ==>[η] hh),
     (ff ◃◃ (ηη ▹▹ ii)) •• disp_lassociator _ _ _ =
     transportb (λ α, _ ==>[α] _) (rwhisker_lwhisker _ _ _)
                (disp_lassociator _ _ _ •• ((ff ◃◃ ηη) ▹▹ ii)).

Definition disp_rwhisker_rwhisker_law : UU
  := (a b c d : C) (f g : Ca,b) (h : Cb,c) (i : c --> d) (η : f ==> g)
       (w : D a) (x : D b) (y : D c) (z : D d)
       (ff : w -->[f] x) (gg : w -->[g] x) (hh : x -->[h] y) (ii : y -->[i] z)
       (ηη : ff ==>[η] gg),
     disp_lassociator _ _ _ •• ((ηη ▹▹ hh) ▹▹ ii) =
     transportb (λ α, _ ==>[α] _) (rwhisker_rwhisker _ _ _)
                ((ηη ▹▹ hh ;; ii) •• disp_lassociator _ _ _).

Definition disp_vcomp_whisker_law : UU
  := (a b c : C) (f g : Ca,b) (h i : Cb,c)
       (η : f ==> g) (φ : h ==> i)
       (x : D a) (y : D b) (z : D c)
       (ff : x -->[f] y) (gg : x -->[g] y)
       (hh : y -->[h] z) (ii : y -->[i] z)
       (ηη : ff ==>[η] gg) (φφ : hh ==>[φ] ii),
     (ηη ▹▹ hh) •• (gg ◃◃ φφ) =
     transportb (λ α, _ ==>[α] _) (vcomp_whisker _ _) ((ff ◃◃ φφ) •• (ηη ▹▹ ii)).

Definition disp_lunitor_linvunitor_law : UU
  := (a b : C) (f : Ca,b)
       (x : D a) (y : D b) (ff : x -->[f] y),
     disp_lunitor ff •• disp_linvunitor _ =
     transportb (λ α, _ ==>[α] _) (lunitor_linvunitor _) (disp_id2 (id_disp _ ;; ff)).

Definition disp_linvunitor_lunitor_law : UU
  := (a b : C) (f : Ca,b)
       (x : D a) (y : D b) (ff : x -->[f] y),
     disp_linvunitor ff •• disp_lunitor _ =
     transportb (λ α, _ ==>[α] _) (linvunitor_lunitor _) (disp_id2 _).

Definition disp_runitor_rinvunitor_law : UU
  := (a b : C) (f : Ca,b)
       (x : D a) (y : D b) (ff : x -->[f] y),
     disp_runitor ff •• disp_rinvunitor _ =
     transportb (λ α, _ ==>[α] _) (runitor_rinvunitor _) (disp_id2 _).

Definition disp_rinvunitor_runitor_law : UU
  := (a b : C) (f : Ca,b)
       (x : D a) (y : D b) (ff : x -->[f] y),
     disp_rinvunitor ff •• disp_runitor _ =
     transportb (λ α, _ ==>[α] _) (rinvunitor_runitor _) (disp_id2 _).

Definition disp_lassociator_rassociator_law : UU
  := (a b c d : C) (f : Ca,b) (g : Cb,c) (h : c --> d)
       (w : D a) (x : D b) (y : D c) (z : D d)
       (ff : w -->[f] x) (gg : x -->[g] y)
       (hh : y -->[h] z),
     disp_lassociator ff gg hh •• disp_rassociator _ _ _ =
     transportb (λ α, _ ==>[α] _) (lassociator_rassociator _ _ _ ) (disp_id2 _).

Definition disp_rassociator_lassociator_law : UU
  := (a b c d : C) (f : Ca,b) (g : Cb,c) (h : c --> d)
       (w : D a) (x : D b) (y : D c) (z : D d)
       (ff : w -->[f] x) (gg : x -->[g] y)
       (hh : y -->[h] z),
     disp_rassociator ff gg hh •• disp_lassociator _ _ _ =
     transportb (λ α, _ ==>[α] _) (rassociator_lassociator _ _ _ ) (disp_id2 _).

Definition disp_runitor_rwhisker_law : UU
  := (a b c : C) (f : Ca,b) (g : Cb,c)
       (x : D a) (y : D b) (z : D c)
       (ff : x -->[f] y) (gg : y -->[g] z),
     disp_lassociator _ _ _ •• (disp_runitor ff ▹▹ gg) =
     transportb (λ α, _ ==>[α] _) (runitor_rwhisker _ _) (ff ◃◃ disp_lunitor gg).

Definition disp_lassociator_lassociator_law : UU
  := (a b c d e: C) (f : Ca,b) (g : Cb,c) (h : c --> d) (i : Cd,e)
       (v : D a) (w : D b) (x : D c) (y : D d) (z : D e)
       (ff : v -->[f] w) (gg : w -->[g] x)
       (hh : x -->[h] y) (ii : y -->[i] z),

     (ff ◃◃ disp_lassociator gg hh ii) •• disp_lassociator _ _ _ ••
     (disp_lassociator _ _ _ ▹▹ ii) =
     transportb (λ α, _ ==>[α] _) (lassociator_lassociator _ _ _ _)
                (disp_lassociator ff gg _ •• disp_lassociator _ _ _).

Laws

Laws projections

Definition disp_prebicat : UU
  := D : disp_prebicat_data, disp_prebicat_laws D.

Coercion disp_prebicat_data_from_disp_prebicat (D : disp_prebicat)
  : disp_prebicat_data
  := pr1 D.

Section disp_prebicat_law_projections.

Context {D : disp_prebicat}.

Definition disp_id2_left {a b : C} {f g : Ca,b} {η : f ==> g}
           {x : D a} {y : D b} {ff : x -->[f] y} {gg : x -->[g] y}
           (ηη : ff ==>[η] gg)
  : disp_id2 _ •• ηη = transportb (λ α, _ ==>[α] _) (id2_left _) ηη
  := pr1 (pr2 D) _ _ _ _ _ x y ff gg ηη.

Definition disp_id2_right {a b : C} {f g : Ca,b} {η : f ==> g}
           {x : D a} {y : D b} {ff : x -->[f] y} {gg : x -->[g] y}
           (ηη : ff ==>[η] gg)
  : ηη •• disp_id2 _ = transportb (λ α, _ ==>[α] _) (id2_right _) ηη
  := pr1 (pr2 (pr2 D)) _ _ _ _ _ _ _ _ _ ηη.

Definition disp_vassocr {a b : C} {f g h k : Ca,b}
           {η : f ==> g} {φ : g ==> h} {ψ : h ==> k}
           {x : D a} {y : D b}
           {ff : x -->[f] y} {gg : x -->[g] y} {hh : x -->[h] y} {kk : x -->[k] y}
           (ηη : ff ==>[η] gg) (φφ : gg ==>[φ] hh) (ψψ : hh ==>[ψ] kk)
  : ηη •• (φφ •• ψψ) =
    transportb (λ α, _ ==>[α] _) (vassocr _ _ _) ((ηη •• φφ) •• ψψ)
  := pr1 (pr2 (pr2 (pr2 D))) _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ηη φφ ψψ .

Definition disp_vassocr' {a b : C} {f g h k : Ca,b}
           {η : f ==> g} {φ : g ==> h} {ψ : h ==> k}
           {x : D a} {y : D b}
           {ff : x -->[f] y} {gg : x -->[g] y} {hh : x -->[h] y} {kk : x -->[k] y}
           (ηη : ff ==>[η] gg) (φφ : gg ==>[φ] hh) (ψψ : hh ==>[ψ] kk)
  : transportf (λ α, _ ==>[α] _) (vassocr _ _ _) (ηη •• (φφ •• ψψ)) =
    ((ηη •• φφ) •• ψψ).
Show proof.
  use (transportf_transpose_left (P := λ x' : f ==> k, ff ==>[x'] kk)).
  apply disp_vassocr.

Definition disp_lwhisker_id2 {a b c : C} {f : Ca,b} {g : Cb,c}
           {x : D a} {y : D b} {z : D c} (ff : x -->[f] y) (gg : y -->[g] z)
  : ff ◃◃ disp_id2 gg =
    transportb (λ α, _ ==>[α] _) (lwhisker_id2 _ _) (disp_id2 (ff ;; gg))
  := pr1 (pr2 (pr2 (pr2 (pr2 D)))) _ _ _ _ _ _ _ _ ff gg.

Definition disp_id2_rwhisker {a b c : C} {f : Ca,b} {g : Cb,c}
           {x : D a} {y : D b} {z : D c}
           (ff : x -->[f] y) (gg : y -->[g] z)
  : disp_id2 ff ▹▹ gg =
    transportb (λ α, _ ==>[α] _) (id2_rwhisker _ _) (disp_id2 (ff ;; gg))
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 D))))) _ _ _ _ _ _ _ _ ff gg.

Definition disp_lwhisker_vcomp {a b c : C} {f : Ca,b} {g h i : Cb,c}
           {η : g ==> h} {φ : h ==> i}
           {x : D a} {y : D b} {z : D c} {ff : x -->[f] y}
           {gg : y -->[g] z} {hh : y -->[h] z} {ii : y -->[i] z}
           (ηη : gg ==>[η] hh) (φφ : hh ==>[φ] ii)
  : (ff ◃◃ ηη) •• (ff ◃◃ φφ) =
    transportb (λ α, _ ==>[α] _) (lwhisker_vcomp _ _ _) (ff ◃◃ (ηη •• φφ))
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))) _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ηη φφ.

Definition disp_rwhisker_vcomp {a b c : C} {f g h : Ca,b} {i : Cb,c}
           {η : f ==> g} {φ : g ==> h}
           {x : D a} {y : D b} {z : D c}
           {ff : x -->[f] y} {gg : x -->[g] y} {hh : x -->[h] y} {ii : y -->[i] z}
           (ηη : ff ==>[η] gg) (φφ : gg ==>[φ] hh)
  : (ηη ▹▹ ii) •• (φφ ▹▹ ii) =
    transportb (λ α, _ ==>[α] _) (rwhisker_vcomp _ _ _) ((ηη •• φφ) ▹▹ ii)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))))
         _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ηη φφ.

Definition disp_vcomp_lunitor {a b : C} {f g : Ca,b} {η : f ==> g}
           {x : D a} {y : D b} {ff : x -->[f] y} {gg : x -->[g] y}
           (ηη : ff ==>[η] gg)
  : (id_disp _ ◃◃ ηη) •• disp_lunitor gg =
    transportb (λ α, _ ==>[α] _) (vcomp_lunitor _ _ _) (disp_lunitor ff •• ηη)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))))) _ _ _ _ _ _ _ _ _ ηη.

Definition disp_vcomp_runitor {a b : C} {f g : Ca,b} {η : f ==> g}
           {x : D a} {y : D b} {ff : x -->[f] y} {gg : x -->[g] y}
           (ηη : ff ==>[η] gg)
  : (ηη ▹▹ id_disp _) •• disp_runitor gg =
    transportb (λ α, _ ==>[α] _) (vcomp_runitor _ _ _) (disp_runitor ff •• ηη)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))) _ _ _ _ _ _ _ _ _ ηη.

Definition disp_lwhisker_lwhisker {a b c d : C} {f : Ca,b} {g : Cb,c}
           {h i : c --> d} {η : h ==> i}
           {w : D a} {x : D b} {y : D c} {z : D d}
           (ff : w -->[f] x) (gg : x -->[g] y) {hh : y -->[h] z} {ii : y -->[i] z}
           (ηη : hh ==>[η] ii)
  : ff ◃◃ (gg ◃◃ ηη) •• disp_lassociator _ _ _ =
    transportb (λ α, _ ==>[α] _) (lwhisker_lwhisker _ _ _)
               (disp_lassociator _ _ _ •• (ff ;; gg ◃◃ ηη))
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))))
         _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ηη.

Definition disp_rwhisker_lwhisker {a b c d : C} {f : Ca,b} {g h : Cb,c}
           {i : c --> d} {η : g ==> h}
           {w : D a} {x : D b} {y : D c} {z : D d}
           (ff : w -->[f] x) {gg : x -->[g] y} {hh : x -->[h] y} (ii : y -->[i] z)
           (ηη : gg ==>[η] hh)
  : (ff ◃◃ (ηη ▹▹ ii)) •• disp_lassociator _ _ _ =
    transportb (λ α, _ ==>[α] _) (rwhisker_lwhisker _ _ _)
               (disp_lassociator _ _ _ •• ((ff ◃◃ ηη) ▹▹ ii))
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))))))))
         _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ηη.

Definition disp_rwhisker_rwhisker {a b c d : C} {f g : Ca,b} {h : Cb,c}
           (i : c --> d) (η : f ==> g)
           {w : D a} {x : D b} {y : D c} {z : D d}
           {ff : w -->[f] x} {gg : w -->[g] x} (hh : x -->[h] y) (ii : y -->[i] z)
           (ηη : ff ==>[η] gg)
  : disp_lassociator _ _ _ •• ((ηη ▹▹ hh) ▹▹ ii) =
    transportb (λ α, _ ==>[α] _) (rwhisker_rwhisker _ _ _)
               ((ηη ▹▹ hh ;; ii) •• disp_lassociator _ _ _)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))))))
         _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ηη.

Definition disp_vcomp_whisker {a b c : C} {f g : Ca,b} {h i : Cb,c}
           (η : f ==> g) (φ : h ==> i)
           (x : D a) (y : D b) (z : D c)
           (ff : x -->[f] y) (gg : x -->[g] y) (hh : y -->[h] z) (ii : y -->[i] z)
           (ηη : ff ==>[η] gg) (φφ : hh ==>[φ] ii)
  : (ηη ▹▹ hh) •• (gg ◃◃ φφ) =
    transportb (λ α, _ ==>[α] _) (vcomp_whisker _ _) ((ff ◃◃ φφ) •• (ηη ▹▹ ii))
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))))))))))
         _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ηη φφ.

Definition disp_lunitor_linvunitor {a b : C} {f : Ca,b}
           {x : D a} {y : D b} (ff : x -->[f] y)
  : disp_lunitor ff •• disp_linvunitor _ =
    transportb (λ α, _ ==>[α] _) (lunitor_linvunitor _) (disp_id2 (id_disp _ ;; ff))
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2
            (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))))))))
         _ _ _ _ _ ff.

Definition disp_linvunitor_lunitor {a b : C} {f : Ca,b}
           {x : D a} {y : D b} (ff : x -->[f] y)
  : disp_linvunitor ff •• disp_lunitor _ =
    transportb (λ α, _ ==>[α] _) (linvunitor_lunitor _) (disp_id2 _)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2
            (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))))))))) _ _ _ _ _ ff.

Definition disp_runitor_rinvunitor {a b : C} {f : Ca,b}
           {x : D a} {y : D b} (ff : x -->[f] y)
  : disp_runitor ff •• disp_rinvunitor _ =
    transportb (λ α, _ ==>[α] _) (runitor_rinvunitor _) (disp_id2 _)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2
            (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))))))))))))) _ _ _ _ _ ff.

Definition disp_rinvunitor_runitor {a b : C} {f : Ca,b}
           {x : D a} {y : D b} (ff : x -->[f] y)
  : disp_rinvunitor ff •• disp_runitor _ =
    transportb (λ α, _ ==>[α] _) (rinvunitor_runitor _) (disp_id2 _)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2
            (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))))))))))) _ _ _ _ _ ff.

Definition disp_lassociator_rassociator {a b c d : C} {f : Ca,b} {g : Cb,c}
           {h : c --> d} {w : D a} {x : D b} {y : D c} {z : D d}
           (ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z)
  : disp_lassociator ff gg hh •• disp_rassociator _ _ _ =
    transportb (λ α, _ ==>[α] _) (lassociator_rassociator _ _ _ ) (disp_id2 _)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2
            (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))))))))))))
         _ _ _ _ _ _ _ _ _ _ _ ff gg hh.

Definition disp_rassociator_lassociator
           {a b c d : C} (f : Ca,b) {g : Cb,c} {h : c --> d}
           {w : D a} {x : D b} {y : D c} {z : D d}
           (ff : w -->[f] x) (gg : x -->[g] y)
           (hh : y -->[h] z)
  : disp_rassociator ff gg hh •• disp_lassociator _ _ _ =
    transportb (λ α, _ ==>[α] _) (rassociator_lassociator _ _ _ ) (disp_id2 _)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2
            (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))))))))))))))))
         _ _ _ _ _ _ _ _ _ _ _ ff gg hh.

Definition disp_runitor_rwhisker {a b c : C} {f : Ca,b} {g : Cb,c}
           {x : D a} {y : D b} {z : D c} (ff : x -->[f] y) (gg : y -->[g] z)
  : disp_lassociator _ _ _ •• (disp_runitor ff ▹▹ gg) =
    transportb (λ α, _ ==>[α] _) (runitor_rwhisker _ _) (ff ◃◃ disp_lunitor gg)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2
            (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))))))))))))))
         _ _ _ _ _ _ _ _ ff gg.

Definition disp_lassociator_lassociator {a b c d e: C} {f : Ca,b} {g : Cb,c}
           {h : c --> d} {i : Cd,e}
           {v : D a} {w : D b} {x : D c} {y : D d} {z : D e}
           (ff : v -->[f] w) (gg : w -->[g] x) (hh : x -->[h] y) (ii : y -->[i] z)
  : (ff ◃◃ disp_lassociator gg hh ii) •• disp_lassociator _ _ _ ••
    (disp_lassociator _ _ _ ▹▹ ii) =
    transportb (λ α, _ ==>[α] _) (lassociator_lassociator _ _ _ _)
               (disp_lassociator ff gg _ •• disp_lassociator _ _ _)
  := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2
            (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))))))))))))))))))
         _ _ _ _ _ _ _ _ _ _ _ _ _ _ ff gg hh ii.

End disp_prebicat_law_projections.

Definition disp_hcomp
           {D : disp_prebicat}
           {b₁ b₂ b₃ : C}
           {f₁ f₂ : b₁ --> b₂}
           {g₁ g₂ : b₂ --> b₃}
           {α : f₁ ==> f₂}
           {β : g₁ ==> g₂}
           {bb₁ : D b₁}
           {bb₂ : D b₂}
           {bb₃ : D b₃}
           {ff₁ : bb₁ -->[ f₁ ] bb₂}
           {ff₂ : bb₁ -->[ f₂ ] bb₂}
           {gg₁ : bb₂ -->[ g₁ ] bb₃}
           {gg₂ : bb₂ -->[ g₂ ] bb₃}
           (αα : ff₁ ==>[ α ] ff₂)
           (ββ : gg₁ ==>[ β ] gg₂)
  : ff₁ ;; gg₁ ==>[ β ⋆⋆ α ] ff₂ ;; gg₂
  := (αα ▹▹ gg₁) •• (ff₂ ◃◃ ββ).

Invertible displayed 2-cells.


Lemma disp_vassocl {D : disp_prebicat} {a b : C} {f g h k : Ca,b}
      {η : f ==> g} {φ : g ==> h} {ψ : h ==> k} {x : D a} {y : D b}
      {ff : x -->[f] y} {gg : x -->[g] y} {hh : x -->[h] y} {kk : x -->[k] y}
      (ηη : ff ==>[η] gg) (φφ : gg ==>[φ] hh) (ψψ : hh ==>[ψ] kk)
  : (ηη •• φφ) •• ψψ
    = transportb (λ α, _ ==>[α] _) (vassocl _ _ _) (ηη •• (φφ •• ψψ)).
Show proof.
  apply (transportf_transpose_right (P := λ x', _ ==>[x'] _)).
  apply pathsinv0.
  etrans.
  { apply disp_vassocr. }
  apply maponpaths_2.
  unfold vassocl.
  apply pathsinv0, pathsinv0inv0.

Section Display_Invertible_2cell.
  Context {D : disp_prebicat}.

  Section Def_inv_2cell.

  Context {c c' : C} {f f' : Cc,c'} {d : D c} {d' : D c'}.

  Definition is_disp_invertible_2cell' {α : invertible_2cell f f'}
             {ff : d -->[f] d'} {ff' : d -->[f'] d'} (x : ff ==>[α] ff')
    : UU
    := (y : ff' ==>[α^-1] ff),
         (x •• y =
          transportb (λ α, _ ==>[α] _) (vcomp_rinv α)
                     (disp_id2 ff))
       × (y •• x =
          transportb (λ α, _ ==>[α] _) (vcomp_linv α)
                     (disp_id2 ff')).

  Definition is_disp_invertible_2cell {α : f ==> f'} (inv_α : is_invertible_2cell α)
             {ff : d -->[f] d'} {ff' : d -->[f'] d'} (x : ff ==>[α] ff')
    : UU
    := (y : ff' ==>[inv_α^-1] ff),
         (x •• y =
          transportb (λ α, _ ==>[α] _) (vcomp_rinv inv_α)
                     (disp_id2 ff))
       × (y •• x =
          transportb (λ α, _ ==>[α] _) (vcomp_linv inv_α)
                     (disp_id2 ff')).

  Definition disp_invertible_2cell (α : invertible_2cell f f')
             (ff : d -->[f] d') (ff' : d -->[f'] d')
    : UU
    := (x : ff ==>[α] ff'), is_disp_invertible_2cell α x.

  Coercion disp_cell_from_invertible_2cell {α : invertible_2cell f f'}
           {ff : d -->[f] d'} {ff' : d -->[f'] d'}
           (e : disp_invertible_2cell α ff ff')
    : ff ==>[α] ff'
    := pr1 e.

  Definition disp_inv_cell {α : invertible_2cell f f'}
             {ff : d -->[f] d'} {ff' : d -->[f'] d'}
             (e : disp_invertible_2cell α ff ff')
    : ff' ==>[α^-1] ff
    := pr1 (pr2 e).

  Definition disp_vcomp_rinv {α : invertible_2cell f f'}
             {ff : d -->[f] d'} {ff' : d -->[f'] d'}
             (e : disp_invertible_2cell α ff ff')
    : e •• disp_inv_cell e =
      transportb (λ α, _ ==>[α] _) (vcomp_rinv α) (disp_id2 ff)
    := pr1 (pr2 (pr2 e)).

  Definition disp_vcomp_linv {α : invertible_2cell f f'}
             {ff : d -->[f] d'} {ff' : d -->[f'] d'}
             (e : disp_invertible_2cell α ff ff')
    : disp_inv_cell e •• e =
      transportb (λ α, _ ==>[α] _) (vcomp_linv α) (disp_id2 ff')
    := pr2 (pr2 (pr2 e)).

  End Def_inv_2cell.

  Lemma disp_mor_transportf_postwhisker (a b : C) {x y z : Ca,b} {f f' : x ==> y}
        (ef : f = f') {g : y ==> z} {aa : D a} {bb : D b}
        {xx : aa -->[x] bb} {yy} {zz} (ff : xx ==>[f] yy) (gg : yy ==>[g] zz)
    : (transportf (λ x, _ ==>[x] _) ef ff) •• gg
      = transportf (λ x, _ ==>[x] _) (maponpaths (λ h, h g) ef) (ff •• gg).
  Show proof.
    induction ef; apply idpath.

  Lemma disp_mor_transportf_prewhisker (a b : C) {x y z : Ca,b}
        {f : x ==> y} {g g' : y ==> z} (ef : g = g')
        {aa : D a} {bb : D b}
        {xx : aa -->[x] bb} {yy} {zz} (ff : xx ==>[f] yy) (gg : yy ==>[g] zz)
    : ff •• (transportf (λ x, _ ==>[x] _) ef gg)
      = transportf (λ x, _ ==>[x] _) (maponpaths (λ h, f h) ef) (ff •• gg).
  Show proof.
    induction ef; apply idpath.

  Lemma disp_mor_transportf_prewhisker_gen (a b : C) {x y z : Ca,b} {f : x ==> y}
        {A : UU} {t : A y ==> z} {g g' : A} (ef : g = g')
        {aa : D a} {bb : D b}
        {xx : aa -->[x] bb} {yy} {zz} (ff : xx ==>[f] yy) (gg : yy ==>[t g] zz)
    : ff •• (transportf (λ x, _ ==>[t x] _) ef gg)
      = transportf (λ x, _ ==>[x] _) (maponpaths (λ h, f t h) ef) (ff •• gg).
  Show proof.
    induction ef; apply idpath.

  Lemma disp_lhs_right_invert_cell' {a b : C} {f g h : a --> b}
        {x : f ==> g} {y : invertible_2cell g h} {z : f ==> h}
        {p : x = z y^-1}
        {aa : D a} {bb : D b}
        {ff : aa -->[f] bb}
        {gg : aa -->[g] bb}
        {hh : aa -->[h] bb}
        (xx : ff ==>[x] gg)
        (yy : gg ==>[y] hh)
        (zz : ff ==>[z] hh)
        (H : is_disp_invertible_2cell y yy)
        (q := lhs_right_invert_cell _ _ _ _ p)
        (pp : xx = transportb (λ x, _ ==>[x] _) p (zz •• disp_inv_cell (yy,,H)))
    : xx •• yy = transportb (λ x, _ ==>[x] _) q zz.
  Show proof.
    set (yy' := (yy,,H) : disp_invertible_2cell _ _ _).
    etrans. { apply maponpaths_2. apply pp. }
    etrans. { apply disp_mor_transportf_postwhisker. }
    etrans. { apply maponpaths. apply disp_vassocl. }
    etrans. { unfold transportb. apply (transport_f_f (λ x' : f ==> h, ff ==>[x'] hh)). }
    etrans. { apply maponpaths. apply maponpaths.
              apply disp_vcomp_linv. }
    etrans. { apply maponpaths.
              apply disp_mor_transportf_prewhisker. }
    etrans. { unfold transportb. apply (transport_f_f (λ x' : f ==> h, ff ==>[x'] hh)). }
    etrans. { apply maponpaths.
              apply disp_id2_right. }
    etrans. { unfold transportb. apply (transport_f_f (λ x' : f ==> h, ff ==>[x'] hh)). }
    unfold transportb.
    apply maponpaths_2.
    apply cellset_property.

  Lemma disp_lhs_right_invert_cell {a b : C} {f g h : a --> b}
        {x : f ==> g} {y : g ==> h} {z : f ==> h}
        (inv_y : is_invertible_2cell y)
        {aa : D a} {bb : D b}
        {ff : aa -->[f] bb}
        {gg : aa -->[g] bb}
        {hh : aa -->[h] bb}
        (xx : ff ==>[x] gg)
        (yy : gg ==>[y] hh)
        (zz : ff ==>[z] hh)
        (H : is_disp_invertible_2cell inv_y yy)
        (q : x y = z)
        (p := rhs_right_inv_cell _ _ _ inv_y q : x = z inv_y^-1)
        (pp : xx =
              transportb
                (λ x, _ ==>[x] _) p
                (zz •• disp_inv_cell ((yy,,H):disp_invertible_2cell (y,,inv_y) gg hh)))
    : xx •• yy = transportb (λ x, _ ==>[x] _) q zz.
  Show proof.
    etrans.
    { use (disp_lhs_right_invert_cell' _ _ _ _ pp). }
    apply maponpaths_2.
    apply cellset_property.

  Lemma disp_lhs_left_invert_cell {a b : C} {f g h : a --> b}
        {x : f ==> g} {y : g ==> h} {z : f ==> h} {inv_x : is_invertible_2cell x}
        {aa : D a} {bb : D b}
        {ff : aa -->[f] bb}
        {gg : aa -->[g] bb}
        {hh : aa -->[h] bb}
        (xx : ff ==>[x] gg)
        (yy : gg ==>[y] hh)
        (zz : ff ==>[z] hh)
        (inv_xx : is_disp_invertible_2cell inv_x xx)
        (q : x y = z)
        (p := rhs_left_inv_cell _ _ _ inv_x q : y = inv_x^-1 z)
        (pp : yy =
              transportb
                (λ x, _ ==>[x] _) p
                (disp_inv_cell ((xx,,inv_xx):disp_invertible_2cell (x,,inv_x) ff gg) •• zz))
    : xx •• yy = transportb (λ x, _ ==>[x] _) q zz.
  Show proof.
    etrans. { apply maponpaths. apply pp. }
    etrans.
    { apply disp_mor_transportf_prewhisker. }
    etrans. { apply maponpaths.
              apply disp_vassocr. }
    etrans. { apply (transport_f_f (λ x, _ ==>[x] _)). }
    etrans. { apply maponpaths.
              apply maponpaths_2.
              apply (disp_vcomp_rinv
                       ((xx,,inv_xx):disp_invertible_2cell (x,,inv_x) _ _)). }
    etrans. { apply maponpaths. apply disp_mor_transportf_postwhisker. }
    etrans. { unfold transportb. apply (transport_f_f (λ x, _ ==>[x] _)). }
    etrans. { apply maponpaths. apply disp_id2_left. }
    etrans. { unfold transportb. apply (transport_f_f (λ x, _ ==>[x] _)). }
    unfold transportb.
    apply maponpaths_2. apply cellset_property.

End Display_Invertible_2cell.

Derived laws


Section Derived_Laws.

Context {D : disp_prebicat}.

Definition is_disp_invertible_2cell_lassociator {a b c d : C}
           {f1 : Ca,b} {f2 : Cb,c} {f3 : Cc,d}
           {aa : D a} {bb : D b} {cc : D c} {dd : D d}
           (ff1 : aa -->[f1] bb)
           (ff2 : bb -->[f2] cc)
           (ff3 : cc -->[f3] dd)
  : is_disp_invertible_2cell (is_invertible_2cell_lassociator _ _ _)
                             (disp_lassociator ff1 ff2 ff3).
Show proof.
  exists (disp_rassociator ff1 ff2 ff3).
  split.
  - apply disp_lassociator_rassociator.
  - apply disp_rassociator_lassociator.

Definition is_disp_invertible_2cell_rassociator {a b c d : C}
           {f1 : Ca,b} {f2 : Cb,c} {f3 : Cc,d}
           {aa : D a} {bb : D b} {cc : D c} {dd : D d}
           (ff1 : aa -->[f1] bb)
           (ff2 : bb -->[f2] cc)
           (ff3 : cc -->[f3] dd)
  : is_disp_invertible_2cell (is_invertible_2cell_rassociator _ _ _)
                             (disp_rassociator ff1 ff2 ff3).
Show proof.
  exists (disp_lassociator ff1 ff2 ff3).
  split.
  - apply disp_rassociator_lassociator.
  - apply disp_lassociator_rassociator.

Lemma disp_lassociator_to_rassociator_post' {a b c d : C}
      {f : Ca,b} {g : Cb,c} {h : Cc,d} {k : Ca,d}
      {x : k ==> (f · g) · h}
      {y : k ==> f · (g · h)}
      (p : x = y lassociator f g h)
      {aa : D a} {bb : D b} {cc : D c} {dd : D d}
      {ff : aa -->[f] bb}
      {gg : bb -->[g] cc}
      {hh : cc -->[h] dd}
      {kk : aa -->[k] dd}
      (xx : kk ==>[x] (ff ;; gg) ;; hh)
      (yy : kk ==>[y] ff ;; (gg ;; hh))
      (q := lassociator_to_rassociator_post x y p)
      (pp : xx = transportb (λ x, _ ==>[x] _) p (yy •• disp_lassociator ff gg hh))
  : xx •• disp_rassociator ff gg hh = transportb (λ x, _ ==>[x] _) q (yy).
Show proof.
  etrans.
  { use disp_lhs_right_invert_cell.
    - exact y.
    - apply is_invertible_2cell_rassociator.
    - exact yy.
    - apply is_disp_invertible_2cell_rassociator.
    - apply lassociator_to_rassociator_post. exact p.
    - cbn. etrans. { apply pp. }
      apply maponpaths_2.
      apply cellset_property.
  }
  apply maponpaths_2. apply cellset_property.

Lemma disp_lassociator_to_rassociator_post {a b c d : C}
      {f : Ca,b} {g : Cb,c} {h : Cc,d} {k : Ca,d}
      {x : k ==> (f · g) · h}
      {y : k ==> f · (g · h)}
      {aa : D a} {bb : D b} {cc : D c} {dd : D d}
      {ff : aa -->[f] bb}
      {gg : bb -->[g] cc}
      {hh : cc -->[h] dd}
      {kk : aa -->[k] dd}
      (xx : kk ==>[x] (ff ;; gg) ;; hh)
      (yy : kk ==>[y] ff ;; (gg ;; hh))
      (q : x rassociator f g h = y)
      (p := rassociator_to_lassociator_post _ _ q : x = y lassociator f g h)
      (pp : xx = transportb (λ x, _ ==>[x] _) p (yy •• disp_lassociator ff gg hh))
  : xx •• disp_rassociator ff gg hh = transportb (λ x, _ ==>[x] _) q (yy).
Show proof.
  etrans.
  { use disp_lassociator_to_rassociator_post'.
    - exact y.
    - exact p.
    - exact yy.
    - exact pp.
  }
  apply maponpaths_2. apply cellset_property.

Lemma disp_lassociator_to_rassociator_pre {a b c d : C}
      {f : Ca,b} {g : Cb,c} {h : Cc, d} {k : Ca,d}
      {x : f · (g · h) ==> k}
      {y : (f · g) · h ==> k}
      {aa : D a} {bb : D b} {cc : D c} {dd : D d}
      {ff : aa -->[f] bb}
      {gg : bb -->[g] cc}
      {hh : cc -->[h] dd}
      {kk : aa -->[k] dd}
      (xx : ff ;; (gg ;; hh) ==>[x] kk)
      (yy : (ff ;; gg) ;; hh ==>[y] kk)
      (q : rassociator f g h x = y)
      (p := rassociator_to_lassociator_pre _ _ q : x = lassociator f g h y)
      (pp : xx = transportb (λ x, _ ==>[x] _) p (disp_lassociator ff gg hh •• yy))
  : disp_rassociator ff gg hh •• xx = transportb (λ x, _ ==>[x] _) q (yy).
Show proof.
  etrans.
  { use disp_lhs_left_invert_cell.
    - exact y.
    - apply is_invertible_2cell_rassociator.
    - exact yy.
    - apply is_disp_invertible_2cell_rassociator.
    - apply lassociator_to_rassociator_pre. exact p.
    - cbn. etrans. { apply pp. }
      apply maponpaths_2.
      apply cellset_property.
  }
  apply maponpaths_2.
  apply cellset_property.

Lemma disp_lunitor_lwhisker {a b c : C} {f : Ca,b} {g : Cb,c}
      {aa : D a} {bb : D b} {cc : D c}
      (ff : aa -->[f] bb)
      (gg : bb -->[g] cc)
  : (disp_rassociator _ _ _ •• (ff ◃◃ disp_lunitor gg)) =
    transportb (λ α, _ ==>[α] _) (lunitor_lwhisker _ _)
               (disp_runitor ff ▹▹ gg).
Show proof.
  etrans.
  { use disp_lassociator_to_rassociator_pre.
    - exact (runitor f g).
    - exact (disp_runitor ff ▹▹ gg).
    - apply lunitor_lwhisker.
    - apply pathsinv0.
      etrans.
      { apply maponpaths. apply disp_runitor_rwhisker. }
      etrans.
      { apply (transport_f_f (λ α, _ ==>[α] _)). }
      apply (transportf_set (λ α, _ ==>[α] _)).
      apply cellset_property.
  }
  apply maponpaths_2, cellset_property.

Lemma disp_rwhisker_transport_left {a b c : C}
      {f1 f2 : Ca,b} {g : Cb,c}
      {x x' : f1 ==> f2} (p : x = x')
      {aa : D a} {bb : D b} {cc : D c}
      {ff1 : aa -->[f1] bb}
      {ff2 : aa -->[f2] bb}
      (xx : ff1 ==>[x] ff2)
      (gg : bb -->[g] cc)
  : (transportf (λ x, _ ==>[x] _) p xx) ▹▹ gg =
    transportf (λ x, _ ==>[x g] _) p (xx ▹▹ gg).
Show proof.
  induction p. apply idpath.

Lemma disp_rwhisker_transport_left_new {a b c : C}
      {f1 f2 : Ca,b} {g : Cb,c}
      {x x' : f1 ==> f2} (p : x = x')
      {aa : D a} {bb : D b} {cc : D c}
      {ff1 : aa -->[f1] bb}
      {ff2 : aa -->[f2] bb}
      (xx : ff1 ==>[x] ff2)
      (gg : bb -->[g] cc)
  : (transportf (λ x, _ ==>[x] _) p xx) ▹▹ gg =
    transportf (λ x, _ ==>[x] _) (maponpaths (λ x, x g) p) (xx ▹▹ gg).
Show proof.
  induction p. apply idpath.

Lemma disp_rwhisker_transport_right {a b c : C}
      {f : Ca,b} {g1 g2 : Cb,c}
      {x x' : g1 ==> g2} (p : x = x')
      {aa : D a} {bb : D b} {cc : D c}
      {ff : aa -->[f] bb}
      (gg1 : bb -->[g1] cc)
      (gg2 : bb -->[g2] cc)
      (xx : gg1 ==>[x] gg2)
  : ff ◃◃ (transportf (λ x, _ ==>[x] _) p xx) =
    transportf (λ x, _ ==>[x] _) (maponpaths (λ x, f x) p) (ff ◃◃ xx).
Show proof.
  induction p. apply idpath.

Definition disp_lwhisker_vcomp_alt
           {a b c : C} {f : Ca,b} {g h i : Cb,c}
           {η : g ==> h} {φ : h ==> i}
           {x : D a} {y : D b} {z : D c} {ff : x -->[f] y}
           {gg : y -->[g] z} {hh : y -->[h] z} {ii : y -->[i] z}
           (ηη : gg ==>[η] hh) (φφ : hh ==>[φ] ii)
  : ff ◃◃ (ηη •• φφ)
    =
    transportf (λ α, _ ==>[α] _) (lwhisker_vcomp _ _ _) ((ff ◃◃ ηη) •• (ff ◃◃ φφ)).
Show proof.
  refine (!_).
  apply (@transportf_transpose_left _ (λ α, _ ==>[α] _)).
  apply disp_lwhisker_vcomp.

Definition disp_rwhisker_vcomp_alt
           {a b c : C} {f g h : Ca,b} {i : Cb,c}
           {η : f ==> g} {φ : g ==> h}
           {x : D a} {y : D b} {z : D c}
           {ff : x -->[f] y} {gg : x -->[g] y} {hh : x -->[h] y} {ii : y -->[i] z}
           (ηη : ff ==>[η] gg) (φφ : gg ==>[φ] hh)
  : (ηη •• φφ) ▹▹ ii
    =
    transportf (λ α, _ ==>[α] _) (rwhisker_vcomp _ _ _) ((ηη ▹▹ ii) •• (φφ ▹▹ ii)).
Show proof.
  refine (!_).
  apply (@transportf_transpose_left _ (λ α, _ ==>[α] _)).
  apply disp_rwhisker_vcomp.

Definition disp_vcomp_whisker_alt
           {a b c : C} {f g : Ca,b} {h i : Cb,c}
           (η : f ==> g) (φ : h ==> i)
           (x : D a) (y : D b) (z : D c)
           (ff : x -->[f] y) (gg : x -->[g] y) (hh : y -->[h] z) (ii : y -->[i] z)
           (ηη : ff ==>[η] gg) (φφ : hh ==>[φ] ii)
  : (ff ◃◃ φφ) •• (ηη ▹▹ ii)
    =
    transportf (λ α, _ ==>[α] _) (vcomp_whisker _ _) ((ηη ▹▹ hh) •• (gg ◃◃ φφ)).
Show proof.
  refine (!_).
  apply (@transportf_transpose_left _ (λ α, _ ==>[α] _)).
  apply disp_vcomp_whisker.

Definition disp_id2_rwhisker_alt
           {a b c : C} {f : Ca,b} {g : Cb,c}
           {x : D a} {y : D b} {z : D c}
           (ff : x -->[f] y) (gg : y -->[g] z)
  : transportf (λ α, _ ==>[α] _) (id2_rwhisker _ _) (disp_id2 ff ▹▹ gg)
    =
    disp_id2 (ff ;; gg).
Show proof.
  apply (@transportf_transpose_left _ (λ α, _ ==>[α] _)).
  apply disp_id2_rwhisker.

Definition disp_vcomp_runitor_alt
           {a b : C} {f g : Ca,b} {η : f ==> g}
           {x : D a} {y : D b} {ff : x -->[f] y} {gg : x -->[g] y}
           (ηη : ff ==>[η] gg)
  : disp_runitor ff •• ηη
    =
    transportf
      (λ α, _ ==>[α] _)
      (vcomp_runitor _ _ _)
      ((ηη ▹▹ id_disp _) •• disp_runitor gg).
Show proof.
  refine (!_).
  etrans.
  {
    apply maponpaths.
    apply disp_vcomp_runitor.
  }
  apply (transportfbinv (λ z, _ ==>[ z ] _) _ _).

Definition disp_vcomp_lcancel
           {b₁ b₂ : C}
           {f g h : b₁ --> b₂}
           {α : f ==> g}
           {β : g ==> h}
           ( : is_invertible_2cell α)
           {bb₁ : D b₁}
           {bb₂ : D b₂}
           {ff : bb₁ -->[ f ] bb₂}
           {gg : bb₁ -->[ g ] bb₂}
           {hh : bb₁ -->[ h ] bb₂}
           {αα : ff ==>[ α ] gg}
           {ββ₁ ββ₂ : gg ==>[ β ] hh}
           (Hαα : is_disp_invertible_2cell αα)
           (p : αα •• ββ₁ = αα •• ββ₂)
  : ββ₁ = ββ₂.
Show proof.
  pose (αα_cell := (αα ,, Hαα) : disp_invertible_2cell (make_invertible_2cell ) ff gg).
  assert (q := maponpaths (λ z, disp_inv_cell αα_cell •• z) p).
  cbn in q.
  rewrite !disp_vassocr in q.
  pose (disp_vcomp_linv αα_cell) as z.
  cbn in z.
  rewrite !z in q.
  unfold transportb in q.
  rewrite !disp_mor_transportf_postwhisker in q.
  rewrite !transport_f_f in q.
  rewrite !disp_id2_left in q.
  unfold transportb in q.
  rewrite !transport_f_f in q.
  pose (q' := @transportb_transpose_right
                _
                (λ z, _ ==>[ z ] _)
                _ _ _ _ _
                q).
  rewrite transportbfinv in q'.
  exact q'.

Definition disp_vcomp_rcancel
           {b₁ b₂ : C}
           {f g h : b₁ --> b₂}
           {α : f ==> g}
           {β : g ==> h}
           ( : is_invertible_2cell β)
           {bb₁ : D b₁}
           {bb₂ : D b₂}
           {ff : bb₁ -->[ f ] bb₂}
           {gg : bb₁ -->[ g ] bb₂}
           {hh : bb₁ -->[ h ] bb₂}
           {αα₁ : ff ==>[ α ] gg}
           {αα₂ : ff ==>[ α ] gg}
           {ββ : gg ==>[ β ] hh}
           (Hββ : is_disp_invertible_2cell ββ)
           (p : αα₁ •• ββ = αα₂ •• ββ)
  : αα₁ = αα₂.
Show proof.
  assert (q := maponpaths (λ z, z •• pr1 Hββ) p).
  cbn in q.
  rewrite !disp_vassocl in q.
  rewrite !(pr12 Hββ) in q.
  unfold transportb in q.
  rewrite !disp_mor_transportf_prewhisker in q.
  rewrite !transport_f_f in q.
  rewrite !disp_id2_right in q.
  unfold transportb in q.
  rewrite !transport_f_f in q.
  pose (q' := @transportb_transpose_right
                _
                (λ z, _ ==>[ z ] _)
                _ _ _ _ _
                q).
  rewrite transportbfinv in q'.
  exact q'.

Definition disp_id2_left_alt
           {x y : C}
           {f g : x --> y}
           {η : f ==> g}
           {xx : D x}
           {yy : D y}
           {ff : xx -->[ f ] yy}
           {gg : xx -->[ g ] yy}
           (ηη : ff ==>[ η ] gg)
  : ηη
    =
    transportf (λ z, ff ==>[ z ] gg) (id2_left η) (disp_id2 ff •• ηη).
Show proof.
  exact (!(@transportf_transpose_left
             _
             (λ z, _ ==>[ z ] _)
             _ _
             _
             _ _
             (disp_id2_left ηη))).

Definition disp_rwhisker_rwhisker_rassociator
           {w x y z : C}
           {f₁ f₂ : w --> x}
           {α : f₁ ==> f₂}
           {g : x --> y}
           {h : y --> z}
           {ww : D w}
           {xx : D x}
           {yy : D y}
           {zz : D z}
           {ff₁ : ww -->[ f₁ ] xx}
           {ff₂ : ww -->[ f₂ ] xx}
           (αα : ff₁ ==>[ α ] ff₂)
           (gg : xx -->[ g ] yy)
           (hh : yy -->[ h ] zz)
  : transportb
      (λ z, _ ==>[ z ] _)
      (rwhisker_rwhisker_alt h g α)
      (disp_rassociator ff₁ gg hh •• (αα ▹▹ (gg ;; hh)))
    =
    (αα ▹▹ gg ▹▹ hh) •• disp_rassociator ff₂ gg hh.
Show proof.
  refine (!_).
  refine (disp_id2_left_alt _ @ _).
  etrans.
  {
    apply maponpaths.
    apply maponpaths_2.
    exact (!(@transportf_transpose_left
               _
               (λ z, _ ==>[ z ] _)
               _ _
               _
               _ _
               (disp_rassociator_lassociator _ ff₁ gg hh))).
  }
  rewrite disp_mor_transportf_postwhisker.
  rewrite transport_f_f.
  rewrite !disp_vassocl.
  unfold transportb.
  rewrite transport_f_f.
  etrans.
  {
    do 2 apply maponpaths.
    rewrite disp_vassocr.
    rewrite disp_rwhisker_rwhisker.
    unfold transportb.
    rewrite disp_mor_transportf_postwhisker.
    rewrite transport_f_f.
    rewrite !disp_vassocl.
    rewrite disp_lassociator_rassociator.
    unfold transportb.
    rewrite disp_mor_transportf_prewhisker.
    rewrite disp_id2_right.
    unfold transportb.
    rewrite !transport_f_f.
    apply idpath.
  }
  rewrite disp_mor_transportf_prewhisker.
  rewrite transport_f_f.
  apply maponpaths_2.
  apply cellset_property.

End Derived_Laws.

Total bicategory of a displayed bicategory


Section total_prebicat.

Variable D : disp_prebicat.

Definition total_prebicat_1_data : precategory_data
  := total_category_ob_mor D ,, total_category_id_comp D.

Definition total_prebicat_cell_struct : prebicat_2cell_struct (total_category_ob_mor D)
  := λ a b f g, η : pr1 f ==> pr1 g, pr2 f ==>[η] pr2 g.

Definition total_prebicat_1_id_comp_cells : prebicat_1_id_comp_cells
  := (total_prebicat_1_data,, total_prebicat_cell_struct).

Definition total_prebicat_2_id_comp_struct
  : prebicat_2_id_comp_struct total_prebicat_1_id_comp_cells.
Show proof.
  repeat split; cbn; unfold total_prebicat_cell_struct.
  - intros. exists (id2 _). exact (disp_id2 _).
  - intros. exists (lunitor _). exact (disp_lunitor _).
  - intros. exists (runitor _). exact (disp_runitor _).
  - intros. exists (linvunitor _). exact (disp_linvunitor _).
  - intros. exists (rinvunitor _). exact (disp_rinvunitor _).
  - intros. exists (rassociator _ _ _).
    exact (disp_rassociator _ _ _).
  - intros. exists (lassociator _ _ _).
    exact (disp_lassociator _ _ _).
  - intros a b f g h r s. exists (pr1 r pr1 s).
    exact (pr2 r •• pr2 s).
  - intros a b d f g1 g2 r. exists (pr1 f pr1 r).
    exact (pr2 f ◃◃ pr2 r).
  - intros a b c f1 f2 g r. exists (pr1 r pr1 g).
    exact (pr2 r ▹▹ pr2 g).

Definition total_prebicat_data : prebicat_data
  := _ ,, total_prebicat_2_id_comp_struct.

Lemma total_prebicat_laws : prebicat_laws total_prebicat_data.
Show proof.
  repeat split; intros.
  - use total2_paths_b.
    + apply id2_left.
    + apply disp_id2_left.
  - use total2_paths_b.
    + apply id2_right.
    + apply disp_id2_right.
  - use total2_paths_b.
    + apply vassocr.
    + apply disp_vassocr.
  - use total2_paths_b.
    + apply lwhisker_id2.
    + apply disp_lwhisker_id2.
  - use total2_paths_b.
    + apply id2_rwhisker.
    + apply disp_id2_rwhisker.
  - use total2_paths_b.
    + apply lwhisker_vcomp.
    + apply disp_lwhisker_vcomp.
  - use total2_paths_b.
    + apply rwhisker_vcomp.
    + apply disp_rwhisker_vcomp.
  - use total2_paths_b.
    + apply vcomp_lunitor.
    + apply disp_vcomp_lunitor.
  - use total2_paths_b.
    + apply vcomp_runitor.
    + apply disp_vcomp_runitor.
  - use total2_paths_b.
    + apply lwhisker_lwhisker.
    + apply disp_lwhisker_lwhisker.
  - use total2_paths_b.
    + apply rwhisker_lwhisker.
    + apply disp_rwhisker_lwhisker.
  - use total2_paths_b.
    + apply rwhisker_rwhisker.
    + apply disp_rwhisker_rwhisker.
  - use total2_paths_b.
    + apply vcomp_whisker.
    + apply disp_vcomp_whisker.
  - use total2_paths_b.
    + apply lunitor_linvunitor.
    + apply disp_lunitor_linvunitor.
  - use total2_paths_b.
    + apply linvunitor_lunitor.
    + apply disp_linvunitor_lunitor.
  - use total2_paths_b.
    + apply runitor_rinvunitor.
    + apply disp_runitor_rinvunitor.
  - use total2_paths_b.
    + apply rinvunitor_runitor.
    + apply disp_rinvunitor_runitor.
  - use total2_paths_b.
    + apply lassociator_rassociator.
    + apply disp_lassociator_rassociator.
  - use total2_paths_b.
    + apply rassociator_lassociator.
    + apply disp_rassociator_lassociator.
  - use total2_paths_b.
    + apply runitor_rwhisker.
    + apply disp_runitor_rwhisker.
  - use total2_paths_b.
    + apply lassociator_lassociator.
    + apply disp_lassociator_lassociator.

Definition total_prebicat : prebicat := _ ,, total_prebicat_laws.
End total_prebicat.

Definition has_disp_cellset (D : disp_prebicat) : UU
  := (a b : C) (f g : Ca,b) (x : f ==> g)
       (aa : D a) (bb : D b)
       (ff : aa -->[f] bb)
       (gg : aa -->[g] bb),
     isaset (ff ==>[x] gg).

Definition disp_bicat : UU
  := D : disp_prebicat, has_disp_cellset D.

Coercion disp_prebicat_of_disp_bicat (D : disp_bicat)
  : disp_prebicat
  := pr1 D.

Definition disp_cellset_property (D : disp_bicat)
  : has_disp_cellset D
  := pr2 D.

Lemma isaset_cells_total_prebicat (D : disp_bicat)
  : isaset_cells (total_prebicat D).
Show proof.
red.
cbn.
intros.
unfold total_prebicat_cell_struct.
apply isaset_total2.
- apply cellset_property.
- intros.
  apply disp_cellset_property.

Definition total_bicat (D : disp_bicat) : bicat
  := total_prebicat D,, isaset_cells_total_prebicat D.

End disp_prebicat.

Arguments disp_prebicat_1_id_comp_cells _ : clear implicits.
Arguments disp_prebicat_data _ : clear implicits.
Arguments disp_prebicat _ : clear implicits.
Arguments disp_bicat _ : clear implicits.

Displayed left and right unitors coincide on the identity


Theorem disp_lunitor_runitor_identity {C : bicat} {D : disp_bicat C} (a : C) (aa : D a)
  : disp_lunitor (id_disp aa) =
    cell_transportb (lunitor_runitor_identity a) (disp_runitor (id_disp aa)).
Show proof.
  set (TT := fiber_paths (lunitor_runitor_identity (C := total_bicat D) (a ,, aa))).
  cbn in TT.
  apply cell_transportf_to_b.
  etrans.
  2: now apply TT.
  unfold cell_transportf.
  apply maponpaths_2.
  apply cellset_property.

Theorem disp_runitor_lunitor_identity {C : bicat} {D : disp_bicat C} {a : C} (aa : D a)
  : disp_runitor (id_disp aa) =
    transportb (λ x, disp_2cells x _ _) (runitor_lunitor_identity a)
               (disp_lunitor (id_disp aa)).
Show proof.
  apply (transportf_transpose_right (P := (λ x, disp_2cells x _ _))).
  apply pathsinv0.
  etrans.
  1: now apply disp_lunitor_runitor_identity.
  unfold cell_transportb.
  apply maponpaths_2, cellset_property.

Lemma adjequiv_base_adjequiv_tot
      {B : bicat}
      (HB : is_univalent_2_0 B)
      {D : disp_bicat B}
      {a b : B}
  : adjoint_equivalence a b (aa : D a), (bb : D b), @adjoint_equivalence (total_bicat D) (a ,, aa) (b ,, bb).
Show proof.
  use (J_2_0 HB (λ _ _ _, _)).
  intros c aa.
  exact (aa ,, internal_adjoint_equivalence_identity _).

Useful properties


Definition disp_2cells_isaprop
           {B : bicat} (D : disp_prebicat_1_id_comp_cells B)
  := (a b : B) (f g : a --> b) (x : f ==> g)
       (aa : D a) (bb : D b) (ff : aa -->[f] bb) (gg : aa -->[g] bb),
    isaprop (disp_2cells x ff gg).

Definition disp_2cells_iscontr
           {B : bicat} (D : disp_prebicat_1_id_comp_cells B)
  := (a b : B) (f g : a --> b) (x : f ==> g)
       (aa : D a) (bb : D b) (ff : aa -->[f] bb) (gg : aa -->[g] bb),
     iscontr (disp_2cells x ff gg).

Definition disp_locally_groupoid
           {B : bicat} (D : disp_bicat B)
  := (a b : B) (f g : a --> b) (x : invertible_2cell f g)
       (aa : D a) (bb : D b) (ff : aa -->[f] bb) (gg : aa -->[g] bb)
       (xx : disp_2cells x ff gg), is_disp_invertible_2cell x xx.

Definition disp_locally_sym
           {B : bicat} (D : disp_bicat B)
  := (a b : B) (f g : a --> b) (x : invertible_2cell f g)
       (aa : D a) (bb : D b) (ff : aa -->[f] bb) (gg : aa -->[g] bb)
       (xx : disp_2cells x ff gg), disp_2cells (x^-1) gg ff.

Definition make_disp_locally_groupoid
           {B : bicat} (D : disp_bicat B)
           (H : disp_locally_sym D)
           (HD : disp_2cells_isaprop D)
  : disp_locally_groupoid D.
Show proof.
  intros a b f g x aa bb ff gg xx.
  use tpair.
  - apply H.
    exact xx.
  - split; apply HD.

Definition disp_locally_groupoid_over_id
           {B : bicat} (D : disp_bicat B)
  : UU
  := (a b : B)
       (f : B a, b )
       (aa : D a)
       (bb : D b)
       (ff gg : aa -->[ f] bb)
       (xx : disp_2cells (id2_invertible_2cell f) ff gg),
     is_disp_invertible_2cell (is_invertible_2cell_id₂ f) xx.

Definition make_disp_locally_groupoid_univalent_2_1
           {B : bicat} (D : disp_bicat B)
           (HD : disp_locally_groupoid_over_id D)
           (HB : is_univalent_2_1 B)
  : disp_locally_groupoid D.
Show proof.
  use (J_2_1 HB).
  exact HD.

Definition disp_2cells_isaprop_from_disp_2cells_iscontr
  {B : bicat} (D : disp_prebicat_1_id_comp_cells B)
  : disp_2cells_iscontr D -> disp_2cells_isaprop D.
Show proof.
  intro c ; intro ; intros.
  apply isapropifcontr.
  apply c.

Definition disp_2cells_isgroupoid_from_disp_2cells_iscontr
  {B : bicat} (D : disp_bicat B)
  : disp_2cells_iscontr D -> disp_locally_groupoid D.
Show proof.
  intro c ; intro ; intros.
  simple refine (_ ,, _).
  - apply c.
  - split; apply isapropifcontr, c.

Section HomDisplayedCategory.
  Context {B : bicat}
          {D : disp_bicat B}.

  Notation "f' ==>[ x ] g'" := (disp_2cells x f' g') (at level 60).
  Notation "rr •• ss" := (disp_vcomp2 rr ss) (at level 60).

  Definition disp_hom_ob_mor
             {x y : B}
             (xx : D x)
             (yy : D y)
  : disp_cat_ob_mor (hom x y).
  Show proof.
    simple refine (_ ,, _).
    - exact (λ f, xx -->[ f ] yy).
    - exact (λ f g ff gg α, ff ==>[ α ] gg).

  Definition disp_hom_id_comp
             {x y : B}
             (xx : D x)
             (yy : D y)
    : disp_cat_id_comp _ (disp_hom_ob_mor xx yy).
  Show proof.
    simple refine (_ ,, _).
    - exact (λ f ff, disp_id2 ff).
    - exact (λ f g h α β ff gg hh αα ββ, αα •• ββ).

  Definition disp_hom_data
             {x y : B}
             (xx : D x)
             (yy : D y)
    : disp_cat_data (hom x y).
  Show proof.
    simple refine (_ ,, _).
    - exact (disp_hom_ob_mor xx yy).
    - exact (disp_hom_id_comp xx yy).

  Definition disp_hom_laws
             {x y : B}
             (xx : D x)
             (yy : D y)
    : disp_cat_axioms _ (disp_hom_data xx yy).
  Show proof.
    repeat split ; intro ; intros ; cbn.
    - rewrite disp_id2_left.
      apply maponpaths_2.
      apply cellset_property.
    - rewrite disp_id2_right.
      apply maponpaths_2.
      apply cellset_property.
    - rewrite disp_vassocr.
      apply maponpaths_2.
      apply cellset_property.
    - apply D.

  Definition disp_hom
             {x y : B}
             (xx : D x)
             (yy : D y)
    : disp_cat (hom x y).
  Show proof.
    simple refine (_ ,, _).
    - exact (disp_hom_data xx yy).
    - exact (disp_hom_laws xx yy).
End HomDisplayedCategory.

Notations.


Module Notations.

Export Bicat.Notations.

Notation "f' ==>[ x ] g'" := (disp_2cells x f' g') (at level 60).
Notation "f' <==[ x ] g'" := (disp_2cells x g' f') (at level 60, only parsing).
Notation "rr •• ss" := (disp_vcomp2 rr ss) (at level 60).
Notation "ff ◃◃ rr" := (disp_lwhisker ff rr) (at level 60).
Notation "rr ▹▹ gg" := (disp_rwhisker gg rr) (at level 60).

End Notations.