\import Arith.Nat
\import Data.Array
\import Function
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Paths
\import Set
\import Set.Fin
\import Set.Fin.Pigeonhole

\class KFinSet \extends BoundedPigeonholeSet
  | finSurj : ∃ (f : Fin finCard -> E) (isSurj f)
  | boundedPigeonhole => \case finSurj \with {
    | inP (f,s) => boundedPigeonhole {pigeonhole-surj (\new BoundedPigeonholeSet (Fin finCard) finCard (pigeonhole-fin __ id<suc)) f s}
  }
  \where {
    \lemma fromArray {A : \Set} (l : Array A) (p : \Pi (a : A) -> ∃ (i : Fin l.len) (l i = a)) : KFinSet A l.len \cowith
      | finSurj => inP (l,p)

    \lemma toArray (A : KFinSet) : ∃ (l : Array A) (\Pi (a : A) -> ∃ (i : Fin l.len) (l i = a))
      => TruncP.map A.finSurj $ \lam (f,p) => (f,p)

    \lemma KFin+Dec=>Fin (A : KFinSet) {d : DecSet A} : FinSet A
      => \case toArray A \with {
        | inP (l,q) =>
          \let l' => nub l
          \in FinSet.fromArray l' (\lam a => TruncP.map (q a) $ \lam p =>
              \let t => nub-isSurj l p.
              \in (t., t. *> p.)) nub-isInj
      }
  }