Meaning explanations at higher dimension

DOI10.1016/j.indag.2017.07.010zbMath1436.03102OpenAlexW2765255795MaRDI QIDQ1688954

Robert Harper, Carlo Angiuli

Publication date: 12 January 2018

Published in: Indagationes Mathematicae. New Series (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.indag.2017.07.010

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Related Items (3)

Higher Structures in Homotopy Type Theory ⋮ Unnamed Item ⋮ Syntax and models of Cartesian cubical type theory

Uses Software

• Coq
• Nuprl
• UniMath
• Lean
• cubicaltt
• GitHub
• RedPRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Logic, language, information and computation. 18th international workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18--20, 2011. Proceedings
• Constructions, proofs and the meaning of logical constants
• The identity type weak factorisation system
• Constructivism in mathematics. An introduction. Volume II
• Computational foundations of basic recursive function theory
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Practical Foundations for Programming Languages
• Canonicity for 2-dimensional type theory
• Types are weak ω -groupoids
• The Lean Theorem Prover (System Description)
• Homotopy theoretic models of identity types
• Weak ω-Categories from Intensional Type Theory
• Setoids in type theory
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• A Cubical Approach to Synthetic Homotopy Theory
• Computational higher-dimensional type theory
• ABSTRACT HOMOTOPY

This page was built for publication: Meaning explanations at higher dimension