Proposition eq_scott_open_set {D : dcpo} {P₁ P₂ : scott_open_set D} (H₁ : ∏ (x : D), P₁ x → P₂ x) (H₂ : ∏ (x : D), P₂ x → P₁ x) : P₁ = P₂. Proof. use subtypePath. { intro. apply propproperty. } use funextsec. intro x. use hPropUnivalence. - exact (H₁ x). - exact (H₂ x). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.