Kaposi, Ambrus ;
Kovács, András
A Syntax for Higher InductiveInductive Types
Abstract
Higher inductiveinductive 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 welltyped syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a domainspecific 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 betarules are computed from the context using a variant of the syntactic logical relation translation. We show that for indexed Wtypes 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 InductiveInductive Types}},
booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
pages = {20:120:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770774},
ISSN = {18688969},
year = {2018},
volume = {108},
editor = {H{\'e}l{\`e}ne Kirchner},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9190},
URN = {urn:nbn:de:0030drops91906},
doi = {10.4230/LIPIcs.FSCD.2018.20},
annote = {Keywords: homotopy type theory, inductiveinductive types, higher inductive types, quotient inductive types, logical relations}
}
2018
Keywords: 

homotopy type theory, inductiveinductive types, higher inductive types, quotient inductive types, logical relations 
Seminar: 

3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Issue date: 

2018 
Date of publication: 

2018 