# The constructive Kan-Quillen model structure: two new proofs

## TL;DR

This paper provides two new constructive proofs for the Kan-Quillen model structure on simplicial sets, avoiding complex combinatorics and establishing properness, thus enhancing the foundational understanding in a constructive setting.

## Contribution

It introduces two novel, self-contained constructive proofs of the Kan-Quillen model structure and its properness, simplifying previous combinatorial approaches.

## Key findings

- Constructive proofs of the Kan-Quillen model structure
- Proofs of left and right properness in a constructive setting
- Simplification of existing combinatorial arguments

## Abstract

We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs are entirely self-contained and avoid complex combinatorial arguments on anodyne extensions. We also give new constructive proofs of the left and right properness of the model structure.