category theory tutorial maintenance

Stream: maths

[Alena Gusakov]

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]

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]

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

[Alena Gusakov]

Cool, thank you!

[Johan Commelin]

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.

[Alena Gusakov]

My github username is agusakov

[Bryan Gin-ge Chen]

invite sent!

[Alena Gusakov]

Thanks!