\import Equiv
\import Function
\import Function.Meta
\import Logic
\import Paths
\import Set.Fin.Pigeonhole

\type isDFin (A : \Set) : \Prop
  => \Pi (f : A -> A) -> isInj f -> isSurj f
  \where {
    \lemma isEquiv {A : \Set} (p : isDFin A) (f : A -> A) (inj : isInj f) : Equiv f
      => Equiv.fromInjSurj f inj (p f inj)

    \func isSplit {A : \Set} (p : isDFin A) (f : A -> A) (inj : isInj f) (a : A) : \Sigma (a' : A) (f a' = a)
      => (ret {isEquiv p f inj} a, Equiv.f_ret a)

    \lemma fromPigeonhole (A : PigeonholeSet) : isDFin A
      => \lam f inj a => TruncP.map (A.pigeonhole< (\lam i => iterr f i a))
          \lam t => (_, inv $ iterr_inj f inj a t. t. t. t.)
  }