|
|
|
|
|
by syrak
689 days ago
|
|
IMO your view, if not common, is kinda intuitive from the point of view of someone trained in set theory/classical logic (i.e., most people before they find an interest in type theory; I myself was here a few years ago). If it feels like you're in a minority, it's because most others who might have the same opinion haven't reached the point where they could articulate it; many just give up way earlier on understanding type theory. It certainly makes sense to a set theorist that union and intersection are more primitive than sums and products. From that perspective, type theory seems like a roundabout and unnecessary way of doing things. The challenge is to imagine type theory as a radically different foundation to logic (because that's what it is), with sums and products as primitives instead, for one superficial difference. It's hard to explain in words. I personally didn't get it without years of first-hand
experience with proof assistants based on type theory. Constructivism and category theory are other possible gateways into the right mindset. There is one key difference which I think highlights the charm and simplicity of type theory without delving in technical details too much. The syntax of set theory is in two layers: there are sets, and there are propositions (about elements of those sets). In contrast, there is only one such "layer" in (dependent) type theory: types. Types play the role of both sets and propositions if you want to encode set theory in type theory. The point is that types can be much more than either of those things, and that idea is inherently difficult to convey to someone whose only conception of logic is sets and propositions. |
|