A Homotopical Model of Univalence

Opening obstruction

The syntax alone cannot show that univalence is consistent with intensional identity or explain which computation rules the axiomatic principle lacks.

Development contract

Construct the simplicial-set model of the contextual type theory from chapter 191, interpret its dependent type formers and identity types, and build the universe of small Kan fibrations. Under the stated two-inaccessible-cardinal and classical model-structure assumptions, prove that this universe is univalent and derive relative consistency without claiming definitional computation.