## Stream: maths

### Topic: category theory tutorial maintenance

#### Alena Gusakov (Jun 28 2020 at 18:31):

I've been using the tutorial in docs/tutorial/category_theory as a jumping-off point for doing category theory stuff in Lean, but its syntax for declaring categories is a bit outdated. I'd like to replace lines like this

variables (C : Type u) [𝒞 : category.{v} C]
include 𝒞


in the intro file with the updated syntax

variables (C : Type u) [category.{v} C]


Would it be possible for me to get write access to a branch in the mathlib repository? Hope this is the right channel to ask about it

#### Jalex Stark (Jun 28 2020 at 18:33):

this is approximately the best place to ask (I think any of the mathlib maintainers can grant this, and they mostly pay attention to this stream)

#### Jalex Stark (Jun 28 2020 at 18:34):

This has some details about the process of contributing to mathlib
https://leanprover-community.github.io/contribute/index.html
the review standards are lower for things outside of src/ but the process is the same

Cool, thank you!

#### Johan Commelin (Jun 28 2020 at 19:15):

Alena Gusakov said:

Would it be possible for me to get write access to a branch in the mathlib repository? Hope this is the right channel to ask about it

Sure! And thanks for helping! We'll need your github username in order to give you the access.