Proposition bot_partial_setoid_morphism_eq {X : partial_setoid H} (f : partial_setoid_morphism bot_partial_setoid X) : f = bot_partial_setoid_morphism X. Proof. use eq_partial_setoid_morphism ; cbn. - refine (hyperdoctrine_cut (partial_setoid_mor_dom_defined f (π₁ (tm_var _)) (π₂ (tm_var _)) _) _). + cbn. rewrite <- hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. + exact (from_eq_in_bot_partial_setoid (hyperdoctrine_hyp _)). - 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.