# Homotopy Type Theory in Lean

Preprint · Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz

- Archive id: arxiv:1704.06781
- Published: 2017-04-22
- DOI: https://doi.org/10.1007/978-3-319-66107-0_30
- arXiv: https://arxiv.org/abs/1704.06781
- Source URL: https://arxiv.org/abs/1704.06781
- PDF: https://arxiv.org/pdf/1704.06781
- Provenance: arxiv

## Abstract

We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.