proof of absence of infinity

noInfinity.idr

module noInfinity

%default total

data T2 = Mk1 | Mk2

Mk1neqMk2 : Not (Mk1 = Mk2)
Mk1neqMk2 Refl impossible

Mk2neqMk1 : Not (Mk2 = Mk1)
Mk2neqMk1 Refl impossible

fix : (x->x) -> (x->Type)
fix f x = x = f x

swap2 : T2 -> T2
swap2 Mk1 = Mk2
swap2 Mk2 = Mk1

okSwap2 : Not (fix swap2 t)
okSwap2 {t=Mk1} = Mk1neqMk2
okSwap2 {t=Mk2} = Mk2neqMk1

iter : Nat -> (x->x) -> (x->x)
iter Z f = id
iter (S n) f = f . (iter n f)

infixl 5 $:, :$

($:) : (f0: x->y) -> (x1=x2) -> (f0 x1 = f0 x2)
($:) f0 Refl = Refl

(:$) : (f1=f2) -> (x0: x) -> (f1 x0 = f2 x0)
(:$) Refl x0 = Refl

noFix : Not (fix S inf)
noFix eq = okSwap2 (iter $: eq :$ swap2 :$ Mk1)

Infinity : Type
Infinity = Sigma Nat (fix S)

noInfinity : Not Infinity
noInfinity I = noFix (getProof I)