doc: Make the docs more uniform for the Category and Quiver modules (#…

…8928) Fix the description of the definition of `Quiver` and change the example of the use of `⊚` to be consistent with the above use of `≫`.
leanprover-community · Dec 13, 2023 · 91ebbbe · 91ebbbe
1 parent 39229b7
commit 91ebbbe
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -22,9 +22,9 @@ Introduces notations in the `CategoryTheory` scope
 * `𝟙 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
+Users may like to add `g ⊚ f` for composition in the standard convention, using
 ```lean
-local notation f ` ⊚ `:80 g:80 := category.comp g f    -- type as \oo
+local notation g ` ⊚ `:80 f:80 := category.comp f g    -- type as \oo
 ```
 
 ## Porting note

diff --git a/Mathlib/Combinatorics/Quiver/Basic.lean b/Mathlib/Combinatorics/Quiver/Basic.lean
@@ -17,7 +17,7 @@ is a very permissive notion of directed graph.
 
 ## Implementation notes
 
-Currently `Quiver` is defined with `arrow : V → V → Sort v`.
+Currently `Quiver` is defined with `Hom : V → V → Sort v`.
 This is different from the category theory setup,
 where we insist that morphisms live in some `Type`.
 There's some balance here: it's nice to allow `Prop` to ensure there are no multiple arrows,