License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2018.20
URN: urn:nbn:de:0030-drops-91906
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9190/
Go to the corresponding LIPIcs Volume Portal

Kaposi, Ambrus ; Kovács, András

A Syntax for Higher Inductive-Inductive Types

pdf-format:
LIPIcs-FSCD-2018-20.pdf (0.4 MB)

Abstract

Higher inductive-inductive types (HIITs) generalise inductive types of dependent type theories in two directions. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalising higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy reals and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a domain-specific type theory. A context in this small type theory encodes a HIIT by listing the type formation rules and constructors. The type of the elimination principle and its beta-rules are computed from the context using a variant of the syntactic logical relation translation. We show that for indexed W-types and various examples of HIITs the computed elimination principles are the expected ones. Showing that the thus specified HIITs exist is left as future work. The type theory specifying HIITs was formalised in Agda together with the syntactic translations. A Haskell implementation converts the types of sorts and constructors into valid Agda code which postulates the elimination principles and computation rules.

BibTeX - Entry

@InProceedings{kaposi_et_al:LIPIcs:2018:9190,
  author =	{Ambrus Kaposi and Andr{\'a}s Kov{\'a}cs},
  title =	{{A Syntax for Higher Inductive-Inductive Types}},
  booktitle =	{3rd International Conference on Formal Structures for  Computation and Deduction (FSCD 2018)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{H{\'e}l{\`e}ne Kirchner},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9190},
  URN =		{urn:nbn:de:0030-drops-91906},
  doi =		{10.4230/LIPIcs.FSCD.2018.20},
  annote =	{Keywords: homotopy type theory, inductive-inductive types, higher inductive types, quotient inductive types, logical relations}
}

Keywords: homotopy type theory, inductive-inductive types, higher inductive types, quotient inductive types, logical relations
Collection: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Issue Date: 2018
Date of publication: 04.07.2018

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