chore(category_theory/functor): explain how to type 𝟭 (#3364)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jul 11, 2020 · f669a78 · f669a78
1 parent 574dac5
commit f669a78
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/docs/tutorial/category_theory/intro.lean b/docs/tutorial/category_theory/intro.lean
@@ -142,7 +142,7 @@ example : F.map (𝟙 X) = 𝟙 (F.obj X) := F.map_id X
 -- and preserves compositions
 example : F.map (f ≫ g) = (F.map f) ≫ (F.map g) := F.map_comp f g
 
--- The identity functor is `𝟭`, currently apparently untypesettable in Lean!
+-- The identity functor is `𝟭`, which you can write as `\sb1`.
 example : C ⥤ C := 𝟭 C
 
 -- The identity functor is (definitionally) the identity on objects and morphisms:

diff --git a/src/category_theory/functor.lean b/src/category_theory/functor.lean
@@ -53,7 +53,7 @@ protected def id : C ⥤ C :=
 { obj := λ X, X,
   map := λ _ _ f, f }
 
-notation `𝟭` := functor.id
+notation `𝟭` := functor.id -- Type this as `\sb1`
 
 instance : inhabited (C ⥤ C) := ⟨functor.id C⟩