 Further connections between identity types and notions from homotopy theory and higher categories were subsequently discovered by (Awodey and Warren 2009), (Lumsdaine 2010), and (van den Berg and Garner 2011). Voevodsky realized that the whole intensional intuitionistic type theory could be modelled by a well-known category studied in homotopy theory, namely the Kan simplicial sets. Inspired by this model he introduced the univalence axiom. For a universe \(\U\) of small types, this axiom states that the substitution map associated with the \(J\)-operator