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

Joseph Hua, Yiming Xu

The category of contexts underlying a model of Martin-Löf type theory with Unit-, $\hat{I}\pounds$-, and $\hat{I}$-types need not be locally Cartesian closed, but is necessarily a $\ddot{I}€$-clan. We ex…