Category of U-Sets listed?

Stream: general

[Daniel Donnelly]

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?

[Mario Carneiro]

what notation? Most categories are just notated using their names

[Mario Carneiro]

i.e. Top

[Daniel Donnelly]

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

how would I get notation for it?

[Scott Morrison]

I don't understand.

[Scott Morrison]

What notation are you expecting?

[Daniel Donnelly]

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

[Scott Morrison]

Top is in src/topology/Top/.

[Scott Morrison]

So import category_theory.all won't find it.

[Daniel Donnelly]

I c

[Daniel Donnelly]

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.

[Scott Morrison]

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

[Simon Hudon]

don't you use cache-olean?

[Daniel Donnelly]

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

[Kevin Buzzard]

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.