Realizability of Univalence: Modest Kan complexes

Wouter Pieter Stekelenburg

A modest Kan complex is a modest simplicial set which has a right lifting property with respect to horn inclusions ${\Lambda }_k[n]\to \Delta [n]$. This paper develops the categorical logical th…