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

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).