Categorical harmony and path induction

Review of Symbolic Logic 10 (2):301-321 (2017)
Download Edit this record How to cite View on PhilPapers
Abstract
This paper responds to recent work in the philosophy of Homotopy Type Theory by James Ladyman and Stuart Presnell. They consider one of the rules for identity, path induction, and justify it along ‘pre-mathematical’ lines. I give an alternate justification based on the philosophical framework of inferentialism. Accordingly, I construct a notion of harmony that allows the inferentialist to say when a connective or concept is meaning-bearing and this conception unifies most of the prominent conceptions of harmony through category theory. This categorical harmony is stated in terms of adjoints and says that any concept definable by iterated adjoints from general categorical operations is harmonious. Moreover, it has been shown that identity in a categorical setting is determined by an adjoint in the relevant way. Furthermore, path induction as a rule comes from this definition. Thus we arrive at an account of how path induction, as a rule of inference governing identity, can be justified on mathematically motivated grounds.
Keywords
No keywords specified (fix it)
PhilPapers/Archive ID
WALCHA-2
Revision history
Archival date: 2017-06-27
View upload history
References found in this work BETA
The Logical Basis of Metaphysics.Dummett, Michael; Putnam, Hilary & Conant, James
Category Theory.Awodey, Steve

View all 19 references / Add more references

Citations of this work BETA

Add more citations

Added to PP index
2017-05-18

Total views
97 ( #24,513 of 40,103 )

Recent downloads (6 months)
24 ( #21,198 of 40,103 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks to external links.