IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

### Proof that Counting is Unique

Show Thm*  (A ~ m  (A ~ k  m = k.

We shall build this argument from a lemma about injections on standard finite types,

Thm*  ( f:( m   k). Inj( m kf))  m k,

and exploiting the connection between X ~ Y and injections, and the connection between x y and equality.

Assume a class has size m, but also has size k;
show m must actually be k.
Each direction of the equality, namely,

m k and k m,

may be proved in the same way, so we generalize the goal slightly to x,y: . ( x ~ y  x y.

Once this is proved, m k and k m follow easily from it since m ~ k and k ~ m follow easily from our assumptions and the fact that X ~ Y is an equivalence relation, i.e.,

Thm*  EquivRel X,Y:Type. X ~ Y.

So, it is enough to show that x y, assuming that x ~ y.
The connection between X ~ Y and bijection is established by

Thm*  ( f:(A  B). Bij(ABf))  (A ~ B).

And since being an injection is part of being a bijection, i.e.,

Def  Bij(ABf) == Inj(ABf) & Surj(ABf),

x y follows from the lemma

Thm*  ( f:( m   k). Inj( m kf))  m k.

QED

A corrolary is Thm* a,b: . ( a ~ b  a = b.