> 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? -- 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/568c0211-878d-447e-af94-f80f72de215cn%40googlegroups.com.
