CATEGORICAL HARMONY AND PATH INDUCTION

DOI10.1017/S1755020317000077zbMath1384.03093OpenAlexW2606054052MaRDI QIDQ5274880

Patrick M. Walsh

Publication date: 6 July 2017

Published in: The Review of Symbolic Logic (Search for Journal in Brave)

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

zbMATH Keywords

harmonycategory theoryhomotopy type theoryphilosophy of logic

Mathematics Subject Classification ID

Related Items (2)

The hole argument, take \(n\) ⋮ The justification of identity elimination in Martin-Löf's type theory

Uses Software

• MathOverflow

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Categorical logic and type theory
• Generalized definitional reflection and the inversion principle
• A judgmental reconstruction of modal logic
• Identity in Homotopy Type Theory, Part I: The Justification of Path Induction
• Adjointness in Foundations
• What is Required of a Foundation for Mathematics?
• Does Homotopy Type Theory Provide a Foundation for Mathematics?
• Not so stable
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Categorical Harmony and Paradoxes in Proof-Theoretic Semantics

This page was built for publication: CATEGORICAL HARMONY AND PATH INDUCTION