Zulip Chat Archive

Stream: maths

Topic: category theory tutorial maintenance


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Alena Gusakov (Jun 28 2020 at 18:35):

Cool, thank you!

view this post on Zulip 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.

view this post on Zulip Alena Gusakov (Jun 28 2020 at 19:46):

My github username is agusakov

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 19:48):

invite sent!

view this post on Zulip Alena Gusakov (Jun 28 2020 at 20:00):

Thanks!


Last updated: May 09 2021 at 11:09 UTC