feat(category_theory/shapes): basic shapes of cones and conversions

[semorrison]

Some helper methods for building and decomposing cones of various standard shapes.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[semorrison]

I've just rebased this.

[jcommelin]

I think this looks fine. But I don't have as clear a vision of what the end result of the implementation of the limits library should look like as others might have. I would say, let's get this merged and see how it works. We don't have too many users, so we can still refactor after we have more experience.

[semorrison]

What do you think, @rwbarton?

[rwbarton]

I haven't had a chance to look at this in depth. I'm okay with the plan of merging something along these lines with the idea that it may change substantially in the future.

I'm especially unsure that in the long run we really want two different notions square and cosquare.

I think we should also take a look at prior art in other category theory libraries, for example the Lean 2 category theory library (e.g. 1, 2).

[jcommelin]

@fpvandoorn Can you comment on your experience developing the category lib in Lean2?

[fpvandoorn]

I'm not sure what kind of things you want to know. I remember that it was a lot of work with 1-2 people to build a category library (it was mostly me and Jakob von Raumer, @javra), especially since we didn't have a clear goal in sight. Therefore the library has many rough edges and is very incomplete. It was fun to build parts of a category theory library, though, especially since some things in category theory work quite differently in HoTT.

I like how the category theory library in Lean 3 does more with automation. There were quite some diagram chases which we had to write out explicitly, which are done by a single tactic in Lean 3. There are various other differences, for example we used bundled categories ((C : Category) instead of (C : Type) [category C]), but I think that is a minor difference in practice.

About limits, I remember one trick which was neat, namely what we called a "sparse category". It's a special case of the free category, where you cannot compose any of the given morphisms. So basically it just adds identity morphisms. Instances include many of the "walking structures": like the shape of pullbacks, pushouts and (co)equalizers.

If you have more specific questions, I'm happy to answer them.

[javra]

I remember that some tricks we used are also mentioned in this paper by Gross, Chlipala, and Spivak. Especially making the the category definition symmetric (section 3.1 of the paper) was quite helpful.

[fpvandoorn]

Oh yes, that was useful to make (Cᵒᵖ)ᵒᵖ definitionally equal to C up to eta for records. So if C was of the form category.mk _ _ ... _ then (Cᵒᵖ)ᵒᵖ ≡ C. I think these tricks are unnecessary if you have definitional proof irrelevance, though.

[jcommelin]

But we don't have eta for records...

[javra]

Not having eta for records prevents the trick from working in all cases, but it still does whenever the the category is an application of the constructor, which happens from time to time when you write the library.

I guess, as @fpvandoorn said, the benefits are much smaller than in HoTT, but it might still result in cleaner terms.

[semorrison]

I'm not sure of the consequence of formalabstracts incorporating this into their codebase. I'm still hopeful that we can merge this. I would like to be able to add more stuff to the category theory library, but I'm mostly stalled on this decision.

[fpvandoorn]

Once this PR is merged here we will remove it from our repository.

[semorrison]

Just rebased onto master; travis had been getting sad.

[semorrison]

Err... this PR seems to be stranded off on some strange repository leanprover-fork/mathlib-backup. I'm going to close and reopen a new one.