Proposition pair_partial_setoid_morphism_pr2 : partial_setoid_comp_morphism pair_partial_setoid_morphism (partial_setoid_pr2 _ _) = ψ. Proof. use eq_partial_setoid_morphism ; cbn. - use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. unfold partial_setoid_pr2_form. simplify_form. rewrite !partial_setoid_subst. simplify. pose (w := π₁ (π₁ (tm_var ((W ×h Y) ×h X ×h Y)))). pose (x := π₁ (π₂ (tm_var ((W ×h Y) ×h X ×h Y)))). pose (y' := π₂ (π₁ (tm_var ((W ×h Y) ×h X ×h Y)))). pose (y := π₂ (π₂ (tm_var ((W ×h Y) ×h X ×h Y)))). fold w x y y'. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var ((W ×h Y) ×h X ×h Y)))). fold w y'. use hyp_ltrans. use weaken_right. use hyp_sym. use hyp_ltrans. use weaken_right. use (partial_setoid_mor_eq_defined ψ). + exact w. + exact y. + use weaken_right. exact (partial_setoid_mor_dom_defined ψ _ _ (hyperdoctrine_hyp _)). + use weaken_left. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. - use (exists_elim (partial_setoid_mor_hom_exists φ _)). + exact (π₁ (tm_var _)). + use (partial_setoid_mor_dom_defined ψ _ (π₂ (tm_var _))). rewrite <- hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. + unfold partial_setoid_pr2_form. simplify_form. rewrite !partial_setoid_subst. simplify. use exists_intro. * exact (⟨ π₂ (tm_var _) , π₂ (π₁ (tm_var _)) ⟩). * simplify_form. rewrite !partial_setoid_subst. simplify. use conj_intro. ** use conj_intro. *** use weaken_right. apply hyperdoctrine_hyp. *** use weaken_left. rewrite <- hyperdoctrine_pair_eta. apply hyperdoctrine_hyp. ** use conj_intro. *** use weaken_right. exact (partial_setoid_mor_cod_defined φ _ _ (hyperdoctrine_hyp _)). *** use weaken_left. use (partial_setoid_mor_cod_defined ψ). { exact (π₁ (π₁ (tm_var _))). } rewrite <- hyperdoctrine_pair_eta. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation. 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.