What is type theory, and why it matters
Ref:
- Girard
- It is an abuse (and this is not cheap philosophy --- it is a concrete question) to say that \(27\times37\) equals 999, since if the two things we have were the same then we would never feel the need to state their equality.