Varieties of cubical sets

DOI10.1007/978-3-319-57418-9_5MaRDI QIDQ5283204zbMATH OpenOpenAlexFDO

Authors Ulrik Buchholtz, Edward Morehouse

Publication date 21 July 2017

Published in Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1701.08189

Mathematics Subject Classification ID

Theories (e.g., algebraic theories), structure, and semantics (18C10) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Abstract: We define a variety of notions of cubical sets, based on sites organized using substructural algebraic theories presenting PRO(P)s or Lawvere theories. We prove that all our sites are test categories in the sense of Grothendieck, meaning that the corresponding presheaf categories of cubical sets model classical homotopy theory. We delineate exactly which ones are even strict test categories, meaning that products of cubical sets correspond to products of homotopy types.

Recommendations

• The cubical category with connections is a strict test category
• Symmetric cubical sets
• Nominal presentation of cubical sets models of type theory
• scientific article; zbMATH DE number 1924514
• A cubical approach to straightening

Cites work

• Computational higher-dimensional type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• Grothendieck's homotopy theory
• Higher algebraic K-theory: I
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 1924514 (Why is no real title available?)
• Normal forms and truth tables for fuzzy logics
• The cubical category with connections is a strict test category

Cited in

(26)

• A cubical model of homotopy type theory
• Homology groups of cubical sets with connections
• Hilbert cubes meet arithmetic sets
• Equivalence of cubical and simplicial approaches to \((\infty, n)\)-categories
• scientific article; zbMATH DE number 1924514 (Why is no real title available?)
• Internal universes in models of homotopy type theory
• Syntax and models of Cartesian cubical type theory
• Cubical methods in homotopy type theory and univalent foundations
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing
• A cubical approach to straightening
• Nominal presentation of cubical sets models of type theory
• Symmetric cubical sets
• Simplicial sets inside cubical sets
• Induced model structures for higher categories
• Cubical models of higher categories without connections
• Higher Structures in Homotopy Type Theory
• From cubes to twisted cubes via graph morphisms in type theory
• Kripke-Joyal forcing for type theory and uniform fibrations
• Symmetry in the cubical Joyal model structure
• Cubical approximation for directed topology. II
• A parametricity-based formalization of semi-simplicial and semi-cubical sets
• Cubical setting for discrete homotopy theory, revisited
• The equivariant model structure on cartesian cubical sets
• Complexity of cubical cofibration logics. I: coNP-complete examples
• The cubical category with connections is a strict test category

Describes a project that uses

Uses Software

• cubicaltt

This page was built for publication: Varieties of cubical sets

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