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
*********************************************************************************

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.Core.Adjunctions.
Require Import UniMath.Bicategories.Core.Univalence.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

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 αα = ββ.
Proof.
  unfold cell_transportf.
  apply (transportf_pathsinv0 (λ x : f ==> g, ff ==>[x] gg)).
  exact ee.
Defined.

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 αα = ββ.
Proof.
  apply cell_transportf_pathsinv0.
  apply pathsinv0.
  exact ee.
Defined.

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 ββ.
Proof.
  apply pathsinv0.
  apply (transportf_pathsinv0 (λ x : f ==> g, ff ==>[ x] gg)).
  etrans.
  { apply maponpaths_2.
    apply pathsinv0inv0. }
  exact ee.
Defined.

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 _ _ _) (ηη •• (φφ •• ψψ)) =
    ((ηη •• φφ) •• ψψ).
Proof.
  use (transportf_transpose_left (P := λ x' : f ==> k, ff ==>[x'] kk)).
  apply disp_vassocr.
Defined.

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.

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 _ _ _) (ηη •• (φφ •• ψψ)).
Proof.
  apply (transportf_transpose_right (P := λ x', _ ==>[x'] _)).
  apply pathsinv0.
  etrans.
  apply disp_vassocr.
  apply maponpaths_2.
  unfold vassocl.
  apply pathsinv0, pathsinv0inv0.
Qed.

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).
  Proof.
    induction ef; apply idpath.
  Qed.

  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).
  Proof.
    induction ef; apply idpath.
  Qed.

  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).
  Proof.
    induction ef; apply idpath.
  Qed.

  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.
  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.
  Qed.

  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.
  Proof.
    etrans.
    use (disp_lhs_right_invert_cell' _ _ _ _ pp).
    apply maponpaths_2.
    apply cellset_property.
  Qed.

  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.
  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.
  Qed.

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).
Proof.
   (disp_rassociator ff1 ff2 ff3).
  split.
  - apply disp_lassociator_rassociator.
  - apply disp_rassociator_lassociator.
Defined.

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).
Proof.
   (disp_lassociator ff1 ff2 ff3).
  split.
  - apply disp_rassociator_lassociator.
  - apply disp_lassociator_rassociator.
Defined.

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).
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.
Qed.

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).
Proof.
  etrans.
  use disp_lassociator_to_rassociator_post'.
  - exact y.
  - exact p.
  - exact yy.
  - exact pp.
  - apply maponpaths_2. apply cellset_property.
Qed.

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).
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.
Qed.

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).
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.
Qed.

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).
Proof.
  induction p. apply idpath.
Defined.

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).
Proof.
  induction p. apply idpath.
Defined.

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).
Proof.
  induction p. apply idpath.
Defined.

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 ◃◃ φφ)).
Proof.
  refine (!_).
  apply (@transportf_transpose_left _ (λ α, _ ==>[α] _)).
  apply disp_lwhisker_vcomp.
Qed.

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)).
Proof.
  refine (!_).
  apply (@transportf_transpose_left _ (λ α, _ ==>[α] _)).
  apply disp_rwhisker_vcomp.
Qed.

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 ◃◃ φφ)).
Proof.
  refine (!_).
  apply (@transportf_transpose_left _ (λ α, _ ==>[α] _)).
  apply disp_vcomp_whisker.
Qed.

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).
Proof.
  apply (@transportf_transpose_left _ (λ α, _ ==>[α] _)).
  apply disp_id2_rwhisker.
Qed.

End Derived_Laws.

Total bicategory of a displayed bicategory