Homotopical patch theory

DOI10.1017/S0956796816000198zbMath1420.68060OpenAlexW2520449974MaRDI QIDQ5371976

Edward Morehouse, Robert Harper, Daniel R. Licata, Carlo Angiuli

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796816000198

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Topological categories, foundations of homotopy theory (55U40)

Related Items (3)

The construction of set-truncated higher inductive types ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types

Uses Software

• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A categorical theory of patches
• The identity type weak factorisation system
• Containers: Constructing strictly positive types
• Canonicity for 2-dimensional type theory
• Types are weak ω -groupoids
• Two-dimensional models of type theory
• Homotopy theoretic models of identity types
• Weak ω-Categories from Intensional Type Theory
• Eilenberg-MacLane spaces in homotopy type theory
• A Cubical Approach to Synthetic Homotopy Theory
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• 2-Dimensional Directed Type Theory
• A generalization of the Takeuti–Gandy interpretation
• Univalence for inverse diagrams and homotopy canonicity
• On the interpretation of intuitionistic number theory

This page was built for publication: Homotopical patch theory