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
Upload history
Archival date: 2017-06-27
View other versions
Added to PP index
2017-05-18

Total views
195 ( #31,632 of 64,180 )

Recent downloads (6 months)
14 ( #40,401 of 64,180 )

How can I increase my downloads?

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