On Sun, Feb 6, 2022 at 8:44 AM vvs <[email protected]> wrote: > That's nonsense, this should be easy to do. :) The equivalent of a type >> with a parameter in set.mm is a function from sets to sets. You use >> function application to represent the application of the type function to >> some particular type. >> > > Very well, then. > > Also, maybe I was looking in the wrong direction and this isn't relevant > here, but function is still just an approximation and it is not a type, > right? I mean, in case where you really want it to be different from set? > Then it would be not enough to just define a function and you will need > several theorems to prove that. And if you will use it too often then it > might become annoying. >
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. -- 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/CAFXXJSs8QZ-PCZei1oumxX6Y206fY2ZsJe71nZOR4OO9t0eSSA%40mail.gmail.com.
