Why do term equalities have a type annotation?

[andrejbauer]

It seems like we have an antisymmetry in how we treat terms vs. term equations. A term judgement does not have a type annotation. Thus, if we ask for its boundary (the type of the term), we either get the natural type of the term, or the type given to it by a conversion (because internally we record such conversions).

In contrast, a type equality always has a type associated with it, i.e., we have to write a == b : A, not just a == b. Other than for the purposes of easier parsing (being able to tell type equalities from term equalities), there seems to be little reason to do so. It would make equally good sense to have just a == b and keep a record of the conversions of term equalities, like we do for term judgement.