Thanks, Thierry, Mario and Alex, I will follow your advice, and take the exercise. :-)
The community is so friendly! I will ask if I am blocked. Mingli On Mon, Feb 7, 2022 at 8:00 AM vvs <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/14ce5c0a-44e9-4ee8-b6be-ac2d67848ac8n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAGDRuAjit9eJhHeBkVAp4ckWHvEeGkDy4G10NtZb3FRJEzGYdA%40mail.gmail.com.
