License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2020.8
URN: urn:nbn:de:0030-drops-138876
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13887/
Hugunin, Jasper
Why Not W?
Abstract
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.
BibTeX - Entry
@InProceedings{hugunin:LIPIcs.TYPES.2020.8,
author = {Hugunin, Jasper},
title = {{Why Not W?}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {8:1--8:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13887},
URN = {urn:nbn:de:0030-drops-138876},
doi = {10.4230/LIPIcs.TYPES.2020.8},
annote = {Keywords: dependent types, intensional type theory, inductive types, W types}
}
