Papers With

← All papers
First page of Internal Algebraic Type Theory

Internal Algebraic Type Theory

Joseph Hua

math.CT Jul 30, 2026 · v1 cs.PL
formalization tooling mathlib type-theory
Read PDF arXiv abstract Code
TL;DR
Implements HoTTLean, a Lean DSL with a deep embedding of MLTT, and formalizes its semantics and the groupoid model using Mathlib.
Abstract
This thesis brings us closer to applying computer-assisted, internal, type-theoretic reasoning to a category, with examples in the category of cubical sets, the category of groupoids, and the category of categories. The steps we make towards this general goal are both in furthering the type theoretic analysis of these examples, as well as implementing computer-assisted syntax-semantic reasoning as part of the HoTTLean project. One key component of this work is the consideration of new exponentiability conditions with respect to a class of maps in a category, and the development of polynomial functors for these maps, making the methods of "algebraic type theory" possible in this very general setting.
Problem

The goal is computer-assisted, internal, type-theoretic reasoning about categories such as cubical sets, groupoids and categories. Proofs are written in a domain-specific language and then interpreted into a formalized semantic model.

Approach

The thesis introduces exponentiability conditions relative to a class of maps (preclans) and develops polynomial functors for these maps, which extends algebraic type theory to this general setting. As part of the HoTTLean project, it implements a DSL for Martin-Löf type theory in Lean through metaprogramming. The DSL rests on a deep embedding of MLTT whose interpretation into a generic natural model is formalized in Lean. The Hofmann–Streicher groupoid model, built on Mathlib's groupoids, serves as a test case.

Results

Users can write synthetic proofs in the DSL that are interpreted as constructions on Mathlib groupoids. Parts of the categorical arguments, including a version of the polynomial-functor development, are formalized in Lean. Further type-theoretic analysis is given for cubical sets, groupoids and categories.