scientific article; zbMATH DE number 7215286

MaRDI QIDQ5114825

Kuen-Bang Hou (Favonia), Ulrik Buchholtz

Publication date: 26 June 2020

Full work available at URL: https://arxiv.org/abs/1802.02191

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Uses Software

• cubicaltt
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Homotopy type theory in Lean
• Meaning explanations at higher dimension
• π n (S n ) in Homotopy Type Theory
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
• On Higher Inductive Types in Cubical Type Theory
• The Independence of Markov's Principle in Type Theory.
• Computational higher-dimensional type theory
• Axiomatic Approach to Homology Theory