## Stream: maths

### Topic: A bunch of Lean files

#### Neil Strickland (Apr 14 2019 at 20:08):

I have put almost all of my Lean files at https://github.com/NeilStrickland/lean_lib/tree/master. There are about 19000 lines by the crudest metric, although I am sure that someone more skilful could achieve the same results with much less space. There is a README outlining what is there, and many files have substantial header comments. I would be interested in moving some of it to mathlib, although that will probably take a large amount of work with refactoring, complying with coding conventions and so on. I would be interested in comments and suggestions.

#### Kevin Buzzard (Apr 14 2019 at 20:58):

Which of the homotopy stuff do you think is appropriate for mathlib? Do you know about what Reid Barton has been doing with homotopy theory? (I don't but there's a repo somewhere)

#### Neil Strickland (Apr 14 2019 at 21:07):

The file itloc.lean is rather specialised, but poset.lean, subdiv.lean and upper.lean could certainly move into mathlib, possibly after some reorganisation. I don't think that anything I have done or am thinking of doing actually overlaps with what Reid has done, although it would be sensible to ensure that there is a smooth interface between them.

#### Kevin Buzzard (Apr 14 2019 at 21:42):

rw[mul_assoc (r0 ^ i) r0 s0,mul_assoc (r0 ^ i)] -- I think mathlib convention is a space between rw and [, and also space after the comma.

#### Scott Morrison (Apr 14 2019 at 22:57):

@Neil Strickland, you should definitely start PRing stuff, so that others can use it, it doesn't get lost, and it can all be polished up!

#### Scott Morrison (Apr 14 2019 at 22:59):

Regardling poset.lean: you should look at category_theory/concrete_category.lean, or some of the examples in the category_theory/instances/ directory, where you'll see an existing general framework for this kind of thing, which should save some repetition. By the time you're define comp, comp_id, id_comp, and assoc, you really should provide the category instance. (After which, as I keep telling Kevin, you get a lot of things for free :-)

#### Scott Morrison (Apr 14 2019 at 23:01):

There's tonnes of things in there that can be stand alone PRs. (e.g.) I think it's best to make "minimal" PRs, as big ones tend to get stuck in the throat of the reviewing process, unless they are done really well. :-)

#### Neil Strickland (Apr 15 2019 at 00:11):

Do you have examples yet of categories that are self-enriched? I really need to use the fact that poset.hom P Q has a poset structure such that composition and (co)evaluation are poset morphisms. I don't know if that will cause any problems with your general framework.

#### Scott Morrison (Apr 15 2019 at 02:10):

No, we haven't done (self-) enrichment yet. It really needs to happen.

#### Scott Morrison (Apr 15 2019 at 02:12):

I waited a long time on doing this because I wanted to do something overly general. :-) I've seen the error of my ways.

#### Scott Morrison (Apr 15 2019 at 02:13):

The long-standing issue of how to handle products in categories (are they just special cases of limits, or do you provide a separate API for them?) has also been a hold up on this.

Last updated: May 12 2021 at 08:14 UTC