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.


2 Answers 2


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.

  • $\begingroup$ Thanks very much for the link! $\endgroup$
    – ice1000
    Commented Jul 8, 2022 at 21:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.