docs(category_theory): mention notation for identity homs (#16410)

leanprover-community · Sep 13, 2022 · ed9be88 · ed9be88
1 parent d268bb7
commit ed9be88
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/category_theory/category/basic.lean b/src/category_theory/category/basic.lean
@@ -14,8 +14,9 @@ Defines a category, as a type class parametrised by the type of objects.
 ## Notations
 
 Introduces notations
-* `X ⟶ Y` for the morphism spaces,
-* `f ≫ g` for composition in the 'arrows' convention.
+* `X ⟶ Y` for the morphism spaces (type as `\hom`),
+* `𝟙 X` for the identity morphism on `X` (type as `\b1`),
+* `f ≫ g` for composition in the 'arrows' convention (type as `\gg`).
 
 Users may like to add `f ⊚ g` for composition in the standard convention, using
 ```lean