Zulip Chat Archive

Stream: general

Topic: category theory directories


view this post on Zulip 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/?

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 22 2018 at 22:27):

And, I also use your -pr library.

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip 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. :-)

view this post on Zulip 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.

view this post on Zulip 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