A cubical approach to synthetic homotopy theory

DOI10.1109/LICS.2015.19MaRDI QIDQ4635794zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(16)

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

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)