> In traditional mathematics equality is treated as a relation. Two things are either equal or not.
That sounds like the way to go. No (identity) types needed.
lmm53 minutes ago
The problem is that you have model everything in a lossy way to make that work. If you want to say that 2 green apples plus 2 red apples equals 4 apples, you have to just say that you have 2 apples plus 2 apples, and you can't then go back and ask what colour your apples are. Whereas in homotopy type theory you can say a red apple is equivalent to a green apple, and that equivalence is a mathematical object you can manipulate in nice ways, but if you ever need to go back and work with the colour again it's still there.
kazinator3 hours ago
But can you escape from that relation being identifiable as having a type or being a type, even if you don't find it interesting/helpful and don't use it?
Also the concept of a proof of equality strikes as relevant, because some equalities are actually incomputable. E.g. suppose you want a an equality type for whether two functions are equivalent (two instances of the same function type).
drumnerd3 hours ago
In type checking, particularly in dependent types, it is not trivial to check that two types are the same. Different notions of equality are useful in this field. A type can contain a function value inside. How to prove that two functions are the same? Is not enough to prove that for all X f X and g X implies f is g.
> In traditional mathematics equality is treated as a relation. Two things are either equal or not.
That sounds like the way to go. No (identity) types needed.
The problem is that you have model everything in a lossy way to make that work. If you want to say that 2 green apples plus 2 red apples equals 4 apples, you have to just say that you have 2 apples plus 2 apples, and you can't then go back and ask what colour your apples are. Whereas in homotopy type theory you can say a red apple is equivalent to a green apple, and that equivalence is a mathematical object you can manipulate in nice ways, but if you ever need to go back and work with the colour again it's still there.
But can you escape from that relation being identifiable as having a type or being a type, even if you don't find it interesting/helpful and don't use it?
Also the concept of a proof of equality strikes as relevant, because some equalities are actually incomputable. E.g. suppose you want a an equality type for whether two functions are equivalent (two instances of the same function type).
In type checking, particularly in dependent types, it is not trivial to check that two types are the same. Different notions of equality are useful in this field. A type can contain a function value inside. How to prove that two functions are the same? Is not enough to prove that for all X f X and g X implies f is g.
Post from yesterday (with very little discussion): https://news.ycombinator.com/item?id=45333548