Proposition omega_per_axioms : per_axioms omega_per_form. Proof. split. - unfold per_symm_axiom ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. pose (φ := Prf [ π₂ (π₁ (tm_var (((𝟙 : ty H) ×h Ω) ×h Ω))) ] ). pose (ψ := Prf [ π₂ (tm_var (((𝟙 : ty H) ×h Ω) ×h Ω)) ]). fold φ ψ. use iff_sym. apply hyperdoctrine_hyp. - unfold per_trans_axiom ; cbn. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify. cbn. pose (φ := Prf [ π₂ (π₁ (π₁ (tm_var ((((𝟙 : ty H) ×h Ω) ×h Ω) ×h Ω)))) ]). pose (ψ := Prf [ π₂ (π₁ (tm_var ((((𝟙 : ty H) ×h Ω) ×h Ω) ×h Ω))) ]). pose (χ := Prf [ π₂ (tm_var ((((𝟙 : ty H) ×h Ω) ×h Ω) ×h Ω)) ]). fold φ ψ χ. use iff_trans. + exact ψ. + use weaken_left. apply hyperdoctrine_hyp. + 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.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. 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. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERTerminal. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMonomorphisms.