Lemma isaprop_disp_cat_axioms (C : category) (D : disp_cat_data C) : isaprop (disp_cat_axioms C D). Proof. apply isofhlevelsn. intro X. set (XR := ( _ ,, X) : disp_cat C). apply isofhleveltotal2. - repeat (apply impred; intro). apply (@homsets_disp _ XR). - intros x. repeat (apply isofhleveldirprod); repeat (apply impred; intro). + apply (@homsets_disp _ XR). + apply (@homsets_disp _ XR). + apply isapropiscontr. Qed.
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.