Perform addition arithmetic and equality testing entirely in TypeScript's type system

adding_types.ts

// i++
interface Inc<T> {
    1: Inc<this>
    t: T
}

// i--
interface Dec<T> {
    0: T extends Inc<infer T> ? T : never
}

// A few identities
type Zero<Z> = Dec<Inc<Z>>[0];
type One<Z> = Inc<Z>;
type Two<Z> = Inc<One<Z>>;
type NegOne<Z> = Dec<Zero<Z>>[0];

// Some helpers for coding
type isTruthy<A> = A extends never ? never : true;

// Equality
// Resolves to type A if A == B otherwise resolves never
// Falsy cases must be instantiated to become never
type Eq<A, B> = A | B extends A ? A : never;

// Tests for equality
type OneEqOne<Z> = Eq<One<Z>, One<Z>>;
type OneNeqTwo<Z> = Eq<Two<Z>, One<Z>>;
type checkA = isTruthy<OneEqOne<0>>;
type checkB = isTruthy<OneNeqTwo<0>>;

// Adding
// 3 = 1 + 2
type Three<Z> = One<Two<Z>>;
// 6 = 3 + 3
type Six<Z> = Three<Three<Z>>;
// 6 = 1 + 1 + 1 + 1 + 1 + 1
type Six2<Z> = Inc<Z>[1][1][1][1][1]

// Equality check
type SixEqSix = isTruthy<Eq<Six<0>, Six2<0>>>;

// Powers of two
type TwoPow2<Z> = Two<Two<Z>>;
type TwoPow3<Z> = TwoPow2<TwoPow2<Z>>;
type TwoPow4<Z> = TwoPow3<TwoPow3<Z>>;
type TwoPow5<Z> = TwoPow4<TwoPow4<Z>>;
type TwoPow6<Z> = TwoPow5<TwoPow5<Z>>;
// Fails here because too deep :(
// type TwoPow7<Z> = TwoPow6<TwoPow6<Z>>;
// type TwoPow8<Z> = TwoPow7<TwoPow7<Z>>;