fact: Definition isaposetmorphism_hProp {P Q : Poset} (f : P -> Q) : hProp := ∀ x x' : P, x ≤ x' ⇒ f x ≤ f x'.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo