We shall build this argument from a lemma about injections on standard finite types,
Thm* (f:(mk). Inj(m; k; f)) mk,
and exploiting the connection between
Assume a class has size
Each direction of the equality, namely,
may be proved in the same way, so we generalize the goal slightly to
x,y:. (x ~ y) xy.
Once this is proved,
Thm* EquivRel X,Y:Type. X ~ Y.
So, it is enough to show that
The connection between
Thm* (f:(AB). Bij(A; B; f)) (A ~ B).
And since being an injection is part of being a bijection, i.e.,
Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f),
Thm* (f:(mk). Inj(m; k; f)) mk.
A corrolary is
Thm* a,b:. (a ~ b) a = b.