Cover Image

The equivariant model structure on cartesian cubical sets

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Awodey, Steve, Cavallo, Evan, Coquand, Thierry, Riehl, Emily, Sattler, Christian
Format:	Preprint
Published:	2024
Subjects:	Algebraic Topology Logic in Computer Science Logic
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Path Types in Algebraic Type Theory
by: Awodey, Steve, et al.
Published: (2026)

Constructive higher sheaf models with applications to synthetic mathematics
by: Coquand, Thierry, et al.
Published: (2026)

Eliminating reversals from cubical type theories
by: Cavallo, Evan, et al.
Published: (2026)

Central H-spaces and banded types
by: Buchholtz, Ulrik, et al.
Published: (2023)

Internal languages of locally cartesian closed $(\infty,1)$-categories
by: Cherradi, El Mehdi
Published: (2025)

Symmetric Monoidal Smash Products in Homotopy Type Theory
by: Ljungström, Axel
Published: (2024)

Delooping cyclic groups with lens spaces in homotopy type theory
by: Mimram, Samuel, et al.
Published: (2024)

Computational Synthetic Cohomology Theory in Homotopy Type Theory
by: Ljungström, Axel, et al.
Published: (2024)

Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda
by: Ljungström, Axel, et al.
Published: (2023)

Classifying covering types in homotopy type theory
by: Mimram, Samuel, et al.
Published: (2025)

The Steenrod squares via unordered joins
by: Ljungström, Axel, et al.
Published: (2025)

Hypercubical manifolds in homotopy type theory
by: Mimram, Samuel, et al.
Published: (2025)

Computational techniques for sheaf cohomology of locally profinite sets
by: Schachner, Mark
Published: (2026)

Relative elegance and cartesian cubes with one connection
by: Cavallo, Evan, et al.
Published: (2022)

Impredicative Encodings of (Higher) Inductive Types
by: Awodey, Steve, et al.
Published: (2018)

Reduction Free Normalisation for a proof irrelevant type of propositions
by: Coquand, Thierry
Published: (2021)

Manifold Diagrams for Higher Categories
by: Heidemann, Lukas
Published: (2024)

Epimorphisms and Acyclic Types in Univalent Foundations
by: Buchholtz, Ulrik, et al.
Published: (2024)

Formalizing the zigzag construction of path spaces of pushouts
by: Štěpančík, Vojtěch
Published: (2025)

On cohomology of locally profinite sets
by: Aoki, Ko
Published: (2024)

Univalence without function extensionality
by: Cavallo, Evan, et al.
Published: (2026)

Wadge degrees of $Δ^0_2$ omega-powers
by: Finkel, Olivier, et al.
Published: (2024)

Towards solid abelian groups: A formal proof of Nöbeling's theorem
by: Asgeirsson, Dagur
Published: (2023)

Persistent homology of partially ordered spaces
by: Calk, Cameron, et al.
Published: (2023)

A type-theoretic definition of lax $(\infty,\infty)$-limits
by: Mikhail, Thomas Jan
Published: (2024)

Two Remarks about Game Semantics of Classical Logic
by: Coquand, Thierry
Published: (2026)

Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
by: Coquand, Thierry
Published: (2026)

Classification of Covering Spaces and Canonical Change of Basepoint
by: Wemmenhove, Jelle, et al.
Published: (2024)

Choice axioms and Postnikov completeness
by: Anel, Mathieu, et al.
Published: (2024)

Modal Fracture of Higher Groups
by: Myers, David Jaz
Published: (2021)

Higher presentable categories and limits
by: Aoki, Ko
Published: (2025)

Basic Category Theory
by: Leinster, Tom
Published: (2016)

Interpreting type theory in a quasicategory: a Yoneda approach
by: Cherradi, El Mehdi
Published: (2022)

Elementary $\infty$-toposes from type theory
by: Apol, Daniël, et al.
Published: (2025)

Higher geometric sheaf theories
by: Stenzel, Raffael
Published: (2022)

$2$-dimensional Lawvere theories: commutativity and lax phenomena
by: Perutka, Tomáš
Published: (2026)

Non-trivial higher homotopy of first-order theories
by: Campion, Tim, et al.
Published: (2023)

Synthetic perspectives on spaces and categories
by: Riehl, Emily
Published: (2025)

On the Formalization of Network Topology Matrices in HOL
by: Aksoy, Kubra, et al.
Published: (2026)

A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
by: Bezem, Marc, et al.
Published: (2026)