Polynomial functors in π-clans for the semantics of type theory
Joseph Hua, Yiming Xu
TL;DR
This work develops a theory of polynomial functors in $\pi$-clans to provide a strict semantic framework for Martin-Löf type theory with unit, sigma, and pi types. It introduces two equivalent strict viewpoints—elementary semantics and algebraic semantics—and proves translations between them, enabling construction of MLTT models in weaker, non-LCC contexts. The central contribution is the algebraic presentation of type formers via polynomial functors in $\pi$-clans, together with a method to extract algebraic formers from a clan and to recover elementary models from algebraic ones. The results generalize polynomial-functor techniques beyond locally Cartesian closed categories and are formalized in the Lean-based HoTTLean project, with potential applications to groupoid models and broader semantic frameworks for type theory.
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.