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: https://drops.dagstuhl.de/opus/volltexte/2021/13887/
Go to the corresponding LIPIcs Volume Portal


Hugunin, Jasper

Why Not W?

pdf-format:
LIPIcs-TYPES-2020-8.pdf (0.6 MB)


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}
}

Keywords: dependent types, intensional type theory, inductive types, W types
Collection: 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Issue Date: 2021
Date of publication: 07.06.2021
Supplementary Material: Software (Source Code): https://github.com/jashug/WhyNotW/releases/tag/v0.1 archived at: https://archive.softwareheritage.org/swh:1:rel:75acce4d588f3622361f0adc3f1255ac24147669


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI