diff --git a/theories/base.v b/theories/base.v
index 4284a89627f3f8c4e0ca1841a21deee2944286e4..51dcdad2f233e0fa907ac48a321b8dd648e4044d 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -726,6 +726,8 @@ End disjoint_list.
 
 Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
 
+Class UpClose A B := up_close : A → B.
+Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
 (** We define operational type classes for the monadic operations bind, join