What are the proper imports used in this Category theory vid

Stream: lean4

[Daniel Donnelly]

https://youtu.be/1NUc-ZNC_2s?si=_aJI_qNVHjoFlLXs&t=65

Thanks. Need it for Lean4 :sweat_smile:

[Dev Joshi]

I'm working with Dan and I also want to know how this works, what a coincidence!

[Mario Carneiro]

The file is https://github.com/leanprover-community/lftcm2020/blob/master/src/demos/category_theory.lean and it seems to still be working (on lean 3) as of Jan 2023 so it should be relatively simple to run it through mathport

[Mario Carneiro]

I don't think anyone has tried to mathport this repo

[Daniel Donnelly]

Mario Carneiro said:

The file is https://github.com/leanprover-community/lftcm2020/blob/master/src/demos/category_theory.lean and it seems to still be working (on lean 3) as of Jan 2023 so it should be relatively simple to run it through mathport

Thanks! Would this be feasible for two Lean4 novices to accomplish?

One who knows the basics of category theory, and both know how to program in other languages.

[Mario Carneiro]

hm, apparently it hasn't been checked recently, category_theory.functor no longer exists, nor algebra.category.Module.monoidal or topology.category.Top

[Mario Carneiro]

https://github.com/leanprover-community/mathport/ has instructions on how you can use it to port lean 3 files

[Mario Carneiro]

but it has a prerequisite that the files have to work on the latest lean 3

[Daniel Donnelly]

Mario Carneiro said:

hm, apparently it hasn't been checked recently, category_theory.functor no longer exists, nor algebra.category.Module.monoidal or topology.category.Top

You mean these are missing in Lean3 side?

[Mario Carneiro]

they've been renamed or split on the lean 3 side

[Daniel Donnelly]

Mario Carneiro said:

they've been renamed or split on the lean 3 side

Thanks for your expertise! We will look at mathport docs now.

[Mario Carneiro]

replacing those with category_theory.functor.basic, algebra.category.Module.monoidal.basic and topology.category.Top.limits.basic respectively seems to produce a working file

[Daniel Donnelly]

@Mario Carneiro
https://github.com/leanprover-community/mathlib4/blob/56102518894110f4b30d5d61e3711a9f2c677574/Mathlib/CategoryTheory/Functor/Category.lean#L85

Found these. I think you're right. We will try translating the examples in the video into the existing Mathlib4 Category calls

[Mario Carneiro]

Since I happen to have a prepared mathport install already, I've run make oneshot on that file: CategoryTheory.lean

[Eric Wieser]

Have you considered watching the LftCM 2023 video instead?

[Eric Wieser]

That uses lean 4

[Eric Wieser]

Perhaps this is evidence that the LftCM 2023 videos need to live on youtube and not just the LftCM 2023 website

[Daniel Donnelly]

Eric Wieser said:

Perhaps this is evidence that the LftCM 2023 videos need to live on youtube and not just the LftCM 2023 website

@Eric Wieser I found this page:
https://lftcm2023.github.io/tutorial/

But I can't access the vids

[Eric Wieser]

Why can't you access them?

[Daniel Donnelly]

@Eric Wieser nvm, I reread yes there's a password given there

[Eric Wieser]

@Marcus Zibrowius, I assume there's no way to remove the password requirements

[Scott Morrison]

Can we just upload them to the leanprover community youtube channel? Ideally all videos would go there.

[Scott Morrison]

I can do the upload if you make it trivial for me (e.g. a zip file of the videos, and a list of the titles you want).

[Marcus Zibrowius]

@Daniel Donnelly The password is printed on the page, after every single video link. Here again is the link:
https://lftcm2023.github.io/tutorial/index.html
And this is the password for all videos: LftCM2023

[Marcus Zibrowius]

@Eric Wieser Your assumption is correct. I would have removed the password if I could. I've also asked our IT support for a workaround, but they didn't have one. For the record: This is CISCO technology.

[Marcus Zibrowius]

@Eric Wieser @Scott Morrison Currently, downloading is blocked. I cannot download myself without allowing downloads from the internet. I could enable public downloads temporarily and bulk download to my own computer, but I have no idea how long this might take and whether I even have sufficient disc space. And if that succeeds, I'm not sure how to share it. We're talking about 20 hours of video recordings here. If you think it's doable and worth the effort, I can contact the tutors and ask whether they'd be happy with this.

[Scott Morrison]

Youtube is perfectly happy with 20 hours.

[Scott Morrison]

I can do the download too if you make it easy for me (e.g. a list of URLs to get)

[Ruben Van de Velde]

What's the issue with enabling public downloads?

[Marcus Zibrowius]

@Scott Morrison I'll prepare either a list of url's or a zip file of the recordings in the next couple of days, and get back to you.