Realizability of Univalence: Modest Kan complexes

الأصل · EN

A modest Kan complex is a modest simplicial set which has a right lifting property with respect to horn inclusions Λₖ[n] → Δ[n]. This paper develops the categorical logical that is required to show that there is a univalent universe of modest Kan complexes among simplicial assemblies.