proposition: Proposition isPartialOrder_hProp : isPartialOrder (λ (P₁ P₂ : hProp), (P₁ ⇒ P₂)%logic).
proof: Proof. refine ((_ ,, _) ,, _). - exact (λ P₁ P₂ P₃ f g x, g(f x)). - exact (λ P x, x). - exact (λ P₁ P₂ f g, hPropUnivalence _ _ f g). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous