Lemma isaprop_section_disp_axioms (F : section_disp_data) (Hmor : ∏ (x y : C) (f : x --> y) (c : D x) (d : D y), isaset (c -->[f] d)) : isaprop (section_disp_axioms F). Proof. apply isapropdirprod. - apply impred; intro. apply Hmor. - do 5 (apply impred; intro). apply Hmor. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core.