Learning category theory

Stream: new members

[Mateusz Zugaj]

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]

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

[Johan Commelin]

And presheaves are there as well.

[Johan Commelin]

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]

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]

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

[Mateusz Zugaj]

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]

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]

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

[Johan Commelin]

Not yet, it's on our wish list.

[Mateusz Zugaj]

That's great! Really excited then.

[Johan Commelin]

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

[Johan Commelin]

But it doesn't use cool graphics yet.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

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]

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