Fully typed arithmetics with TypeScript 😨

peano.ts

type Nat = ["S", Nat] | ["Z"];

type Succ<N extends Nat> = ["S", N]
type S<N extends Nat> = Succ<N>
type Prev<N extends Nat> = N[1]

type Z     = ["Z"]
type Zero  = Z
type One   = S<Z>
type Two   = S<S<Z>>
type Three = S<S<S<Z>>>
type Four  = S<S<S<S<Z>>>>
type Five  = S<S<S<S<S<Z>>>>>
type Six   = S<S<S<S<S<S<Z>>>>>>
type Seven = S<S<S<S<S<S<S<Z>>>>>>>
type Eight = S<S<S<S<S<S<S<S<Z>>>>>>>>
type Nine  = S<S<S<S<S<S<S<S<S<Z>>>>>>>>>
type Ten   = S<S<S<S<S<S<S<S<S<S<Z>>>>>>>>>>

type IsZero<N extends Nat> =
    N extends Zero ? true : false

type Concat<X extends Nat, Y extends Nat> =
    X extends Zero ? Y :
    ["S", Concat<X[1], Y>];

type Prod<X extends Nat, Y extends Nat> = 
    X extends Zero ? Zero :
    Concat<Y, Prod<X[1], Y>>;

type Power<Base extends Nat, Exp extends Nat> =
    Exp extends Zero ? One :
    Prod<Base, Power<Base, Exp[1]>>;

type ToS<N extends Nat> =
    N extends Zero ? 'Z' :
    `S${ToS<N[1]>}`;

type ToDots<N extends Nat> =
    N extends Zero ? '' :
    `.${ToDots<N[1]>}`;

type LTE<X extends Nat, Y extends Nat> = 
  X extends Zero ? true :
  Y extends Zero ? false :
  LTE<X[1], Y[1]>

type LT<X extends Nat, Y extends Nat> = LTE<["S", X], Y>
type GTE<X extends Nat, Y extends Nat> = LTE<Y, X>
type GT<X extends Nat, Y extends Nat> = LT<Y, X>

type Eq<X extends Nat, Y extends Nat> = 
    X extends Zero ? IsZero<Y> :
    Y extends Zero ? false :
    Eq<X[1], Y[1]>

type Fib<X extends Nat> =
    X extends Zero ? Zero :
    X extends One ? One :
    Concat<Fib<X[1]>, Fib<X[1][1]>>

type Fac<X extends Nat> =
    X extends Zero ? One :
    Prod<X, Fac<X[1]>>