Proposition bot_partial_setoid_axioms : @per_axioms H 𝟙 ⊥. Proof. split. - unfold per_symm_axiom. simplify. use forall_intro. use forall_intro. use impl_intro. use weaken_right. apply hyperdoctrine_hyp. - unfold per_trans_axiom. simplify. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use weaken_right. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.StrictInitial. 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.