## 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 ...

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 ...

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] \...

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 ...

Top 50 recent answers are included

#### Related Tags

type-theory × 200lo.logic × 114

homotopy-type-theory × 49

ct.category-theory × 47

reference-request × 23

set-theory × 21

foundations × 21

lambda-calculus × 19

constructive-mathematics × 17

proof-theory × 13

soft-question × 9

computability-theory × 9

categorical-logic × 9

computer-science × 8

mathematical-philosophy × 8

proof-assistants × 7

new-foundations × 7

homotopy-theory × 6

higher-category-theory × 5

topos-theory × 5

universal-algebra × 5

intuitionism × 5

model-theory × 4

terminology × 4

formal-languages × 4