# Towards a constructive simplicial model of Univalent Foundations

## TL;DR

This paper develops a constructive version of Voevodsky's simplicial model of univalent foundations by establishing key homotopy-theoretic results constructively, enabling a model supporting various type formers and univalence.

## Contribution

It provides the first constructive counterparts of essential simplicial homotopy theory results needed for univalent foundations, including a univalent universe and comprehension category.

## Key findings

- Constructive proof of the Kan-Quillen model structure.
- Dependent products along fibrations with cofibrant domains preserve fibrations.
- Established the univalent classifying fibration for small fibrations.

## Abstract

We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of univalent foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory, building on the constructive version of the Kan-Quillen model structure established by the second-named author. In particular, we show that dependent products along fibrations with cofibrant domains preserve fibrations, establish the weak equivalence extension property for weak equivalences between fibrations with cofibrant domain and define a univalent classifying fibration for small fibrations between bifibrant objects. These results allow us to define a comprehension category supporting identity types, $\Sigma$-types, $\Pi$-types and a univalent universe, leaving only a coherence question to be addressed.