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

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, 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.

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.

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.

• Thanks very much for the link! Jul 8, 2022 at 21:23