## Stream: general

### Topic: category theory directories

#### Reid Barton (Aug 22 2018 at 22:25):

@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 (Aug 22 2018 at 22:27):

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 (Aug 22 2018 at 22:27):

And, I also use your -pr library.

#### Reid Barton (Aug 23 2018 at 00:11):

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 (Aug 25 2018 at 15:03):

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 (Aug 25 2018 at 15:03):

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 (Aug 25 2018 at 15:04):

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 (Aug 25 2018 at 15:06):

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

Last updated: May 15 2021 at 00:39 UTC