Zulip Chat Archive

Stream: new members

Topic: Learning category theory


Mateusz Zugaj (Jun 01 2020 at 17:34):

Hello, I am new here,
I was looking for a theorem prover which is nice to use to prove category theory lemmas. I want to formalize basic proofs like "limit of presheafs are computed pointwise" or "Cat is cartesian closed", because I feel that I miss some details there. Is Lean a good place for this?

Johan Commelin (Jun 01 2020 at 17:40):

Hi, welcome!
We just got this "Cat is cartesian closed" yesterday (-;

Johan Commelin (Jun 01 2020 at 17:40):

And presheaves are there as well.

Johan Commelin (Jun 01 2020 at 17:41):

Otoh, if you want to do category theory, and only category theory, then you might also want to look at Coq (and/or HoTT) libraries

Mateusz Zugaj (Jun 01 2020 at 17:48):

Oh, so there is much for me to explore. :) Thank you.
What are differences between Lean and Coq when it comes to category theory? I proved some first order logic stuff on both Coq and Lean and they look almost identically...

Johan Commelin (Jun 01 2020 at 17:48):

I think that their library is just bigger (although to be honest, I never looked at it in detail).

Mateusz Zugaj (Jun 01 2020 at 17:50):

The size of the library is not an issue for me I think, because I just want to scratch some stuff myself for now.

Johan Commelin (Jun 01 2020 at 17:50):

In that case it shouldn't matter too much. If you care about unicode notation, that's a plus for lean. If you care about constructive logic, use coq.

Mateusz Zugaj (Jun 01 2020 at 17:51):

Btw, is there a tool to convert graphical categoric diagrams (thinking like https://tikzcd.yichuanshen.de/) to formal format?

Johan Commelin (Jun 01 2020 at 17:51):

Not yet, it's on our wish list.

Mateusz Zugaj (Jun 01 2020 at 17:51):

That's great! Really excited then.

Johan Commelin (Jun 01 2020 at 17:51):

We are about to get a diagram chasing automated prover though...

Johan Commelin (Jun 01 2020 at 17:51):

But it doesn't use cool graphics yet.

Johan Commelin (Jun 01 2020 at 17:52):

Otoh, we also just got a "widget" framework. So we should be able to build fancy UI frontends soonish as well.

Johan Commelin (Jun 01 2020 at 17:52):

If you care about that sort of stuff, my impression is that lean is ahead of coq

Johan Commelin (Jun 01 2020 at 17:52):

But again, I haven't looked at their side of the fence very closely.

Kevin Buzzard (Jun 01 2020 at 18:06):

There are two Lean category theory questions in codewars. I still haven't done either of them :-/ I think that we need more documentation on how to steer this stuff

Bhavik Mehta (Jun 01 2020 at 18:20):

Johan Commelin said:

Hi, welcome!
We just got this "Cat is cartesian closed" yesterday (-;

We don't have that Cat is cartesian closed! I defined cartesian closed categories, didn't show that Cat itself is cartesian closed :) I agree that doing category theory (from scratch) in Lean or Coq doesn't make a huge difference - though I've heard from others who have done more category theory in Coq than I have that proof relevance gets annoying for more complex things. I've actually just done limits of presheaves are computed pointwise myself today, it was easier than I expected! (there's a version in mathlib already though)

Mateusz Zugaj (Jun 01 2020 at 18:26):

That's neat! Can't wait to go through it. But first, I need to learn the basics

Johan Commelin (Jun 01 2020 at 19:05):

Bhavik Mehta said:

Johan Commelin said:

Hi, welcome!
We just got this "Cat is cartesian closed" yesterday (-;

We don't have that Cat is cartesian closed!

Oops... sorry for overselling your PR

Bhavik Mehta (Jun 01 2020 at 19:12):

No worries, saves something for @Mateusz Zugaj to do :)


Last updated: Dec 20 2023 at 11:08 UTC