Definition partial_setoids_disp_functor_ess_split_surj : disp_functor_disp_ess_split_surj partial_setoids_disp_functor. Proof. refine (λ (A : ty H) f, _). simple refine (_ ,, _). - exact (partial_setoids_disp_functor_eso_form (pr21 f)). - simple refine (_ ,, _ ,, _ ,, _). + simple refine ((_ ,, _) ,, tt) ; cbn. * apply partial_setoids_disp_functor_eso_mor. exact (pr2 f). * apply partial_setoids_disp_functor_eso_mor_comm. + simple refine ((_ ,, _) ,, tt) ; cbn. * apply partial_setoids_disp_functor_eso_inv. * apply partial_setoids_disp_functor_eso_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.PERConstantObjects.