When I started studying dependent types a few years ago, one question I never got a good answer to was: why is equality such a big deal? Equality types are, of course, practically important. They're practically important because we want to prove stuff equal to other stuff a lot! But why does adding equality types necessitate so much deep theory about how a dependent type system works?1 [1 After all, integers, also a complicated concept, can be added cleanly and independently, even though indu...
