eng
Schloss Dagstuhl β Leibniz-Zentrum fΓΌr Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
8:1
8:9
10.4230/LIPIcs.TYPES.2020.8
article
Why Not W?
Hugunin, Jasper
1
https://orcid.org/0000-0002-1133-5354
Carnegie Mellon University, Pittsburgh, PA, USA
In an extensional setting, π types are sufficient to construct a broad class of inductive types, but in intensional type theory the standard construction of even the natural numbers does not satisfy the required induction principle. In this paper, we show how to refine the standard construction of inductive types such that the induction principle is provable and computes as expected in intensional type theory without using function extensionality. We extend this by constructing from π an internal universe of codes for inductive types, such that this universe is itself an inductive type described by a code in the next larger universe. We use this universe to mechanize and internalize our refined construction.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.8/LIPIcs.TYPES.2020.8.pdf
dependent types
intensional type theory
inductive types
W types