New answers tagged

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