Proposition parital_setoid_morphism_to_terminal_eq {H : first_order_hyperdoctrine} {X : partial_setoid H} (φ : partial_setoid_morphism X (eq_partial_setoid 𝟙)) : φ = partial_setoid_morphism_to_terminal X. Proof. pose (x := π₁ (tm_var (X ×h 𝟙))). pose (y := π₂ (tm_var (X ×h 𝟙))). use eq_partial_setoid_morphism ; cbn ; fold x. - use (partial_setoid_mor_dom_defined φ x y). unfold x, y. rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. - use (exists_elim (partial_setoid_mor_hom_exists φ (hyperdoctrine_hyp _))). cbn. use weaken_right. unfold x, y ; clear x y. simplify. pose (x := π₁ (tm_var ((X ×h 𝟙) ×h 𝟙))). pose (y := π₂ (tm_var ((X ×h 𝟙) ×h 𝟙))). fold x y. assert (y = π₂ x) as p. { use hyperdoctrine_unit_eq. } rewrite p. rewrite <- (hyperdoctrine_pair_eta x). apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation. 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.