Proposition isaset_partial_setoid_morphism : isaset partial_setoid_morphism. Proof. use isaset_total2. - apply isaset_hyperdoctrine_formula. - intro. apply isasetaprop. apply isaprop_partial_setoid_morphism_laws. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs.