> To avoid Russell's Paradox, there isn't a type of all types. Instead, we have universes.
This is an oversimplification, and Lean-specific (to be fair, the author claims to explore these concept in Lean). Girard's paradox comes from unrestricted impredicativity. To maintain consistency one needs to control impredicativity, type universes are a possible, very straightforward choice, but it is not the only choice.
Some theorem provers, such as Cedille, do not use type universes, and even have `Type : Type` while still being consistent. See Stump, Aaron: “The Calculus of Dependent Lambda Eliminations.” Journal of Functional Programming 27 (2017): e14. DOI:10.1017/S0956796817000053[0]
Additionally:
> The famous Curry-Howard correspondence states [...] Propositions are types in Prop [...]
Curry-Howard doesn't say anything about Prop, Prop vs. Type is just a distinction done in some particular type theories for pragmatic reasons, or because it simplifies classical (as opposed to intuitionistic) reasoning. In fact the reason why Prop vs. Type is a distinction done by many theorem provers leads Lawrence Paulson[1] to claim that modern theorem provers don't really use Curry-Howard[2], at least as Curry-Howard was originally defined. I disagree, because elements of Prop are still types, but please understand that this is a departure from original Curry-Howard.
Moreover:
> The famous Curry-Howard correspondence states [...] True propositions have exactly one term [...]
As explained above, this is not the case for the "original" Curry-Howard, and it is just a choice in Lean, which is a type theory with proof irrelevance. There are different type theories without proof irrelevance (such as Adga by default without a recent extension), and Curry-Howard certainly still applies to them. In fact even in Rocq (Coq), which still has Prop vs. Set, proof irrelevance has to be assumed explicitly[3]. (Rocq also has SProp[4] for proof irrelevant propositions.
nLab has more information about propositions as types[5] vs. propositions as some types[6].
This is really helpful. Minor nit under Curry-Howard correspondence: "True propositions have exactly one term" should be "have at least one term".
Great article, two minor nitpicks:
> To avoid Russell's Paradox, there isn't a type of all types. Instead, we have universes.
This is an oversimplification, and Lean-specific (to be fair, the author claims to explore these concept in Lean). Girard's paradox comes from unrestricted impredicativity. To maintain consistency one needs to control impredicativity, type universes are a possible, very straightforward choice, but it is not the only choice.
Some theorem provers, such as Cedille, do not use type universes, and even have `Type : Type` while still being consistent. See Stump, Aaron: “The Calculus of Dependent Lambda Eliminations.” Journal of Functional Programming 27 (2017): e14. DOI:10.1017/S0956796817000053[0]
Additionally:
> The famous Curry-Howard correspondence states [...] Propositions are types in Prop [...]
Curry-Howard doesn't say anything about Prop, Prop vs. Type is just a distinction done in some particular type theories for pragmatic reasons, or because it simplifies classical (as opposed to intuitionistic) reasoning. In fact the reason why Prop vs. Type is a distinction done by many theorem provers leads Lawrence Paulson[1] to claim that modern theorem provers don't really use Curry-Howard[2], at least as Curry-Howard was originally defined. I disagree, because elements of Prop are still types, but please understand that this is a departure from original Curry-Howard.
Moreover:
> The famous Curry-Howard correspondence states [...] True propositions have exactly one term [...]
As explained above, this is not the case for the "original" Curry-Howard, and it is just a choice in Lean, which is a type theory with proof irrelevance. There are different type theories without proof irrelevance (such as Adga by default without a recent extension), and Curry-Howard certainly still applies to them. In fact even in Rocq (Coq), which still has Prop vs. Set, proof irrelevance has to be assumed explicitly[3]. (Rocq also has SProp[4] for proof irrelevant propositions.
nLab has more information about propositions as types[5] vs. propositions as some types[6].
[0] https://doi.org/10.1017/S0956796817000053
[1] https://www.cl.cam.ac.uk/~lp15/
[2] https://lawrencecpaulson.github.io/2023/08/23/Propositions_a...
[3] https://github.com/rocq-prover/rocq/wiki/The-Logic-of-Coq#wh...
[4] https://rocq-prover.org/doc/V8.15.0/refman/addendum/sprop.ht...
[5] https://ncatlab.org/nlab/show/propositions+as+types
[6] https://ncatlab.org/nlab/show/propositions+as+some+types