A big topic in type theory nowadays is equational reasoning. The classic example is, how can you prove that two functions are observationally equivalent -- that they give the same output for all inputs? Bob discusses that in his book.
More generally, you can discuss various other notions of equivalence, both for functions and (in this case) types. So if we do allow a programmer to define their own notions of equivalence, is that good enough? Not quite -- it can be difficult to propagate this notion through to derivative constructs. You'd like for there to be a way to get all sorts of "free" theorems basically. So I think that is what this blog post is beginning to talk about, in somewhat technical terms.
More generally, you can discuss various other notions of equivalence, both for functions and (in this case) types. So if we do allow a programmer to define their own notions of equivalence, is that good enough? Not quite -- it can be difficult to propagate this notion through to derivative constructs. You'd like for there to be a way to get all sorts of "free" theorems basically. So I think that is what this blog post is beginning to talk about, in somewhat technical terms.