Proposition partial_setoids_disp_functor_eso_inv_comm : partial_setoid_comp_morphism partial_setoids_disp_functor_eso_inv (formula_to_partial_setoid_incl partial_setoids_disp_functor_eso_form) = partial_setoid_comp_morphism φ (id_partial_setoid_morphism (eq_partial_setoid A)). Proof. use eq_partial_setoid_morphism. - cbn. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify_form. rewrite partial_setoid_subst. simplify. use hyp_rtrans. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). simplify_form. use hyp_ltrans. use weaken_right. use exists_intro. + exact (π₂ (π₁ (tm_var _))). + simplify_form. rewrite partial_setoid_subst. simplify. use conj_intro. * do 2 use weaken_left. apply hyperdoctrine_hyp. * use eq_in_eq_partial_setoid. use weaken_left. use weaken_right. apply hyperdoctrine_hyp. - cbn. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify. use exists_intro. + exact (π₂ (tm_var _)). + simplify_form. rewrite partial_setoid_subst. simplify. repeat (use conj_intro). * use weaken_left. apply hyperdoctrine_hyp. * use weaken_right. use from_eq_in_eq_partial_setoid. apply hyperdoctrine_hyp. * use exists_intro. ** exact (π₁ (π₁ (tm_var _))). ** simplify. use weaken_left. apply hyperdoctrine_hyp. Qed.
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.