fact: Definition disp_prebicat_ops (D : disp_prebicat_1_id_comp_cells C) : UU := (∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y), f' ==>[id2 _] f') × (∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y), id_disp x ;; f' ==>[lunitor _] f') × (∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y), f' ;; id_disp y ==>[runitor _] f') × (∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y), id_disp x ;; f' <==[linvunitor _] f') × (∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y), f' ;; id_disp y <==[rinvunitor _] f') × (∏ (a b c d : C) (f : C⟦a,b⟧) (g : C⟦b,c⟧) (h : C⟦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), (ff ;; gg) ;; hh ==>[rassociator _ _ _] ff ;; (gg ;; hh)) × (∏ (a b c d : C) (f : C⟦a,b⟧) (g : C⟦b,c⟧) (h : C⟦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), ff ;; (gg ;; hh) ==>[lassociator _ _ _] (ff ;; gg) ;; hh) × (∏ (a b : C) (f g h : C⟦a,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 : C⟦a,b⟧) (g1 g2 : C⟦b,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 : C⟦a,b⟧) (g : C⟦b,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).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Univalence