{"id":"arxiv/2602.05689","url":"https://arxiv.org/abs/2602.05689","tags":["math.CT"],"score":0,"title":"Polynomial functors in π-clans for the semantics of type theory","domain":"math.CT","source":"arxiv","authors":["Joseph Hua","Yiming Xu"],"reviews":0,"subject":"math.CT","summary":"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,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-02-05","reactions":{}}