## Stream: general

### Topic: Category of U-Sets listed?

#### 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?

#### Mario Carneiro (Aug 29 2019 at 00:25):

what notation? Most categories are just notated using their names

#### Mario Carneiro (Aug 29 2019 at 00:25):

i.e. Top

#### 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?

#### Scott Morrison (Aug 29 2019 at 00:31):

I don't understand.

#### Scott Morrison (Aug 29 2019 at 00:31):

What notation are you expecting?

#### Daniel Donnelly (Aug 29 2019 at 00:31):

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

#### Scott Morrison (Aug 29 2019 at 00:31):

Top is in src/topology/Top/.

#### Scott Morrison (Aug 29 2019 at 00:31):

So import category_theory.all won't find it.

I c

#### 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.

#### 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.

#### Simon Hudon (Aug 29 2019 at 00:58):

don't you use cache-olean?

#### 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?

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