A cubical approach to synthetic homotopy theory

DOI10.1109/LICS.2015.19zbMATH Open1395.55019OpenAlexW1553187622MaRDI QIDQ4635794FDOQ4635794

Authors: Daniel R. Licata, Guillaume Brunerie 

Publication date: 23 April 2018

Published in: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/lics.2015.19

Recommendations

• Canonicity and homotopy canonicity for cubical type theory
• Homotopy type theory in Lean
• scientific article; zbMATH DE number 7003193
• On higher inductive types in cubical type theory
• A cubical model of homotopy type theory

zbMATH Keywords

theorem provingtype theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Cited In (16)

• Synthetic integral cohomology in Cubical Agda
• The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
• From reversible programs to univalent universes and back
• Adjoint logic with a 2-category of modes
• The equivalence of the torus and the product of two circles in homotopy type theory
• A purely homotopy-theoretic proof of the Blakers-Massey theorem for \(n\)-cubes
• Constructing higher inductive types as groupoid quotients
• Homotopical patch theory
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Homotopy type theory in Lean
• Meaning explanations at higher dimension
• Cubical type theory: a constructive interpretation of the univalence axiom
• Coherence for monoidal groupoids in HoTT
• The Cayley-Dickson construction in homotopy type theory
• Syntax and models of Cartesian cubical type theory
• Observability in the univalent universe

This page was built for publication: A cubical approach to synthetic homotopy theory

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