Note that e.g. Agda uses unary representation of natural numbers during typechecking, but then compiles them to `BigInt`s to avoid exactly this kind of slowdown

Note that e.g. Agda uses unary representation of natural numbers during typechecking, but then compiles them to `BigInt`s to avoid exactly this kind of slowdown due to a representation that is well-suited for proofs.