Proposition prod_per_axioms : per_axioms prod_per_data. Proof. split. - unfold per_symm_axiom, prod_per_data. pose (T := X ×h Y). pose (x := π₂ (π₁ (tm_var ((𝟙 ×h T) ×h T)))). pose (y := π₂ (tm_var ((𝟙 ×h T) ×h T))). unfold T in *. fold x y. use forall_intro. use forall_intro. use impl_intro. simplify_form. rewrite !partial_setoid_subst. use conj_intro. + use partial_setoid_sym. use weaken_right. use weaken_left. simplify_term. apply hyperdoctrine_hyp. + use partial_setoid_sym. use weaken_right. use weaken_right. simplify_term. apply hyperdoctrine_hyp. - unfold per_trans_axiom, prod_per_data. pose (T := X ×h Y). pose (x := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h T) ×h T) ×h T))))). pose (y := π₂ (π₁ (tm_var (((𝟙 ×h T) ×h T) ×h T)))). pose (z := π₂ (tm_var (((𝟙 ×h T) ×h T) ×h T))). unfold T in *. fold x y z. use forall_intro. use forall_intro. use forall_intro. use impl_intro. use impl_intro. simplify_form. rewrite !partial_setoid_subst. use conj_intro. + use (partial_setoid_trans (π₁ y)). * use weaken_left. use weaken_right. use weaken_left. simplify_term. apply hyperdoctrine_hyp. * use weaken_right. use weaken_left. simplify_term. apply hyperdoctrine_hyp. + use (partial_setoid_trans (π₂ y)). * use weaken_left. use weaken_right. use weaken_right. simplify_term. apply hyperdoctrine_hyp. * use weaken_right. use weaken_right. simplify_term. 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.