FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Impredicative Encodings of (Higher) Inductive Types

Authors: Steve Awodey, Jonas Frey and Sam Speight

Paper Information

Title:Impredicative Encodings of (Higher) Inductive Types
Authors:Steve Awodey, Jonas Frey and Sam Speight
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:polymorphism, impredicativity, impredicative encodings, inductive types, higher inductive types, system F, Martin-L\"{o}f type theory, homotopy type theory
Abstract:

ABSTRACT. The impredicative $\forall$ operation in Girard's system F permits encodings of various inductive types, such as the natural numbers. However, these types fail to satisfy the relevant $\eta$-rules, and so, in dependent type theory, lack \emph{dependent} elimination rules. We work in Martin-L\"{o}f type theory with an impredicative universe. Using ideas from homotopy type theory, we refine the impredicative encodings so that the dependent elimination rules do hold. We construct a type of natural numbers as an initial algebra, which arises as a subtype of the System F encoding. We also encode some higher inductive types, such as the unit circle $S^1$.

Pages:10
Talk:Jul 10 11:00 (Session 54E)
Paper: