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:(mk). Inj(mkf))  mk,

and exploiting the connection between X ~ Y and injections, and the connection between xy 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,

mk and km,

may be proved in the same way, so we generalize the goal slightly to

x,y:. (x ~ y xy.

Once this is proved, mk and km 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 xy, assuming that x ~ y.
The connection between X ~ Y and bijection is established by

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

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

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

xy follows from the lemma

Thm*  (f:(mk). Inj(mkf))  mk.

QED

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

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