Coercion completion and conservativity in coercive subtyping (Q5957918)

The idea of coercive subtyping is to consider some given maps as coercions. One main application is in proof development based on type-theoretical systems [see the second author, Lect. Notes Comput. Sci. 1258, 273-296 (1997; Zbl 0882.03029), J. Log. Comput. 9, 105-130 (1999; Zbl 0920.03062)]. This can be seen as an extension of type theory, in this paper a typed version of Per Martin-Löf's logical framework. It is important for this extension to be a conservative extension. The main result of this paper is that if the given maps satisfy a suitable coherence condition then the extension is conservative.