Zulip Chat Archive

Stream: general

Topic: Category of U-Sets listed?


view this post on Zulip Daniel Donnelly (Aug 29 2019 at 00:24):

I've tried:

import category_theory.all
open category_theory
#print instances category

But of course get a long list I don't understand. Also how would I print the standard notation for each in the above list?

view this post on Zulip Mario Carneiro (Aug 29 2019 at 00:25):

what notation? Most categories are just notated using their names

view this post on Zulip Mario Carneiro (Aug 29 2019 at 00:25):

i.e. Top

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 00:30):

category_theory.ulift_category : Π (C : Type u) [_inst_1 : category C], category (ulift C)

how would I get notation for it?

view this post on Zulip Scott Morrison (Aug 29 2019 at 00:31):

I don't understand.

view this post on Zulip Scott Morrison (Aug 29 2019 at 00:31):

What notation are you expecting?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 00:31):

@Mario Carneiro the above code does not list even Top.

view this post on Zulip Scott Morrison (Aug 29 2019 at 00:31):

Top is in src/topology/Top/.

view this post on Zulip Scott Morrison (Aug 29 2019 at 00:31):

So import category_theory.all won't find it.

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 00:31):

I c

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 00:34):

Any reason I have to keep restarting VSCode when I mess with the import command and also it always says "Updating" in upper right. I did follow directions.

view this post on Zulip Scott Morrison (Aug 29 2019 at 00:35):

Run leanpkg build on the command line first. Almost certainly this is a symptom of not having a fully compiled copy of mathlib.

view this post on Zulip Simon Hudon (Aug 29 2019 at 00:58):

don't you use cache-olean?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 02:06):

@Simon Hudon I'm not sure how to enable that, is cache-olean in setttings of vscode?

view this post on Zulip Kevin Buzzard (Aug 29 2019 at 07:52):

cache-olean and update-mathlib are shell commands written by the community to help with compiling mathlib. See the installation instructions here https://github.com/leanprover-community/mathlib . "Updating" is normal though -- the clue that mathlib isn't installed is a lot of orange bars indicating that things are compiling. "Updating" just means "waiting for the next thing to happen" as far as I can see.


Last updated: May 15 2021 at 00:39 UTC