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-, $\Sigma$-, and $\Pi$-types need not be locally Cartesian closed, but is necessarily a $\pi$-clan. We exploi…