diff --git a/theories/base.v b/theories/base.v
index 49cc37e9120c63cd2e3157337c17d81da835ec0b..886543243b65101fd634494e27fdd800dbbfa33a 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -684,6 +684,9 @@ Class FreshSpec A C `{ElemOf A C}
 }.
 
 (** * Miscellaneous *)
+Class Half A := half: A → A.
+Notation "x .½" := (half x) (at level 20, format "x .½") : C_scope.
+
 Lemma proj1_sig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) :
   x↾Px = y↾Py → x = y.
 Proof. injection 1; trivial. Qed.