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)).
Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering.