On Sun, Feb 6, 2022 at 11:11 AM vvs <[email protected]> wrote: > There isn't really any essential way that a type is different from a set, >> except that a type abstracts some encoding details that sets instantiate in >> a particular way. That means that if you have a type you want to model then >> sets are a way to do it, maybe not the only way. Of course the function >> giving the type family is only the beginning of the story: in haskell an >> inductive data type comes with constructors and pattern matching, and that >> corresponds to functions and a recursion principle in metamath. >> > > I'm thinking more about elements that may belong to many sets, while they > can have only one type. Isn't that the main reason why type theory was > invented in the first place? Yes, it's possible to use set theory with > particular axioms like ZFC, but trying to model type theory inside it kinda > defeats the purpose. Why not implement type theory in Metamath then? >
Two things: (1) it's been done, see hol.mm or dtt.mm. (2) It's not necessary; type theory can be simulated in set.mm without straying very far from idiomatic style, and without a lot of overhead, so it amounts to a particular way of handling propositions in ZFC. I don't see why you are so eager to say "types are not quite sets" and therefore you may as well throw away the library and get another one if you want to use type-based reasoning. 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. 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. -- 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/CAFXXJSvnyudzewe81Fh%3DkSBQx%3DR_QcDZrb%2Bew-4_4ChR3z_vpw%40mail.gmail.com.
