Skip to main content
6 votes
Accepted

Power of existential types

Universal types can be used to encode the least fixed point, while dually, existential types can be used to encode the greatest fixed point. For example, consider $F(X) = 1 + A \times X$, then the ...
Trebor's user avatar
  • 345
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
  • 29.2k
2 votes

Derivability of `Vector` in pure calculus of constructions

Source 1 does not say anything about deriving the induction principle for inductive types, it's only about non-dependent recursion. Source 2 says that deriving the induction principle is not possible. ...
András Kovács's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible