diff --git a/theories/base.v b/theories/base.v
index 4452a6960cd3189ed0a9b6b0ab19e843fa486476..08e1f021e691a9de807fdaf759a3ac31d8958ecc 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -209,6 +209,9 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 Class Empty A := empty: A.
 Notation "∅" := empty : C_scope.
 
+Class Top A := top : A.
+Notation "⊤" := top : C_scope.
+
 Class Union A := union: A → A → A.
 Instance: Params (@union) 2.
 Infix "∪" := union (at level 50, left associativity) : C_scope.
@@ -311,7 +314,7 @@ Instance: Params (@disjoint) 2.
 Infix "⊥" := disjoint (at level 70) : C_scope.
 Notation "(⊥)" := disjoint (only parsing) : C_scope.
 Notation "( X ⊥.)" := (disjoint X) (only parsing) : C_scope.
-Notation "(.⊥ X )" := (λ Y, Y ⊥  X) (only parsing) : C_scope.
+Notation "(.⊥ X )" := (λ Y, Y ⊥ X) (only parsing) : C_scope.
 Infix "⊥*" := (Forall2 (⊥)) (at level 70) : C_scope.
 Notation "(⊥*)" := (Forall2 (⊥)) (only parsing) : C_scope.
 Infix "⊥**" := (Forall2 (⊥*)) (at level 70) : C_scope.
diff --git a/theories/bsets.v b/theories/bsets.v
index 8ae132f1f432046baa268c02ab2a64609d4b0a72..2b486081ab18a1f5b14a155e768833ca5a8dc6d1 100644
--- a/theories/bsets.v
+++ b/theories/bsets.v
@@ -6,7 +6,7 @@ From stdpp Require Export prelude.
 Record bset (A : Type) : Type := mkBSet { bset_car : A → bool }.
 Arguments mkBSet {_} _.
 Arguments bset_car {_} _ _.
-Definition bset_all {A} : bset A := mkBSet (λ _, true).
+Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
 Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
 Instance bset_singleton {A} `{∀ x y : A, Decision (x = y)} :
   Singleton A (bset A) := λ x, mkBSet (λ y, bool_decide (y = x)).
diff --git a/theories/co_pset.v b/theories/co_pset.v
index 85e80a4665b84b99ee4bfde4ab3bd6a1ac2af3d3..16692659c6134950bda693dd9bb3ab689508591d 100644
--- a/theories/co_pset.v
+++ b/theories/co_pset.v
@@ -148,7 +148,7 @@ Instance coPset_singleton : Singleton positive coPset := λ p,
   coPset_singleton_raw p ↾ coPset_singleton_wf _.
 Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
 Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
-Definition coPset_all : coPset := coPLeaf true ↾ I.
+Instance coPset_top : Top coPset := coPLeaf true ↾ I.
 Instance coPset_union : Union coPset := λ X Y,
   let (t1,Ht1) := X in let (t2,Ht2) := Y in
   (t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
diff --git a/theories/sets.v b/theories/sets.v
index bb9c9ddd102c9267d4e632927f6a1bf63eb0aa69..a6740fab42381292fa4ade49b80143bc5d7080a3 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -6,7 +6,7 @@ From stdpp Require Export prelude.
 Record set (A : Type) : Type := mkSet { set_car : A → Prop }.
 Arguments mkSet {_} _.
 Arguments set_car {_} _ _.
-Definition set_all {A} : set A := mkSet (λ _, True).
+Instance set_all {A} : Top (set A) := mkSet (λ _, True).
 Instance set_empty {A} : Empty (set A) := mkSet (λ _, False).
 Instance set_singleton {A} : Singleton A (set A) := λ x, mkSet (x =).
 Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.