Definition make_partial_setoid {H : first_order_hyperdoctrine} (X : ty H) (e : per X) : partial_setoid H := X ,, e. Coercion partial_setoid_to_type {H : first_order_hyperdoctrine} (X : partial_setoid H) : ty H. Proof. exact (pr1 X). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.