Simplicial sets inside cubical sets

MaRDI QIDQ5858940zbMATH OpenFDO

Authors Thomas Streicher, Jonathan Weinberger

Publication date 15 April 2021

Full work available at URL https://arxiv.org/abs/1911.09594, http://www.tac.mta.ca/tac/volumes/37/10/37-10abs.html

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

cubical setssimplicial setsunivalence axiomuniverses

Mathematics Subject Classification ID

Type theory (03B38) Categorical logic, topoi (03G30) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Abstract: As observed recently by various people the topos $mathbfsSet$ of simplicial sets appears as essential subtopos of a topos $mathbfcSet$ of cubical sets, namely presheaves over the category $mathbfFL$ of finite lattices and monotone maps between them. The latter is a variant of the cubical model of type theory due to Cohen et al. for the purpose of providing a model for a variant of type theory which validates Voevodsky's Univalence Axiom and has computational meaning. Our contribution consists in constructing in $mathbfcSet$ a fibrant univalent universe for those types that are sheaves. This makes it possible to consider $mathbfsSet$ as a submodel of $mathbfcSet$ for univalent Martin-L"of type theory. Furthermore, we address the question whether the type-theoretic Cisinski model structure considered on $mathbfcSet$ coincides with the test model structure, the latter of which models the homotopy theory of spaces. We do not provide an answer to this open problem, but instead give a reformulation in terms of the adjoint functors at hand.

Recommendations

• Towards a constructive simplicial model of Univalent Foundations
• Model structures on categories of models of type theories
• Syntax and models of Cartesian cubical type theory
• W-types in homotopy type theory
• Unifying Cubical Models of Univalent Type Theory
• Univalence for inverse diagrams and homotopy canonicity
• Martin-Löf identity types in C-systems
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• The simplicial model of univalent foundations (after Voevodsky)
• Decomposing the univalence axiom

Cites work

• A cubical approach to straightening
• Categorical homotopy theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• Grothendieck's homotopy theory
• Higher categories and homotopical algebra
• scientific article; zbMATH DE number 3297895 (Why is no real title available?)
• scientific article; zbMATH DE number 2247252 (Why is no real title available?)
• Presheaves as models for homotopy types
• Simplicial homotopy theory
• The Frobenius condition, right properness, and uniform fibrations
• Varieties of cubical sets

Cited in

(5)

• Model structures on categories of models of type theories
• A cubical approach to straightening
• Sets in homotopy type theory
• Induced model structures for higher categories
• Levels in the toposes of simplicial sets and cubical sets

Describes a project that uses

Uses Software

• cubicaltt

This page was built for publication: Simplicial sets inside cubical sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5858940)