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