Spahn univalence in simplicial sets

1. Representability of fibrations

Let $X$ be a simplicial set, let . $W_\alpha(X)$ denote the class of well ordered morphisms $f:Y\to X$. Then the assignation $X\mapsto W_\alpha_X$ is a functor which is representable by the functor $y^{op}\circ y^{op}:\Delta^{op}\to Set$ where $y$ is Yoneda (…)

References

• Kapulkin, Lumsdaine, Voevodsky, univalence in simplicial sets

For a different model of the univalence axiom:

• Ieke Moerdijk, Fiber Bundles and Univalence

For universes:

• Thomas Streicher, Universes in Toposes, In: From sets and types to topology and analysis: towards practicable foundations for constructive mathematics (ps,pdf)

For references and recent contributions on cordials:

• Joan Bagaria, Carles Casacuberta?, Adrian Mathias, Jiri Rosicky? Definable orthogonality classes in accessible categories are small, arXiv