New answers tagged

0 votes

Are there any books or articles that contain information on the P weak omega or second order predicate calculi?

I've talked about a couple of these in this question, though Neel's answer gives a lot of insight as well, though I didn't dwell on $\lambda P_\underline{\omega}$ specifically. $\lambda P_2$ is quite ...
cody's user avatar
  • 13.8k
2 votes

Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

I claim that $T \cong \mathbb 1+\mathbb2+\mathbb3\,+\,…$. I will prove the type equivalence and then show what terms of type $T$ correspond to values of type $\mathbb 1+\mathbb2+\mathbb3\,+\,…$ The ...
winitzki's user avatar
  • 294
0 votes

Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

They are inequivalent. Let's number the three $\phi$ you listed as $\phi_1, \phi_2, \phi_3$. Then $\phi_1 \mathbb N (\lambda f. f(0)+1) = 1$, while $\phi_2, \phi_3$ both give the result $2$. Therefore ...
Trebor's user avatar
  • 335
5 votes
Accepted

Generalizations, or extensions of W-types in MLTT

The representation issue of W-types was resolved by Jasper Hugunin. So from type formers $0$, $1$, $2$, $W$, $\Pi$, $\Sigma$, identity and a universe hierarchy we do get all indexed inductive families ...
András Kovács's user avatar
3 votes

Generalizations, or extensions of W-types in MLTT

You could start with Spartan type theory (which honestly should be upgraded to use evaluation-by-normalization) and add simple inductive datatypes to them. This would involve several steps. First, add ...
Andrej Bauer's user avatar
  • 28.7k

Top 50 recent answers are included