category theory directories

Stream: general

[Reid Barton]

@Scott Morrison, would you accept PRs to lean-category-theory and lean-category-theory-pr which move everything from categories/ to category_theory/?

[Reid Barton]

I'm trying to update my project to use the new mathlib with categories, and I'd rather only go through the Great Renaming of modules once

[Reid Barton]

And, I also use your -pr library.

[Reid Barton]

Actually, I may just add some "forwarding" modules to my project for now, since I think I only use a few modules from -pr at this point.

[Scott Morrison]

Okay, the lean-category-theory-prlibrary has finally been laid to rest, and there's just mathlib and lean-category-theory. Sorry about that. :-)

[Scott Morrison]

In related news, lean-category-theory now contains my updated version of limits (not all the colimit stuff is filled in yet, hoping someone wants to write me a nice tactic. :-)

[Scott Morrison]

It's missing some things that used to be in lean-category-theory, in particular constructing limits from products and equalizers, and showing that if D has limits, the functor category C \lea D has limits too. Hopefully these should be easier to reimplement with the new design, anyway.

[Reid Barton]

It turned out .isomorphisms was the only module I was using, so it was easy to work around.