# Zulip Chat Archive

## 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-pr`

library 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: Dec 20 2023 at 11:08 UTC