Polynomial functors in π-clans for the semantics of type theory
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,…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2602.05689
curl -X POST /api/v1/records/arxiv/2602.05689/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2602.05689/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'