We present some possible definitions for what it means for a type theory to be a conservative extension over another type theory. We do so by giving two type theories of natural numbers: T T (N) and T T (N, ×). T T (N) is ...