How to show in type theory (like in a proof assistant) that finite sets of different cardinalities are not isomorphic?

Question

Disclaimer: this question is not asking for code -- it's asking for a proof strategy.

For simplicity we may use Fin n (for the usual Fin type like in Idris/Agda) for finite sets. I'm wondering what the best practice is to show that for $n\ne m$, it holds that $\text{Fin}~n\not\simeq\text{Fin}~m$ (i.e. there isn't a bijection). I can guess a proof that starts with:

Suppose there is an isomorphism $\phi$. Also, w.l.o.g. we may assume $n<m$, then $\text{Fin}~m$ has more inhabitants.

Then, some distinct inhabitants of $\text{Fin}~m$ are sent to the same inhabitants of $\text{Fin}~n$, but how to show that?

In a math class, we draw pictures of sets and draw arrows to demonstrate the non-existence of bijections, but type theory wouldn't admit that.

Answer 1

This is called the Pigeonhole Principle. In a weak form it says that there is no injection from Fin (n+1) to Fin n. In a stronger form it says that if f : Fin m -> Fin n then there is some i : Fin n such that the fibre at i has cardinality at least m / n. The stronger form is perhaps more intuitive to prove but it requires more background machinery. For the weak form, proceed by induction on n : Nat to prove that for every f : Fin (n+1) -> Fin n there are i j : Fin (n+1) such that i < j and f i = f j.

The base case is trivial since Fin 1 is inhabited while Fin 0 is not.

For the induction step, given f : Fin (n+2) -> Fin (n+1). We may assume that f 0 = 0 otherwise compose with the involution that swaps 0 and f 0. Then consider these alternatives:

• If f (i+1) > 0 for every i : Fin (n+1) then we have a function f' : Fin (n+1) -> Fin n such that f (i+1) = (f' i) + 1 for all i : Fin (n+1). Apply the induction hypothesis to f' and conclude.
• Otherwise f (i+1) = 0 for some i : Fin (n+1). Since f 0 = 0 and 0 < i+1, we conclude immediately.

Answer 2

This is essentially the pigeonhole principle. If $m < n$, then $f : \mathsf{Fin}\ n → \mathsf{Fin}\ m$ takes two distinct values to the same value, meaning it cannot be an equivalence. This can then be used to prove that $\sf Fin$ is injective (simply by deciding trichotomy of $m$ and $n$; the above refutes the off-diagonal cases), which your proposition is the contrapositive of.

The linked proof is rather tricky, but that is mainly because the inductive step involves shrinking the function to a smaller example.