# Homotopy Type Theory in Lean

## TL;DR

This paper presents a library for homotopy type theory in Lean, emphasizing synthetic homotopy theory using minimal primitives like quotients and truncations, and employing cubical methods for formalization.

## Contribution

It introduces a homotopy type theory library in Lean that leverages minimal primitives and cubical techniques for synthetic homotopy theory.

## Key findings

- Library supports formalization of synthetic homotopy theory
- Uses only quotients and truncations as primitive higher inductive types
- Employs cubical methods for efficient proof development

## 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.