Formalizing the theory of finite sets 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.