cosmologicon / pywat

Python wats
1.22k stars 99 forks source link

"It just happens to work out that the truth table is the same as for the converse implication operator." #31

Open PhantomHoover opened 7 years ago

PhantomHoover commented 7 years ago

This is not, in fact, an arbitrary coincidence; it follows naturally. If A and B are (finite) sets/types then the cardinality of the set/type of functions from A to B is |B|^|A|. If you use the Curry-Howard isomorphism and identify True and False as the unit and empty type respectively, then the function type A -> B is identified with logical implication, and we obtain the result from the original post.