Realizability of Univalence: Modest Kan complexes

Abstract

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 that is required to show that there is a univalent universe of modest Kan complexes among simplicial assemblies.

This paper has been replaced by 'Constructive Simplicial Homotopy'

References in corpus (1)

• Understanding the small object argument

Cited by in corpus (1)

• Lifting Problems in Grothendieck Fibrations