Pigeonhole principle

Baire.agda

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma

data ⊥ : Set where

¬_ : Set → Set
¬ P = P → ⊥

Surjective : {A B : Set} → (A → B) → Set
Surjective f = ∀ y → Σ _ λ x → f x ≡ y

Countable : Set → Set
Countable A = Σ (ℕ → A) Surjective

baire-uncountable : ¬(Countable (ℕ → ℕ))
baire-uncountable (f , sur) with sur λ n → suc (f n n)
baire-uncountable (f , sur) | x , fx≡ω = n≢sn (eqext fx≡ω x)
  where
    n≢sn : ∀{n} → ¬(n ≡ (suc n))
    n≢sn ()
    eqext : {A B : Set} {f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
    eqext refl x = refl

Decidable.agda

module Decidable where

open import Agda.Builtin.Equality public

data ⊥ : Set where

¬_ : (A : Set) → Set
¬ A = A → ⊥

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬(x ≡ y)

infix 0 ¬_
infix 1 _≢_

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

Pred : Set → Set₁
Pred A = A → Set

Decidable : {A : Set} → Pred A → Set
Decidable P = ∀ x → Dec (P x)

Decidable≡ : Set → Set
Decidable≡ A = (x y : A) → Dec (x ≡ y)

Finite.agda

open import Agda.Builtin.Sigma

open import Decidable
open import Func
open import Nat


≡sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
≡sym refl = refl

≡trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
≡trans refl x₂ = x₂

data Fin : ℕ → Set where
  fzero : ∀{n} → Fin (suc n)
  fsuc  : ∀{n} → Fin n → Fin (suc n)

--Drop : ∀{n} {A : Set} → (Fin (suc n) → A) → Fin n → A
--Drop f x = f (fsuc x)
--
--recur : ∀{n} {A : Set} → (f : Fin (suc n) → A) → (P : Pred A) → (∃ λ x → P (f x)) → ¬(P (f fzero)) → (∃ λ y → P (Drop f y))
--recur f P (fzero  , Pfx) ¬Pf0 = ⊥-elim (¬Pf0 Pfx)
--recur f P (fsuc x , Pfx) ¬Pf0 = x , Pfx

finEq : ∀{n} → Decidable≡ (Fin n)
finEq fzero fzero = yes refl
finEq fzero (fsuc y) = no (λ ())
finEq (fsuc x) fzero = no (λ ())
finEq (fsuc x) (fsuc y) with finEq x y
finEq (fsuc x) (fsuc .x) | yes refl = yes refl
finEq (fsuc x) (fsuc y) | no x₁ = no lemma
  where
    lemma : (x₂ : fsuc x ≡ fsuc y) → ⊥
    lemma refl = x₁ refl

data _≼_ : ∀{n m} → Fin n → Fin m → Set where
  0≼x   : ∀{n m} {x : Fin m}                     → fzero {n} ≼ x
  sx≼sy : ∀{n m} {x : Fin n} {y : Fin m} → x ≼ y → fsuc x    ≼ fsuc y

_≺_ : ∀{n m} → Fin n → Fin m → Set
x ≺ y = fsuc x ≼ y

≼refl : ∀{n} {x : Fin n} → x ≼ x
≼refl {.(suc _)} {fzero} = 0≼x
≼refl {.(suc _)} {fsuc x} = sx≼sy ≼refl

≺weaken : ∀{n m} {x : Fin n} {y : Fin m} → x ≺ y → x ≼ y
≺weaken {.(suc _)} {.(suc _)} {fzero} {.(fsuc _)} (sx≼sy x₁) = 0≼x
≺weaken {.(suc _)} {.(suc _)} {fsuc x} {.(fsuc _)} (sx≼sy x₁) = sx≼sy (≺weaken x₁)

≼drop : ∀{n m} {x : Fin n} {y : Fin m} → fsuc x ≼ fsuc y → x ≼ y
≼drop {n} {m} {x} {y} (sx≼sy x₁) = x₁

≼trans : ∀{k n m} {x : Fin k} {y : Fin n} {z : Fin m} → x ≼ y → y ≼ z → x ≼ z
≼trans {.(suc _)} {n} {m} {.fzero} {y} {z} 0≼x x₂ = 0≼x
≼trans {.(suc _)} {.(suc _)} {.(suc _)} {.(fsuc _)} {.(fsuc _)} {.(fsuc _)} (sx≼sy x₁) (sx≼sy x₂) = sx≼sy (≼trans x₁ x₂)

¬disorder : ∀{n m} {x : Fin n} {y : Fin m} → x ≺ y → ¬(y ≼ x)
¬disorder {_} {_} {fzero} {fzero} () y≼x
¬disorder {_} {_} {fzero} {fsuc y} x≺y ()
¬disorder {_} {_} {fsuc x} (sx≼sy x₁) (sx≼sy x₂) = ¬disorder x₁ x₂

¬wdisorder : ∀{n m} {x : Fin n} {y : Fin m} → x ≺ y → ¬(y ≺ x)
¬wdisorder (sx≼sy x) (sx≼sy x₁) = ¬wdisorder x x₁

_≈_ : ∀{n m} → Fin n → Fin m → Set
x ≈ y = (x ≼ y) × (y ≼ x)

≈eq : ∀{n} {x y : Fin n} → x ≈ y → x ≡ y
≈eq {.(suc _)} {fzero} {.fzero} (fst₁ , 0≼x) = refl
≈eq {.(suc _)} {fsuc x} {.(fsuc _)} (sx≼sy fst₁ , sx≼sy snd₁) with ≈eq (fst₁ , snd₁)
≈eq {.(suc _)} {fsuc x} {.(fsuc _)} (sx≼sy fst₁ , sx≼sy snd₁) | refl = refl

suc≈ : ∀{n m} {x : Fin n} {y : Fin m} → x ≈ y → fsuc x ≈ fsuc y
suc≈ {n} {m} {x} {y} (x≼y , y≼x) = sx≼sy x≼y , sx≼sy y≼x

≈sym : ∀{n m} {x : Fin n} {y : Fin m} → x ≈ y → y ≈ x
≈sym (fst₁ , snd₁) = snd₁ , fst₁

≈trans : ∀{k n m} {x : Fin k} {y : Fin n} {z : Fin m} → x ≈ y → y ≈ z → x ≈ z
≈trans {.(suc _)} {.(suc _)} {.(suc _)} {fzero} {.fzero} {.fzero} (fst₁ , 0≼x) (fst₂ , 0≼x) = 0≼x , 0≼x
≈trans {.(suc _)} {.(suc _)} {.(suc _)} {fsuc x} {.(fsuc _)} {.(fsuc _)} (sx≼sy fst₁ , sx≼sy snd₁) (sx≼sy fst₂ , sx≼sy snd₂) with ≈trans (fst₁ , snd₁) (fst₂ , snd₂)
≈trans {.(suc _)} {.(suc _)} {.(suc _)} {fsuc x} {.(fsuc _)} {.(fsuc _)} (sx≼sy fst₁ , sx≼sy snd₁) (sx≼sy fst₂ , sx≼sy snd₂) | fst₃ , snd₃ = sx≼sy fst₃ , sx≼sy snd₃

data Compare : ∀{n m} → Fin n → Fin m → Set where
  less : ∀{n m} {x : Fin n} {y : Fin m} → x ≺ y → Compare x y
  same : ∀{n m} {x : Fin n} {y : Fin m} → x ≈ y → Compare x y
  more : ∀{n m} {x : Fin n} {y : Fin m} → y ≺ x → Compare x y

compare : ∀{n m} → (x : Fin n) → (y : Fin m) → Compare x y
compare fzero fzero = same (0≼x , 0≼x)
compare fzero (fsuc y) = less (sx≼sy 0≼x)
compare (fsuc x) fzero = more (sx≼sy 0≼x)
compare (fsuc x) (fsuc y) with compare x y
compare (fsuc x) (fsuc y) | less x≺y = less (sx≼sy x≺y)
compare (fsuc x) (fsuc y) | same (x≼y , y≼x) = same (sx≼sy x≼y , sx≼sy y≼x)
compare (fsuc x) (fsuc y) | more y≺x = more (sx≼sy y≺x)

drop : ∀{n} {y : Fin (suc n)} → (x : Fin (suc n)) → x ≺ y → Σ (Fin n) λ z → x ≈ z
drop {zero} {fsuc ()} x (sx≼sy x≺y)
drop {suc n} fzero    (sx≼sy x≺y) = fzero , 0≼x , 0≼x
drop {suc n} (fsuc x) (sx≼sy x≺y) with drop x x≺y
drop {suc n} (fsuc x) (sx≼sy x≺y) | z , x≼z , z≼x = fsuc z , sx≼sy x≼z , sx≼sy z≼x

dropeq : ∀{n} {x y x′ y′ : Fin (suc n)} {x≺y : x ≺ y} {x′≺y′ : x′ ≺ y′} → fst (drop x x≺y) ≡ fst (drop x′ x′≺y′) → x ≡ x′
dropeq {n} {x} {y} {x′} {y′} {x≺y} {x′≺y′} x₁ with drop x x≺y | drop x′ x′≺y′
dropeq {n} {x} {y} {x′} {y′} {x≺y} {x′≺y′} refl | z , x≈z | .z , x′≈z = ≈eq (≈trans x≈z (≈sym x′≈z))

lift : ∀{n} → (x : Fin n) → Σ (Fin (suc n)) λ z → x ≈ z
lift fzero = fzero , 0≼x , 0≼x
lift (fsuc x) with lift x
lift (fsuc x) | y , y≼x , x≼y = fsuc y , sx≼sy y≼x , sx≼sy x≼y

lifteq : ∀{n} {x y : Fin n} → fst (lift x) ≡ fst (lift y) → x ≡ y
lifteq {n} {x} {y} x₁ with lift x | lift y
lifteq {.(suc _)} {fzero} {fzero} refl | fst₁ , c | .fst₁ , d = refl
lifteq {.(suc _)} {fzero} {fsuc y} refl | .fzero , 0≼x , 0≼x | .fzero , () , snd₁
lifteq {.(suc _)} {fsuc x} {fzero} refl | .(fsuc _) , sx≼sy fst₂ , sx≼sy snd₁ | .(fsuc _) , 0≼x , ()
lifteq {.(suc _)} {fsuc x} {fsuc y} refl | fzero , () , snd₁ | .fzero , fst₂ , snd₂
lifteq {suc n} {fsuc x} {fsuc y} refl | fsuc fst₁ , sx≼sy fst₂ , sx≼sy snd₁ | .(fsuc fst₁) , sx≼sy fst₃ , sx≼sy snd₂ with ≈trans (fst₂ , snd₁) (snd₂ , fst₃)
lifteq {suc n} {fsuc x} {fsuc y} refl | fsuc fst₁ , sx≼sy fst₂ , sx≼sy snd₁ | .(fsuc fst₁) , sx≼sy fst₃ , sx≼sy snd₂ | fst₄ , snd₃ = ≈eq (sx≼sy fst₄ , sx≼sy snd₃)

fprec : ∀{n m} {y : Fin m} → (x : Fin (suc n)) → y ≺ x → Σ (Fin n) (λ z → fsuc z ≡ x)
fprec (fsuc x) (sx≼sy y≺x) = x , refl

fpreceq : ∀{n m} {x x′ : Fin (suc n)} {y y′ : Fin m} → (y≺x : y ≺ x) → (y′≺x′ : y′ ≺ x′) → fst (fprec x y≺x) ≡ fst (fprec x′ y′≺x′) → x ≡ x′
fpreceq {n} {m} {x} {x′} {y} {y′} y≺x y′≺x′ x₁ with fprec x y≺x | fprec x′ y′≺x′
fpreceq {n} {m} {x} {x′} {y} {y′} y≺x y′≺x′ refl | z , sz≡x | .z , sz≡x′ = ≡trans (≡sym sz≡x) sz≡x′

fprecsuc : ∀{n m} {z : Fin m} → (x : Fin n) → (lt : z ≺ fsuc x) →  x ≈ fst (fprec (fsuc x) lt)
fprecsuc x lt with fprec (fsuc x) lt
fprecsuc x lt | .x , refl = ≼refl , ≼refl


--dropprec : ∀{n m} {x a : Fin (suc n)} {y : Fin (suc n)} {b : Fin m} {x≺a : x ≺ a} {b≺y : b ≺ y} → fst (drop x x≺a) ≡ fst (fprec y b≺y) → (fsuc x) ≈ y
--dropprec {n} {m} {x} {a} {y} {b} {x≺a} {b≺y} eq with drop x x≺a | fprec y b≺y
--dropprec {n} {m} {x} {a} {.(fsuc z)} {b} {x≺a} {b≺y} refl | z , x≈z | .z , refl = suc≈ x≈z

dropprec : ∀{n m} {x a : Fin (suc n)} {y : Fin (suc n)} {b : Fin m} → (x≺a : x ≺ a) → (b≺y : b ≺ y) → fst (drop x x≺a) ≡ fst (fprec y b≺y) → (fsuc x) ≈ y
dropprec x≺a b≺y eq with drop _ x≺a | fprec _ b≺y
dropprec x≺a b≺y refl | z , x≈z | .z , refl = suc≈ x≈z

Func.agda

open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

open import Decidable

∃_ : {A : Set} → (A → Set) → Set
∃_ {A} f = Σ A f

∃₂_ : {A B : Set} → (A → B → Set) → Set
∃₂_ {A} {B} f = Σ A λ x → Σ B λ y → f x y

_×_ : Set → Set → Set
A × B = Σ A λ _ → B

data _⊎_ (A B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

Inj : {A B : Set} → (A → B) → Set
Inj f = ∀ x y → f x ≡ f y → x ≡ y

Sur : {A B : Set} → (A → B) → Set
Sur f = ∀ y → ∃ λ x → f x ≡ y

SingPoint : {A B : Set} → (A → B) → A → Set
SingPoint f x = ∃ λ y → (x ≢ y) × (f x ≡ f y)

Sing : {A B : Set} → (A → B) → Set
Sing f = ∃ SingPoint f

Sing→¬Inj : {A B : Set} {f : A → B} → Sing f → ¬(Inj f)
Sing→¬Inj {A} {B} {f} (x , y , x≢y , fx≡fy) inj = x≢y (inj x y fx≡fy)


module _ where
  open import Agda.Builtin.Nat renaming (Nat to ℕ)

  eqext : {A B : Set} {f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
  eqext refl x = refl

  diag : (ℕ → ℕ → ℕ) → ℕ → ℕ
  diag f x = suc (f x x)

  cantor : (f : ℕ → ℕ → ℕ) → ¬(Sur f)
  cantor f sur with sur (diag f)
  cantor f sur | x , fx≡ω = n≢sn (eqext fx≡ω x)
    where
      n≢sn : ∀{n} → n ≢ (suc n)
      n≢sn ()

Nat.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_<_) public

data _≤_ : ℕ → ℕ → Set where
  0≤n    : ∀{n} → zero ≤ n
  sn≤sm : ∀{n m} → n ≤ m → (suc n) ≤ (suc m)

_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m

Pigeon.agda

open import Agda.Builtin.Sigma

open import Decidable
open import Finite
open import Func
open import Nat

dropfunc : ∀{n m} → (f : Fin (suc n) → Fin (suc m)) → ¬(SingPoint f fzero) → Fin n → Fin m
dropfunc f ¬0sing x with compare (f (fsuc x)) (f fzero)
dropfunc f ¬0sing x | less lt    = fst (drop (f (fsuc x)) lt)
dropfunc f ¬0sing x | same (le , ge) = ⊥-elim (¬0sing (fsuc x , (λ ()) , sameeq ge le))
                                       where
                                          sameeq : ∀{n} {x y : Fin n} → x ≼ y → y ≼ x → x ≡ y
                                          sameeq 0≼x 0≼x = refl
                                          sameeq (sx≼sy x≼y) (sx≼sy y≼x) with sameeq x≼y y≼x
                                          sameeq (sx≼sy x≼y) (sx≼sy y≼x) | refl = refl
dropfunc f ¬0sing x | more gt    = fst (fprec (f (fsuc x)) gt)

pagr : ∀{n m} (f : Fin (suc n) → Fin (suc m)) → (¬0sing : ¬(SingPoint f fzero)) → (x : Fin n) → f (fsuc x) ≺ f fzero → f (fsuc x) ≈ dropfunc f ¬0sing x
pagr f ¬0sing x lt with compare (f (fsuc x)) (f fzero)
pagr f ¬0sing x lt | less x₁ = snd (drop (f (fsuc x)) x₁)
pagr f ¬0sing x lt | same (fst₁ , snd₁) = ⊥-elim (¬disorder lt snd₁)
pagr f ¬0sing x lt | more x₁ = ⊥-elim (¬wdisorder lt x₁)

pmv : ∀{n m} (f : Fin (suc n) → Fin (suc m)) → (¬0sing : ¬(SingPoint f fzero)) → (x : Fin n) → (lt : f fzero ≺ f (fsuc x)) → dropfunc f ¬0sing x ≈ fst (fprec (f (fsuc x)) lt)
pmv f ¬0sing x lt with compare (f (fsuc x)) (f fzero)
pmv f ¬0sing x lt | less x₁ = ⊥-elim (¬wdisorder lt x₁)
pmv f ¬0sing x lt | same (fst₁ , snd₁) = ⊥-elim (¬disorder lt fst₁)
pmv f ¬0sing x lt | more x₁ with snd (fprec (f (fsuc x)) lt)
pmv f ¬0sing x lt | more x₁ | eq = lemma lt (snd (fprec (f (fsuc x)) x₁))
  where
    lemma : ∀{n} {x : Fin n} {y z : Fin (suc n)} → (lt : z ≺ y) → fsuc x ≡ y → x ≈ fst (fprec y lt)
    lemma lt₁ refl = fprecsuc _ lt₁


codomainHas : ∀{n} {A : Set} → Decidable≡ A → (f : Fin n → A) → (y : A) → Dec (Σ _ (λ x → y ≡ f x))
codomainHas {zero} eq f y = no λ x → lemma (fst x)
  where
    lemma : ¬(Fin 0)
    lemma ()
codomainHas {suc n} eq f y with eq y (f fzero)
codomainHas {suc n} eq f y | yes found = yes (fzero , found)
codomainHas {suc n} eq f y | no ¬found with codomainHas eq (λ x → f (fsuc x)) y
codomainHas {suc n} eq f y | no ¬found | yes (fst₁ , snd₁) = yes (fsuc fst₁ , snd₁)
codomainHas {suc n} eq f y | no ¬found | no ¬rest = no lemma
  where
    lemma : ¬(Σ (Fin (suc n)) (λ z → y ≡ f z))
    lemma (fzero , snd₁) = ¬found snd₁
    lemma (fsuc x , snd₁) = ¬rest (x , snd₁)


isZeroSingPoint : ∀{n} {A : Set} → Decidable≡ A → (f : Fin (suc n) → A) → Dec (SingPoint f fzero)
isZeroSingPoint {zero} eq f = no lemma
  where
    lemma : (x  : Σ (Fin 1) (λ z → Σ ((x₁ : fzero ≡ z) → ⊥) (λ _ → f fzero ≡ f z))) → ⊥
    lemma (fzero , fst₁ , snd₁) = fst₁ refl
    lemma (fsuc () , x)
isZeroSingPoint {suc n} eq f with codomainHas eq (λ x → f (fsuc x)) (f fzero)
isZeroSingPoint {suc n} eq f | yes (fst₁ , snd₁) = yes (fsuc fst₁ , (λ ()) , snd₁)
isZeroSingPoint {suc n} eq f | no x = no lemma
  where
    lemma : ¬(Σ (Fin (suc (suc n))) (λ z → Σ (fzero ≢ z) (λ _ → f fzero ≡ f z)))
    lemma (fzero , fst₂ , snd₁) = fst₂ refl
    lemma (fsuc fst₁ , fst₂ , snd₁) = x (fst₁ , snd₁)

pigeon : ∀{n m} → m < n → (f : Fin n → Fin m) → Sing f
pigeon {suc _} {zero}  (sn≤sm m<n) f with f fzero
pigeon {suc _} {zero}  (sn≤sm m<n) f | ()
pigeon {suc n} {suc m} (sn≤sm m<n) f with isZeroSingPoint finEq f
pigeon {suc n} {suc m} (sn≤sm m<n) f | yes 0sing = fzero , 0sing
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing with pigeon m<n (dropfunc f ¬0sing)
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy with compare (f (fsuc x)) (f fzero) | compare (f (fsuc y)) (f fzero)
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy | less x₁ | less x₂ = fsuc x , fsuc y , sx≢sy , fsx≡fsy
  where
    sx≢sy : fsuc x ≢ fsuc y
    sx≢sy refl = x≢y refl
    fsx≡fsy : f (fsuc x) ≡ f (fsuc y)
    fsx≡fsy = dropeq gx≡gy
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy | less x₁ | same x₂ = ⊥-elim (¬0sing (fsuc y , (λ ()) , ≡sym (≈eq x₂)))
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy | less fsx≺f0 | more f0≺fsy = ⊥-elim lemma₃
  where
    lemma₁ : ∀{n m} {x : Fin n} {y : Fin m} → x ≺ y → ¬(y ≺ fsuc x)
    lemma₁ {n} {m} {x} {y} sx≼y y≺sx = ¬disorder sx≼y (≼drop y≺sx)
    lemma₂ : ∀{k n m} {x : Fin k} {y : Fin n} {z : Fin m} → x ≺ y → y ≺ z → z ≼ fsuc x → ⊥
    lemma₂ {k} {n} {m} {x} {y} {z} sx≼y sy≼z z≼sx = lemma₁ sx≼y (≼drop (sx≼sy (≼trans sy≼z z≼sx)))
    lemma₃ : ⊥
    lemma₃ with dropprec fsx≺f0 f0≺fsy gx≡gy
    lemma₃ | sX≼Y , Y≼sX = lemma₂ fsx≺f0 f0≺fsy Y≼sX
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy | same x₁ | less x₂ = ⊥-elim (¬0sing (fsuc x , (λ ()) , ≡sym (≈eq x₁)))
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy | same x₁ | same x₂ = ⊥-elim (¬0sing (fsuc x , (λ ()) , ≡sym (≈eq x₁)))
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy | same x₁ | more x₂ = ⊥-elim (¬0sing (fsuc x , (λ ()) , ≡sym (≈eq x₁)))
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy | more f0≺fsx | less fsy≺f0 = ⊥-elim lemma₃
  where
    lemma₁ : ∀{n m} {x : Fin n} {y : Fin m} → x ≺ y → ¬(y ≺ fsuc x)
    lemma₁ {n} {m} {x} {y} sx≼y y≺sx = ¬disorder sx≼y (≼drop y≺sx)
    lemma₂ : ∀{k n m} {x : Fin k} {y : Fin n} {z : Fin m} → x ≺ y → y ≺ z → z ≼ fsuc x → ⊥
    lemma₂ {k} {n} {m} {x} {y} {z} sx≼y sy≼z z≼sx = lemma₁ sx≼y (≼drop (sx≼sy (≼trans sy≼z z≼sx)))
    lemma₃ : ⊥
    lemma₃ with dropprec fsy≺f0 f0≺fsx (≡sym gx≡gy)
    lemma₃ | fsy≺fsx , fsx≼sfsy = lemma₂ fsy≺f0 f0≺fsx fsx≼sfsy
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy | more x₁ | same x₂ = ⊥-elim (¬0sing (fsuc y , (λ ()) , ≡sym (≈eq x₂)))
pigeon {suc n} {suc m} (sn≤sm m<n) f | no ¬0sing | x , y , x≢y , gx≡gy | more x₁ | more x₂ = fsuc x , fsuc y , sx≢sy , fsx≡fsy
  where
    sx≢sy : fsuc x ≢ fsuc y
    sx≢sy refl = x≢y refl
    fsx≡fsy : f (fsuc x) ≡ f (fsuc y)
    fsx≡fsy = fpreceq x₁ x₂ gx≡gy

test.agda

open import Agda.Builtin.Sigma

open import Finite
open import Func
open import Nat
open import Pigeon

f : Fin 5 → Fin 4
f fzero                                 = fsuc (fsuc fzero)
f (fsuc fzero)                          = fzero
f (fsuc (fsuc fzero))                   = fsuc (fsuc (fsuc fzero))
f (fsuc (fsuc (fsuc fzero)))            = fsuc fzero
f (fsuc (fsuc (fsuc (fsuc fzero))))     = fsuc (fsuc (fsuc fzero))
f (fsuc (fsuc (fsuc (fsuc (fsuc ())))))

fsing : Sing f
fsing = pigeon (sn≤sm (sn≤sm (sn≤sm (sn≤sm (sn≤sm 0≤n))))) f

singularity : Fin 5 × Fin 5
singularity = fst fsing , fst (snd fsing)