BoundedPigeonhole

\import Arith.Fin.Order
\import Data.Fin
\import Function
\import Logic
\import Logic.Bar
\import Logic.Meta
\import Order.LinearOrder
\import Order.StrictOrder
\import Paths
\import Set.Fin (FinSet)
\import Set.Fin.Noetherian
\import Set.Fin.Pigeonhole

\class BoundedPigeonholeSet \extends NoetherianSet {
  | card : Nat
  | boundedPigeonhole (f : Fin (suc card) -> E) : ∃ (i j : Fin (suc card)) (i /= j) (f i = f j)
  | isNoetherianSet => bounded-bar (suc card) \lam l => boundedPigeonhole l

  \lemma boundedPigeonhole< (f : Fin (suc card) -> E) : ∃ (i j : Fin (suc card)) (i < j) (f i = f j)
    => TruncP.map (boundedPigeonhole f) \lam t => \case LinearOrder.trichotomy t.1 t.2 \with {
      | less c => (t.1, t.2, c, t.4)
      | equals c => absurd (t.3 c)
      | greater c => (t.2, t.1, c, inv t.4)
    }
}

\lemma pigeonhole-surj (A : BoundedPigeonholeSet) {B : \Set} (f : A -> B) (s : IsSurj f) : BoundedPigeonholeSet B A.card \cowith
  | boundedPigeonhole g =>
    \have | (inP t) => FinSet.finiteAC (\lam j => s (g j))
          | (inP r) => A.boundedPigeonhole (\lam j => (t j).1)
    \in inP (r.1, r.2, r.3, inv (t r.1).2 *> pmap f r.4 *> (t r.2).2)