Definition isaposetmorphism_hProp {P Q : Poset} (f : P -> Q) : hProp := ∀ x x' : P, x ≤ x' ⇒ f x ≤ f x'.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.