philosophy and univalence

Stream: new members

[ranjan]

hi, i’m interested in type theory as a possible language for codifying philosophy. i’m specifically most interested in inferential role semantics along the lines of robert brandom’s work. i haven’t seen any code implementations of that and it seems like it demands a type theory retelling. the proposals that i’ve seen pointing in this direction (david corfield’s book and hegel pages on nlab) suggest that modal homotopy type theory is a good base language for philosophy. i know lean doesn’t support hott in current versions, but i’m not at the point of understanding why these foundational differences matter- i think i just need to start working with propositions as types- and lean seems like the easiest of these languages to learn.

basically, i’m really interested in seeing existing projects around inferentialism and proof theoretic semantics in general. do people work on this sort of thing in lean or in other languages? i also want to know if the lack of hott may prove limiting in any way; i’d be interested in knowing why the decision was made to drop support for it; is it, in practice, not actually as nice of a place to work in as more traditional set theoretic foundations? how should i understand lean’s metatheory in comparison with alternatives?

[Mario Carneiro]

I would start from the presumption that HoTT is not needed, much less modal HoTT. A good starting point is to come up with some primitive notions you wish to express, and try to state them in lean or ask about it here. Theorems are even better, since they can be used to make sure the notions and axioms are working as expected