A Cubical Approach to Synthetic Homotopy Theory
From MaRDI portal
Publication:4635794
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
