Proposition disp_cat_axioms_per_subobject : disp_cat_axioms (category_of_partial_setoids H) disp_cat_data_per_subobject. Proof. repeat split. - intros. apply isaprop_per_subobject_mor_law. - intros. apply isaprop_per_subobject_mor_law. - intros. apply isaprop_per_subobject_mor_law. - intros. apply isasetaprop. apply isaprop_per_subobject_mor_law. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory.