Efimov K-theory and universal localizing invariant

We give some basic properties of Efimov K-theory. In particular, Efimov K-theory is corepresentable, lax symmetric monoidal functor, preserves any small products and sends Milnor squares satisfying base change to cartesian squares.