Zulip Chat Archive

Stream: general

Topic: a PR for category theory

Scott Morrison (Jun 04 2018 at 02:04):

Dear all, (@Mario Carneiro and @Johannes Hölzl in particular!)
I'm finally about to create a mathlib branch for some category theory, and I would be happy to have some guidance about the scope of the initial PR.

1. Just the definitions of category, functor, natural transformation, and compositions of these.
2. Also some basic constructions, e.g. functor categories, and product categories.
3. Also definitions of basic notions such as products, equalizers, and limits.
4. Also an example, e.g. showing that the category of types has limits.

(I could add many more things, but I think that's probably more than enough for a single PR.)

Essentially it's a question about whether it's easier to have things in very small increments, or easier to have bigger blocks, so that design decisions can be validated by examples and applications.

Mario Carneiro (Jun 04 2018 at 07:23):

Hey, just a heads up, but I am currently traveling and will soon be busy with the lean summer school in Hanoi for the next couple weeks, so my activity here will probably be spotty.

Scott Morrison (Jun 04 2018 at 08:40):

No worries! And thanks for letting us know. Will there be materials from the summer school available online?

Johannes Hölzl (Jun 04 2018 at 09:11):

Hi Scott, I think it would be good to start with a PR for 1. definitions. Then its easier to comment on it. For the summer school: https://hanoifabs.wordpress.com/ will be very ad-hoc, e.g. there are not a lot of slides.

Johan Commelin (Jun 04 2018 at 09:14):

@Johannes Hölzl And you are also flying there, right? So the next two weeks are bad timing for PR's in general?

Johannes Hölzl (Jun 04 2018 at 09:16):

Yes, I just landed in Hanoi. I guess the next 3 weeks are quiet busy. First Formal Abstract Summer School in Hanoi and then Hales60 in Pittsburgh.

Scott Morrison (Jun 04 2018 at 09:21):

Thanks, @Johannes Hölzl . The PR I put up at https://github.com/leanprover/mathlib/pull/152 is just the first few definitions.

Sebastian Ullrich (Jun 08 2018 at 08:51):

@Mario Carneiro @Johannes Hölzl What _is_ happening over in Hanoi/in the fabstracts repo :laughing: ? https://github.com/formalabstracts/formalabstracts/pulls

Johannes Hölzl (Jun 08 2018 at 08:52):

Well, we try to teach people to use github, but some used the wrong formalabstracts fork. They should use Tom's personal formalabstract repo, not the project ones...

Johannes Hölzl (Jun 08 2018 at 08:53):

Teaching git (as setting up remotes) is harder than thought...

Johan Commelin (Jul 09 2018 at 14:05):

What is the status of this PR? I would love to have basic category theory available in mathlib!

Last updated: Aug 03 2023 at 10:10 UTC