I have read this some years ago. I really enjoyed diving into this subject. My favourite part is: > Common wisdom tells us that function types don’t have decid

I have read this some years ago. I really enjoyed diving into this subject. My favourite part is: > Common wisdom tells us that function types don’t have decidable equality. In fact, e.g. the function type Integer -> Integer doesn’t have decidable equality because of the Halting Problem, as is well known. However, common wisdom is not always correct, and, in fact, some other function types do have decidable equality, for example the type Cantor -> y for any type y with decidable equality, without contradicting Turing [...] This seems strange, even fishy, because the Cantor space is in some sense bigger than the integers. In a follow-up post, I’ll explain that this has to do with the fact that the Cantor space is topologically compact, but the integers are not.