Proposition partial_setoids_disp_functor_eso_inv_laws : partial_setoid_morphism_laws partial_setoids_disp_functor_eso_inv_form. Proof. unfold partial_setoids_disp_functor_eso_inv_form. repeat split. - unfold partial_setoid_mor_dom_defined_law ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. exact (partial_setoid_mor_dom_defined φ _ _ (hyperdoctrine_hyp _)). - unfold partial_setoid_mor_cod_defined_law ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. use eq_in_formula_to_partial_setoid. + use from_eq_in_eq_partial_setoid. exact (partial_setoid_mor_cod_defined φ _ _ (hyperdoctrine_hyp _)). + simplify_form. use exists_intro. * exact (π₂ (π₁ (tm_var _))). * simplify. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_eq_defined_law ; cbn. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. simplify. use (partial_setoid_mor_eq_defined φ). + exact (π₂ (π₁ (π₁ (π₁ (tm_var _))))). + exact (π₂ (π₁ (tm_var _))). + do 2 use weaken_left. apply hyperdoctrine_hyp. + use weaken_left. use weaken_right. unfold partial_setoid_formula ; cbn. rewrite conj_subst. use weaken_left. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law ; cbn. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify. use eq_in_formula_to_partial_setoid. + use from_eq_in_eq_partial_setoid. use (partial_setoid_mor_unique_im φ). * exact (π₂ (π₁ (π₁ (tm_var _)))). * use weaken_left. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. + simplify_form. use exists_intro. * exact (π₂ (π₁ (π₁ (tm_var _)))). * simplify. use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law ; cbn. use forall_intro. use impl_intro. use weaken_right. use (exists_elim (partial_setoid_mor_hom_exists φ (hyperdoctrine_hyp _))). simplify_form. use exists_intro. + exact (π₂ (tm_var _)). + cbn. simplify. use weaken_right. 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.