Formalizing the theory of finite sets in type theory Most proof assistants have a formalization of the concept of "finite set".  These formalizations, however, differ wildly (although one hopes that they are all essentially equivalent!).  What I don't understand at this point is the design space involved, and what are the pros and cons of each formalization.

In particular, I would like to understand the following:


Can I axiomatize finite sets (i.e. types inhabited by a finite number of inhabitants) in simple type theory?  System F?  What are the drawbacks of doing it this way?
I know it can be done 'elegantly' in a dependently typed system.  But, from a classical point of view, the resulting definitions seem extremely alien.  [I am not saying they are wrong, far from it!].  But I do not understand why they are 'right' either.  I understand that they pick out the correct concept, but the deeper reason for 'saying it that way' is what I do not fully grasp.


Basically, I would like a reasoned introduction to the design space of formalizations of the concept of 'finite set' in type theory.
I know it can be done 'elegantly' in a dependently typed system. But, from a classical point of view, the resulting definitions seem extremely alien.


Can you explain what you mean by "alien"? It seems to me that you
formalize the concept of finite set in precisely the same way in 
type theory and in set theory. 

In set theory, you proceed by defining the set $Fin(n)$ as 
$$
  \mathrm{Fin}(n) \triangleq \{ k \in \mathbb{N} \;|\; k &lt; n \}
$$
Then, you define the finiteness predicate as:
$$
  \mathrm{Finite}(X) \triangleq \exists n\in\mathbb{N}.\; X \simeq \mathrm{Fin}(n)
$$
Where $A \simeq B$ means isomorphism of sets. 

In type theory, you can do exactly the same thing! 
$$
  \mathrm{Fin}(n) \triangleq \Sigma k:\mathbb{N}.\; \mathsf{if}\; k &lt; n\,\mathsf{then}\; \mathsf{Unit} \;\mathsf{else}\; \mathsf{Void}
$$
Note that $\mathrm{Fin}(n)$ is a type with $n$ elements (since the second component of the pair is
proof-irrelevant). Then, you can define the finiteness type constructor as:
$$
  \mathrm{Finite}(X) \triangleq \Sigma n:\mathbb{N}.\; X \simeq \mathrm{Fin}(n)
$$
Where $A \simeq B$ means isomorphism of types.