Coercion completion and conservativity in coercive subtyping Original Research Article

Coercive subtyping offers a general approach to subtyping and inheritance by introducing a simple abbreviational mechanism to constructive type theories. In this paper, we study coercion completion in coercive subtyping and prove that the formal extension with coercive subtyping of a type theory such as Martin–Löfʹs type theory and UTT is a conservative extension. The importance of coherence conditions for the conservativity result is also discussed.