Proposition formula_to_per_axioms {A : ty H} (φ : form A) : per_axioms (formula_to_per_form φ). Proof. split ; cbn. - unfold per_symm_axiom. simplify. pose (x₁ := π₂ (π₁ (tm_var ((𝟙 ×h A) ×h A)))). pose (x₂ := π₂ (tm_var ((𝟙 ×h A) ×h A))). fold x₁ x₂. do 2 use forall_intro. use impl_intro. use weaken_right. use conj_intro. + use weaken_left. use hyperdoctrine_eq_sym. apply hyperdoctrine_hyp. + use hyperdoctrine_eq_transportf. * exact x₁. * use weaken_left. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. - unfold per_trans_axiom. simplify. pose (x₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h A) ×h A) ×h A))))). pose (x₂ := π₂ (π₁ (tm_var (((𝟙 ×h A) ×h A) ×h A)))). pose (x₃ := π₂ (tm_var (((𝟙 ×h A) ×h A) ×h A))). fold x₁ x₂ x₃. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use conj_intro. + use hyperdoctrine_eq_trans. * exact x₂. * do 2 use weaken_left. apply hyperdoctrine_hyp. * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + use weaken_left. 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.