a PR for category theory

Stream: general

[Scott Morrison]

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.

Options:
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]

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]

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

[Johannes Hölzl]

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]

@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]

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]

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]

@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]

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]

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

[Johan Commelin]

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