A Cubical Approach to Synthetic Homotopy Theory

DOI10.1109/LICS.2015.19zbMath1395.55019OpenAlexW1553187622MaRDI QIDQ4635794

Guillaume Brunerie, Daniel R. Licata

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)

Related Items (14)

The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory ⋮ Adjoint Logic with a 2-Category of Modes ⋮ From reversible programs to univalent universes and back ⋮ Homotopical patch theory ⋮ Unnamed Item ⋮ Observability in the univalent universe ⋮ Homotopy type theory in Lean ⋮ Meaning explanations at higher dimension ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Syntax and models of Cartesian cubical type theory

This page was built for publication: A Cubical Approach to Synthetic Homotopy Theory