> I don't see why you are so eager to say "types are not quite sets" >
I am not, I think. I don't really care. I'm trying to avoid being biased but fall in that trap over and over again. But I know that such people exist <https://en.wikipedia.org/wiki/Type_theory#Differences_from_Set_Theory> and I don't know why someone should insist that they are wrong just because somebody else have a different opinion. This is also a philosophical difference, not just a practical one. But even from a practical point of view everyone have their own definition of feasibility. We can walk backwards or even upside down, that's certainly possible, but not everyone will find this quite feasible. And when I'm not sure what solution is feasible in this particular case, I prefer to reason conservatively. But maybe I'm overreacting sometimes. > Type theory thinking can still be useful without the trappings of type > theory itself, and in fact type theory simulated in set theory has some > advantages over pure type theory in that you can bend the rules when it is > advantageous to do so. > And not everyone will like it. Should we say that there is only one single truth? > In lean, there is a concept called "defeq", or definitional equality, and > it is strictly stronger than regular equality: there are things that are > propositionally equal but not defeq, like x + (y + z) and (x + y) + z. You > can prove these two are equal, but if you have a type family indexed in > natural numbers and an element in F ((x + y) + z) you can't just treat it > as an element of F (x + (y + z)). In metamath you can; since the values are > equal the sets are equal so any element of one is also an element of the > other. Defeq is simply not a thing in metamath, and this is very freeing. > Ok. But this is starting to sound like a preaching :) And don't take me wrong. If you feel so strongly about this issue I won't continue to try to dissuade you. Probably this discussion already turned into bikeshedding and I should stop arguing and do something useful instead :) I'm sorry. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/14ce5c0a-44e9-4ee8-b6be-ac2d67848ac8n%40googlegroups.com.
