# nLab constructive model structure on simplicial sets

Contents

model category

## Model structures

for ∞-groupoids

### for $(\infty,1)$-sheaves / $\infty$-stacks

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

## Idea

The original proofs of the existence of the classical model structure on simplicial sets are based in classical mathematics as they use the principle of excluded middle and the axiom of choice, and are hence not valid in constructive mathematics. This becomes more than a philosophical issue with the relevance of this model category-structure in homotopy type theory, where internalization into the type theory requires constructive methods for interpreting proofs as programs.

A constructively valid model structure on simplicial sets and coinciding with the classical model structure if excluded middle and axiom of choice are assumed was found in Henry 19. Alternative simpler proofs were found in Gambino-Sattler-Szumiło 19

## Properties

### Cofibrant objects

While in the classical model structure on simplicial sets all objects (simplicial sets) are cofibrant, a simplicial set is cofibrant in the constructive model structure if and only if the inclusion of degenerate $n$-simplices into all $n$-simplices is a decidable inclusion of sets.

Likewise, cofibrations $A\to B$ are simplicial maps such that $A_n\to B_n$ is a decidable inclusion of sets and the inclusion of degenerate $n$-simplices as a subset into $B_n\setminus A_n$ is also a decidable inclusion.

Since not all objects are cofibrant, left properness is no longer automatic, but can still be established through nontrivial arguments.

This model structure is also right proper.

See Henry 19 and Gambino-Sattler-Szumiło 19 for a proof of these claims.

## References

Last revised on July 15, 2019 at 06:27:24. See the history of this page for a list of all contributions to it.