Non-wellfounded trees in homotopy type theory

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

External organisations

  • Institut de Recherche en Informatique de Toulouse Université Paul Sabatier, Toulouse, France
  • University of Nottingham

Abstract

We prove a conjecture about the constructibility of coinductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presence of inductive types, coinductive types are derivable. Indeed, in this work, we construct coinductive types in a subsystem of Homotopy Type Theory; this subsystem is given by Intensional Martin- Löf type theory with natural numbers and Voevodsky's Univalence Axiom. Our results are mechanized in the computer proof assistant Agda.

Details

Original languageEnglish
Title of host publication13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
EditorsThorsten Altenkirch
Publication statusPublished - 1 Jul 2015
Event13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) - Warsaw, Poland
Duration: 1 Jul 20153 Jul 2015

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl
Volume38
ISSN (Electronic)1868-8969

Conference

Conference13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
CountryPoland
CityWarsaw
Period1/07/153/07/15

Keywords

  • Agda, Coinductive types, Computer theorem proving, Homotopy Type Theory