Definition partial_setoids_disp_functor_data : disp_functor_data (functor_to_partial_setoids H) (hyperdoctrine_formula_disp_cat H) (disp_mono_codomain _). Proof. simple refine (_ ,, _). - simple refine (λ (A : ty H) (φ : form A), make_mono_cod_fib_ob _). + exact (formula_to_partial_setoid φ). + use make_Monic. * exact (formula_to_partial_setoid_incl φ). * exact (isMonic_formula_to_partial_setoid_incl φ). - refine (λ (Γ₁ Γ₂ : ty H) (Δ : form Γ₁) (φ : form Γ₂) (s : tm Γ₁ Γ₂) p, _). simple refine ((_ ,, _) ,, tt). + exact (proof_to_partial_setoid_morphism (from_disp_mor_hyperdoctrine _ p)). + apply proof_to_partial_setoid_morphism_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.PERConstantObjects.