You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Julius (Jul 16 2023 at 11:31):I may try to write statements in category theory in a formal programming language to enforce rigor on my mind. Is there a preferred, go to programming language I could easily use in a browser or install at the command line? I’m considering using Lean theorem prover. Would anyone care to give me a primer in writing some basic statements of category theory in Lean? (Will research it myself now). Thank you!
Josselin Poiret (Jul 16 2023 at 11:39):Julius said:
I may try to write statements in category theory in a formal programming language to enforce rigor on my mind. Is there a preferred, go to programming language I could easily use in a browser or install at the command line? I’m considering using Lean theorem prover. Would anyone care to give me a primer in writing some basic statements of category theory in Lean? (Will research it myself now). Thank you!
All of Coq, Agda and Lean have libraries containing category theory, sometimes multiple. It depends on what your preferred proof assistant is. I'm biased towards agda's cubical library since that's what I'm working on right now, but it might be a bit much learning about cubical just for this. agda-categories is pretty nice and might be the biggest category theory library around
Josselin Poiret (Jul 16 2023 at 11:40):however, if you want to get used to category theory from the ground up, you could just formalize everything yourself and not rely on a library as well!
Patrick Nicodemus (Jul 16 2023 at 16:41):@Julius There is a Lean mathematics library called mathlib which contains a category theory library. Here is the entry point. https://leanprover-community.github.io/mathlib_docs/category_theory/category/basic.html
I use Coq and have contributed to multiple category theory libraries within Coq.
https://coq.discourse.group/t/survey-of-category-theory-in-coq/371
The easiest way to install Coq is here: https://github.com/coq/platform.
Soon (within months) the math-comp library will start a category theory sublibrary. Math-comp is the most substantial centralized library of mathematics in Coq. This will be very good.
Agda would be a very good choice as well.
Isabelle/HOL has multiple category theory libraries, these can be found at the Archive of Formal Proofs. https://www.isa-afp.org/.
Isabelle/HOL is a simpler logic than Coq, Agda or Lean. The benefit of this is significantly superior automation. The cost is reduced expressiveness, so that trying to do category theory involves some convoluted boilerplate. However, basic Grothendieck-style scheme theory has been formalized in Isabelle/HOL, so it passes the basic stress tests of modern mathematics with large objects. https://www.isa-afp.org/search/?s=category%20theory
There is already a substantial formalization of category theory in (essentially) first order ZFC, taking place in an axiomatic V type. Not sure whether to regard this as an insane Herculean effort or a proof of practicality. https://www.isa-afp.org/entries/CZH_Foundations.html
Patrick Nicodemus (Jul 16 2023 at 16:53):I would like to draw attention to a recent paper on extensional dependent type theory, which has the expressiveness of intensional dependent type theory (Coq, Agda, Lean) without the drawbacks of having to worry about subtle aspects of equality in type theory (which spawned a small cottage industry called 'HoTT'). The rub is that typing judgements are undecidable, which is somewhat alarming as it can be interpreted as meaning "there is no algorithm to decide whether a proposed proof is actually a proof."
The authors give and implement an embedding of extensional dependent type theory into HOL to benefit from the powerful automation of this simpler logic.
https://arxiv.org/pdf/2305.15382.pdf
Patrick Nicodemus (Jul 16 2023 at 16:55):@Josselin Poiret I am curious about Agda and have not used it. I am familiar with Coq and the calculus of inductive constructions, can you say anything about what theorem proving looks like in Agda, what features it has on top of the basic type theory and so on?
Josselin Poiret (Jul 16 2023 at 16:59):Patrick Nicodemus said:
Josselin Poiret I am curious about Agda and have not used it. I am familiar with Coq and the calculus of inductive constructions, can you say anything about what theorem proving looks like in Agda, what features it has on top of the basic type theory and so on?
theorem proving in Agda is writing down terms in the underlying calculus explicitely, ie. what exact does in Coq. There is tactic support but it's seldom used. The upside is that writing down terms is very pleasant, much more than in Coq imo. You have a very good pattern-matching system similar to Haskell, whereas in Coq you need Equations to do something similar, and less readable than in Agda I might say. The interaction is centered around holes, where you leave out some terms to fill in later interactively, and that's how you iterate on proofs
Josselin Poiret (Jul 16 2023 at 16:59):i find Agda code to be much more readable than Coq code
Julius (Jul 16 2023 at 18:26):Thank you. I have set up lean, elan, and lake in VS Code (in GitPod), but cannot import category_theory, as it says the module is not found. Is it required to link to the GitHub repo for mathlib in the dependencies .toml file, for the lake init-created package? I would expect mathlib to be included by default? I can also ask on the Lean Zulip.
Julius (Jul 16 2023 at 18:27):I’ll try this:
“In your leanpkg.toml add:
[dependencies]
MathLib4 = {git = "https://github.com/leanprover-community/mathlib4", rev = "<fill_me_in>"}
“
Mike Shulman (Jul 16 2023 at 20:09):Josselin Poiret said:
i find Agda code to be much more readable than Coq code
Yes, Agda code is much more readable than Coq or Lean code. But Coq and Lean code is much more step-through-able than Agda code. Personally, I find I can understand a proof better by stepping through it than by just reading the code, so I prefer Coq and Lean when possible.
(I don't mean to start a flame war; I recognize that other perspectives are valid. I just wanted to make sure that both perspectives are represented when talking to a newcomer.)
Naso (Jul 17 2023 at 13:49):Patrick Nicodemus said:
Isabelle/HOL has multiple category theory libraries, these can be found at the Archive of Formal Proofs. https://www.isa-afp.org/.
Isabelle/HOL is a simpler logic than Coq, Agda or Lean. The benefit of this is significantly superior automation.
Another advantage of Isabelle besides the automation is the Isar structured-proof language, which lets you write proofs in a a way that's very close to ordinary maths. E.g. here is a proof of Cantor's theorem (from the manual)
lemma "¬ surj (f :: ′a ⇒ ′a set)"
proof
assume "surj f"
hence "∃a. {x. x ∉ f x} = f a" by(auto simp: surj_def)
thus "False" by blast
qed
(Note statements following by are usually completed by the automation.)
I had tried to learn Agda and Lean before but I found it quite laborious to write the tactic-style proofs, I think because I don't have a strong background in logic/type theory. But I started learning Isabelle a month ago and am already really productive with it thanks to the Isar language and automation stuff :smile: Or maybe Lean/Agda/Coq does have something like Isar that I'm unaware of?
Mike Shulman (Jul 17 2023 at 16:09):Lean has, or at least had, a syntax for terms that looked a bit like that. They may have dropped it. But to be honest that proof doesn't look much different from a tactic proof to me. Just substitute "intros" for "assume", "have" for "hence", and remove "thus False by", and it looks like a tactic proof to me.
Mike Shulman (Jul 17 2023 at 16:11):Tactics also allow you to reason "backwards", which is sometimes hard to get used to, although I found that once I got used to it it actually matched the way I think about math in my head better than a traditional "forwards" proof. But you can also reason forwards with tactics just as well.
Mike Shulman (Jul 17 2023 at 16:12):Also the automation of modern Lean is fairly impressive. I haven't used Isabelle/HOL myself (not for anything like this, anyway), but is its automation really still significantly superior? In principle, I don't see any reason that a dependently-typed proof assistant couldn't have equally good automation when restricted to its "HOL" fragment.
Naso (Jul 17 2023 at 23:38):Mike Shulman said:
Also the automation of modern Lean is fairly impressive. I haven't used Isabelle/HOL myself (not for anything like this, anyway), but is its automation really still significantly superior? In principle, I don't see any reason that a dependently-typed proof assistant couldn't have equally good automation when restricted to its "HOL" fragment.
By 'modern Lean' do you mean Lean 4? One other reason I've avoided Lean for now is it's going through a major transition from 3 to 4 where AFAIK code written in 4 is largely incompatible with 3 and vice versa. I looked at Lean 4 early last year but found the documentation quite lacking- e.g. the entries on the built-in types were mostly empty. I've just checked again and they're still empty!
Since I need to actually get stuff down now, not having reliable documentation is a big deal, and also it means what is possible in principle is not really relevant to me!
I haven't used the automation features of Lean so I can't compare on that.
I am definitely looking forward to trying Lean again once it's had its version 4 release and better documentation. :smile:
Mike Shulman (Jul 18 2023 at 01:10):Yes, right now is a bit of a rough time to try to pick up Lean as a beginner, with Lean 3 being phased out and the infrastructure of Lean 4 not fully in place to replace it yet. Personally, I have't used Lean 4 yet, but my experience was that the automation in Lean 3 was already fairly impressive (compared to, say, Agda, at least).
Anand Rao (Jul 19 2023 at 07:28):Lean's mathematics library has in fact now been ported to Lean4 entirely (only a few days ago!): https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/375639225.