Proposition exp_partial_setoid_per_axioms : per_axioms exp_partial_setoid_per_form. Proof. split. - unfold per_symm_axiom ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. pose (f := π₂ (π₁ (tm_var ((𝟙 ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y))))). pose (g := π₂ (tm_var ((𝟙 ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)))). fold f g. use conj_intro. + use exp_partial_setoid_eq_is_function. * exact f. * use weaken_right. apply hyperdoctrine_hyp. * use weaken_left. apply hyperdoctrine_hyp. + use weaken_right. use exp_partial_setoid_eq_sym. apply hyperdoctrine_hyp. - unfold per_trans_axiom ; cbn. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify. pose (f := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)))))). pose (g := π₂ (π₁ (tm_var (((𝟙 ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y))))). pose (h := π₂ (tm_var (((𝟙 ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)))). fold f g h. use conj_intro. + do 2 use weaken_left. apply hyperdoctrine_hyp. + use exp_partial_setoid_eq_trans. * exact g. * use weaken_left. use weaken_right. apply hyperdoctrine_hyp. * do 2 use weaken_right. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos. Require Import UniMath.CategoryTheory.Hyperdoctrines.GenericPredicate. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms.