model category, model -category
Definitions
Morphisms
Universal constructions
Refinements
Producing new model structures
Presentation of -categories
Model structures
for -groupoids
on chain complexes/model structure on cosimplicial abelian groups
related by the Dold-Kan correspondence
for equivariant -groupoids
for rational -groupoids
for rational equivariant -groupoids
for -groupoids
for -groups
for -algebras
general -algebras
specific -algebras
for stable/spectrum objects
for -categories
for stable -categories
for -operads
for -categories
for -sheaves / -stacks
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A model structure on simplicial sets valid in constructive mathematics that reduced to the classical model structure on simplicial sets in presence of the law of excluded middle and axiom of choice.
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
Fibrations and acyclic fibrations
are defined using the right lifting property with respect to the usual sets of horn inclusions and boundary inclusions?. However, the meaning of this definition is more refined: due to the constructive nature of the existential quantifier, being an (acyclic) fibration means we have a section of the map from the set of solutions to lifting problems to the set of lifting problems.
Simplicial weak equivalences? must also be defined more carefully.
Suppose is a simplicial map.
We follow GambinoSattlerSzumilo19. They give two (equivalent) definitions.
In the first proof:
In the second proof:
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 -simplices into all -simplices is a decidable inclusion of sets.
Likewise, cofibrations are simplicial maps such that is a decidable inclusion of sets and the inclusion of degenerate -simplices as a subset into 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.
Simon Henry, Weak model categories in classical and constructive mathematics (arXiv:1807.02650)
Simon Henry, A constructive account of the Kan-Quillen model structure and of Kan’s functor (arXiv:1905.06160)
Nicola Gambino, Simon Henry, Towards a constructive simplicial model of Univalent Foundations (arXiv:1905.06281)
Nicola Gambino, Christian Sattler, Karol Szumiło, The constructive Kan-Quillen model structure: two new proofs (arXiv:1907.05394)
Last revised on October 12, 2022 at 12:45:46. See the history of this page for a list of all contributions to it.