Soundness of Coercion in the Calculus of Constructions (Q4820474)

Subtyping in the Calculus of Constructions (CoC) -- or in fact any Pure Type System -- allows \(\beta\)-equality to be represented by \(\leq\) in a judgement \((\Gamma \vdash A\leq B\) or \(\Gamma, \alpha \leq A:K \vdash M:B\)). It becomes useful when \(A\leq B\) is also allowed to hold for some \(\beta\)-distinct \(A\) and \(B\). \(\beta\eta\)-distinct \(A\)'s and \(B\)'s such that \(A\leq B\), become available in coercisve subtyping, the topic of this paper. It allows judgements such as \(\Gamma \vdash M: A\leq B\) where ``\(M: A\leq B\)'' can be interpreted as ``\(M\) is a function from \(A\) to \(B\)''. \(A\) and \(B\) may be \(\beta\eta\)-distinct and the judgement can be read as ``If \(\Gamma \), then \(A\) is coerced by \(M\) to be a subtype of \(B\)''. The standard properties of CoC are proved for the CoC with coersive subtyping and \(\beta\eta\)-equality. It still seems that this system only becomes useful when \(\Gamma \vdash M: A\leq B\) holds for some \(M\not=_{\beta\eta} \lambda x\! :\! A.x\). The present rules cannot provide such an \(M\). In fact the author proves: \[ \Gamma \vdash M: A\leq B\quad \Rightarrow \quad \Gamma \vdash M: A\to B \] and that there is a mapping \({\mathcal F}\) such that \[ \Gamma \vdash A: B\quad \Leftrightarrow \quad {\mathcal F}(\Gamma) \vdash_C A: B \] where \(C\) is CoC with \(\beta\eta\)-equality and constants.