diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index 5358d8dc17e5d358306be9f3e9cd1b96665c16c1..baed9dd5b55e5481c7c7ef70bc322a0a14a393f2 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -2,6 +2,10 @@ From iris.algebra Require Export auth excl updates.
 From iris.algebra Require Import local_updates.
 From iris.base_logic Require Import base_logic.
 
+(** Authoritative CMRA where the fragment is exclusively owned.
+This is effectively a single "ghost variable" with two views, the frament [â—¯E a]
+and the authority [●E a]. *)
+
 Definition excl_authR (A : ofeT) : cmraT :=
   authR (optionUR (exclR A)).
 Definition excl_authUR (A : ofeT) : ucmraT :=