Realizability of Univalence: Modest Kan complexes

TL;DR

This paper explores the conditions under which modest Kan complexes can form a univalent universe within simplicial assemblies, advancing the understanding of realizability in homotopy type theory.

Contribution

It develops the categorical logic necessary to demonstrate the existence of a univalent universe of modest Kan complexes.

Findings

Established the categorical framework for modest Kan complexes

Proved the existence of a univalent universe within simplicial assemblies

Enhanced the theoretical understanding of realizability in homotopy type theory

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.