fact: Definition disp_cat_axioms (C : category) (D : disp_cat_data C) : UU := (∏ x y (f : x --> y) (xx : D x) yy (ff : xx -->[f] yy), id_disp _ ;; ff = transportb _ (id_left _) ff) × (∏ x y (f : x --> y) (xx : D x) yy (ff : xx -->[f] yy), ff ;; id_disp _ = transportb _ (id_right _) ff) × (∏ x y z w f g h (xx : D x) (yy : D y) (zz : D z) (ww : D w) (ff : xx -->[f] yy) (gg : yy -->[g] zz) (hh : zz -->[h] ww), ff ;; (gg ;; hh) = transportb _ (assoc _ _ _) ((ff ;; gg) ;; hh)) × (∏ x y f (xx : D x) (yy : D y), isaset (xx -->[f] yy)).
imports: UniMath.Foundations.Sets UniMath.Foundations.PartD UniMath.MoreFoundations.PartA UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering