unknown identifier 'category_theory.category.comp'

Stream: general

[ZHAO Jinxiang]

https://leanprover-community.github.io/theories/category_theory.html

import category_theory.types
import category_theory.category.basic

namespace playground

local notation f ` ⊚ `:80 g:80 := category_theory.category.comp g f

example : (ℕ ⟶ ℕ) := id ≫ nat.succ
example : (ℕ ⟶ ℕ) := category_theory.category_struct.comp id nat.succ
example : (ℕ ⟶ ℕ) := nat.succ ⊚ id
end playground

image.png
Why this doesn't work?

[Junyan Xu]

I think it's called docs#category_theory.category_struct.comp ?

[Junyan Xu]

The page https://leanprover-community.github.io/theories/category_theory.html may be slightly outdated

[ZHAO Jinxiang]

Thanks!