| >Sure, whatever - the point is that they're different objects, and results about one are not results about the other. Sorry, I don't understand what you mean by "same" and "different". By "same" do you mean =(x,y).
And by "different" do you mean ¬=(x,y) Or do you mean something like same(x,y) = { 1 if ??? else 0 } >A classical function X -> Y is a relation such that if `(x, y1)` and `(x, y2)` hold then `y1 = y2 You seem to be confusing syntax and semantics here, and the infix notation isn't helping... What does =(y1, y2) mean?
What does =(x,x) mean? >No such thing: it's a metatheoretical judgement, not a theorem. What do you mean? Judgments are first-class citizens in Univalent Mathematics. a:R is a judgment that object a is of type R. This literally means "a proves R", and the particular expression "first class citizen" has well-understood meaning in Programming Language design ( https://en.wikipedia.org/wiki/First-class_citizen ). >`stringToUpperCase (5 :: Int) :: String` isn't a false statement, it's just inexpressible nonsense. So I must be a miracle worker then? Expressing the inexpressible nonsense... In [1]: def stringToUpperCase(x): return(str(x).upper())
In [2]: stringToUpperCase(int(5))
Out[2]: '5'
>No. Self-information of a given outcome with respect to a random variable, which is probably the most common sense of the word.Speaking of randomness in a classical setting, this function exists, right? f(x) = { 1 if random(x), else 0 } |