New answers tagged type-theory
8
votes
How exactly are realizability and the Curry-Howard correspondence related?
I am sure more than one exact correspondence can be made, but here's at least one that is technically precise. We shall employ categorical logic.
Executive summary: realizability is the ...
- 46.7k
2
votes
Does substitution on named terms correspond to substitution on de Bruijn terms?
See the 2021-present work of Joshua Grosso, who formalised the paper in Coq, correcting some errors in the process (last update 3 weeks ago). However, Grosso wrote:
To our knowledge, all of the main ...
- 33.2k
1
vote
Accepted
Constructing set-truncations of types from universes
Given a universe $U$, the type of $U$-small propositions is given by $$\mathrm{Prop} \equiv \sum_{P:U} \prod_{x:P} \prod_{y:P} x = y$$
Given a type $A:U$, for $x:A$ and $y:A$, the type
$$[x = y] \...
- 2,016
1
vote
Why is there no product type in simply typed lambda-calculus?
In spite of all the interesting exchange that has gone back and forth about sum types, the original question about product types (‘how can one prove that the simply typed 𝜆-calculus does not support ...
- 334
Top 50 recent answers are included