Papers With

← All papers
First page of Polynomial functors in π-clans for the semantics of type theory

Polynomial functors in π-clans for the semantics of type theory

Joseph Hua, Yiming Xu

math.CT Feb 5, 2026 · v1
formalization mathlib category-theory type-theory
Read PDF arXiv abstract Code
TL;DR
Definitions and theorems on polynomial functors in π-clans and MLTT semantics are formalized in Lean within the HoTTLean repository, building on Mathlib and Poly.
Abstract
The category of contexts underlying a model of Martin-Löf type theory with Unit-, $Σ$-, and $Π$-types need not be locally Cartesian closed, but is necessarily a $π$-clan. We exploit this $π$-clan structure to build the theory of polynomial functors. This paper presents two equivalent notions of strict semantics for MLTT in this weaker setting, respectively "elementary models" - reformulating categories with families - and "algebraic models" - reformulating natural models. These components fit into a practical sequence of steps for constructing models of MLTT: building an elementary model, extracting a $π$-clan from the elementary model, and then using polynomial functors built on the $π$-clan structure to convert the elementary model into an algebraic one.
Problem

The category of contexts of a model of Martin-Löf type theory with Unit-, Σ- and Π-types need not be locally Cartesian closed. Natural-model-style algebraic semantics usually assume LCC structure, but such a category is necessarily a π-clan.

Approach

The authors develop polynomial functors in π-clans using partial right adjoints. They define elementary models, which reformulate categories with families, and algebraic models, which reformulate natural models using these polynomial functors. They then construct translations between the two notions. Many definitions and theorems are formalized in Lean as part of the HoTTLean project, building on Mathlib and the Lean Poly library.

Results

Algebraic semantics of MLTT is shown to be inter-translatable with elementary semantics without assuming LCC structure, which confirms that the algebraic definition models the type formers correctly. The Lean formalization includes the translations and the proof that groupoids form a π-clan, and HoTTLean uses it to support its groupoid model.