Proposition bot_partial_setoid_morphism_laws (X : partial_setoid H) : @partial_setoid_morphism_laws H bot_partial_setoid X ⊥. Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law. cbn. simplify. do 2 use forall_intro. use impl_intro. use weaken_right. use false_elim. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law. cbn. simplify. do 2 use forall_intro. use impl_intro. use weaken_right. use false_elim. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_eq_defined_law. cbn. simplify. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law. cbn. simplify. do 3 use forall_intro. use impl_intro. use weaken_right. use false_elim. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law. cbn. simplify. use forall_intro. use impl_intro. use weaken_right. unfold partial_setoid_formula ; cbn. simplify. use false_elim. 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.