Definition per_subobject_disp_functor_data : disp_functor_data (functor_identity _) (disp_cat_per_subobject H) (disp_mono_codomain (category_of_partial_setoids H)). Proof. simple refine (_ ,, _). - refine (λ (X : partial_setoid H) (φ : per_subobject X), (subobject_to_partial_setoid φ ,, subobject_to_partial_setoid_incl φ) ,, _). apply isMonic_subobject_to_partial_setoid_incl. - intros X Y ψ₁ ψ₂ φ p. refine ((subobject_to_partial_setoid_mor ψ₁ ψ₂ φ p ,, _) ,, tt). apply subobject_to_partial_setoid_mor_eq. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. 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. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMonomorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat.