Definition disp_cat' (C : category) : UU := ∑ (ob_disp : C -> UU) (mor_disp : ∏ {x y : C}, (x --> y) -> ob_disp x -> ob_disp y -> UU) (id_disp : ∏ {x : C} (xx : ob_disp x), mor_disp (identity x) xx xx) (comp_disp : ∏ {x y z : C} {f : x --> y} {g : y --> z} {xx : ob_disp x} {yy : ob_disp y} {zz : ob_disp z}, mor_disp f xx yy -> mor_disp g yy zz -> mor_disp (f · g) xx zz) (id_left_disp : ∏ {x y} {f : x --> y} {xx} {yy} (ff : mor_disp f xx yy), comp_disp (id_disp xx) ff = transportb (λ g, mor_disp g xx yy) (id_left _) ff) (id_right_disp : ∏ {x y} {f : x --> y} {xx} {yy} (ff : mor_disp f xx yy), comp_disp ff (id_disp yy) = transportb (λ g, mor_disp g xx yy) (id_right _) ff) (assoc_disp : ∏ {x y z w} {f : x --> y} {g : y --> z} {h : z --> w} {xx} {yy} {zz} {ww} (ff : mor_disp f xx yy) (gg : mor_disp g yy zz) (hh : mor_disp h zz ww), comp_disp ff (comp_disp gg hh) = transportb (λ k, mor_disp k _ _) (assoc _ _ _) (comp_disp (comp_disp ff gg) hh)), ∏ x y (f : x --> y) xx yy, isaset (mor_disp f xx 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.