Polynomial functors in {\pi}-clans for the semantics of type theory

TL;DR

This paper develops a framework using polynomial functors within {\

Contribution

It introduces two equivalent notions of strict semantics for MLTT based on {\

Findings

Provides a method to construct models of MLTT using polynomial functors.

Shows the equivalence of elementary and algebraic models in this setting.

Offers a practical sequence for building MLTT models from elementary to algebraic.

Abstract

The category of contexts underlying a model of Martin-L\"of type theory with Unit-, $\Sigma$-, and $\Pi$-types need not be locally Cartesian closed, but is necessarily a $\pi$-clan. We exploit this $\pi$-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 $\pi$-clan from the elementary model, and then using polynomial functors built on the $\pi$-clan structure to convert the elementary model into an algebraic one.