Model Categories and Simplicial Semantics of Type Theory

Opening obstruction

Horn filling supplies fibrations but not yet a model of substitution, dependent products, identity, and universes with the required stability equations.

Development contract

Start with simplicial sets and a Kan fibration $p:E\to B$: factor one map, prove pullback stability, and obtain comprehension, dependent products, and path objects. Then construct the classifier ${\tilde{U}}_{\alpha }\to U_{\alpha }$ for $\alpha$-small fibrations and state its closure theorem under the required inaccessible-cardinal and classical model-structure hypotheses; general model-category preliminaries remain separate from this simplicial construction.