> 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. -- 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/ff8cbe98-31a5-4068-8c2c-f6fa98c25993n%40googlegroups.com.
