Definition per_subobject_disp_functor_ess_split_surj : disp_functor_disp_ess_split_surj per_subobject_disp_functor. Proof. refine (λ (X : partial_setoid H), _). intro f. induction f as [ [ Y φ ] p ]. cbn in Y, φ, p. refine (monic_to_per_subobject φ ,, _). simple refine (_ ,, _ ,, _ ,, _). - simple refine ((_ ,, _) ,, tt) ; cbn. + apply monic_to_per_subobject_mor. exact p. + apply monic_to_per_subobject_mor_eq. - simple refine ((_ ,, _) ,, tt) ; cbn. + apply monic_to_per_subobject_inv. + apply monic_to_per_subobject_inv_comm. - apply locally_propositional_mono_cod_disp_cat. - apply locally_propositional_mono_cod_disp_cat. 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.