**LEMMA D.7 (STABILITY OF TRANSLATION BY WEAKENING).** If $\rho$ is a substitution that maps variables to variables then $[[t]][\rho] = [[t[\rho]]]$.

**PROOF.** Immediate by induction on $t$, the only case interesting case being the translation of variables, with a similar lemma for $[[A \rightsquigarrow B]] \simeq x$ using that neutrals are preserved. $\square$

**LEMMA D.8 (WELL-TYPED TERMS TRANSLATE).** If $\Gamma \vdash_{\text{coe}} t : A$ then $[[\Gamma]]\downarrow, [[A]]\downarrow$ and $[[t]]\downarrow$.

**PROOF.** We prove by a straightforward mutual induction on an algorithmic typing derivation that:

* If $\vdash_{\text{coe}} \Gamma$ then $[[\Gamma]]\downarrow$;

* If $\Gamma \vdash_{\text{coe}} A \triangleleft$ and $[[\Gamma]]\downarrow$ then $[[A]]\downarrow$;

* If $\Gamma \vdash_{\text{coe}} t \triangleleft A$ and $[[\Gamma]]\downarrow$ then $[[t]]\downarrow$;

* If $\Gamma \vdash_{\text{coe}} t \triangleright A$ and $[[\Gamma]]\downarrow$ then $[[t]]\downarrow$;

* If $\Gamma \vdash_{\text{coe}} A \preceq B \triangleleft$ or $\Gamma \vdash_{\text{coe}} A \preceq_h B \triangleleft$ then there exists $x$ such that $[[A \rightsquigarrow B]] \simeq x$. $\square$

**LEMMA D.9 (IDENTITY COERCIONS).** If $\Gamma \vdash_{\text{coe}} A \cong B \triangleleft$ or $\Gamma \vdash_{\text{coe}} A \cong_h B \triangleleft$ then $[[A \rightsquigarrow B]] \simeq \star$. $\square$

**PROOF.** Straightforward mutual induction on the bidirectional conversion derivation. $\square$

**LEMMA D.10 (STABILITY OF TRANSLATION BY SUBSTITUTION).** If $\Gamma \vdash_{\text{coe}} t : A$ and $\Delta \vdash_{\text{coe}} \sigma : \Gamma$ then $[[t]][[\sigma]] = [[t[\sigma]]]$ and similarly for typing.

If $\Gamma \vdash_{\text{coe}} A \preceq B \triangleleft$, $\Delta \vdash_{\text{coe}} \sigma : \Gamma$ and

* $[[A \rightsquigarrow B]] \simeq \star$ then $[[A[\sigma] \rightsquigarrow B[\sigma]]] \simeq \star$;

* $[[A \rightsquigarrow B]] \simeq f$ then $[[A[\sigma] \rightsquigarrow B[\sigma]]] \simeq f[\sigma]$. $\square$

**PROOF.** Straightforward mutual induction on the bidirectional derivation. $\square$

**Forward simulation.** Following the proof strategy employed for the equivalence between subsumptive and coercive subtyping, the next step would require to prove that the translation is a forward simulate, i.e. if $\Gamma \vdash_{\text{coe}} t : A$ and $t \rightsquigarrow^1 t'$ then $[[t]] \rightsquigarrow^* [[t')]$. As stated, this lemma does not hold. Indeed, the rule COECOE leads to reductions of coercions with type annotations which may be convertible but not reduce correctly. We conjecture that a weaker version of the simulation with respect to conversion in MLTT$_{map}$ should hold, that is if $\Gamma \vdash_{\text{coe}} t : A$ and $t \rightsquigarrow^1 t'$ then $[[\Gamma]] \vdash_{\text{map}} [[t]] \simeq [[t')] : [[A]]$. Such statement should be proved mutually with other properties stating that the translation preserves typing, as follows.

**CONJECTURE D.11 (TRANSLATION PRESERVES TYPING).**

(1) If $\vdash_{\text{coe}} \Gamma$ then $\vdash_{\text{map}} [[\Gamma]]$

(2) If $\Gamma \vdash_{\text{coe}} A$ then $\vdash_{\text{map}} [[\Gamma]]$

(3) If $\Gamma \vdash_{\text{coe}} t : A$ then $\vdash_{\text{map}} [[\Gamma]]$

(4) If $\Gamma \vdash_{\text{coe}} A \cong B$ then $\vdash_{\text{map}} [[\Gamma]]$

(5) If $\Gamma \vdash_{\text{coe}} t \cong u : A$ then $\vdash_{\text{map}} [[\Gamma]]$

(6) If $\Gamma \vdash_{\text{coe}} A \preceq B$ then either

(a) $[[A \rightsquigarrow B]] \simeq \star$ and $[[\Gamma]] \vdash_{\text{map}} [[A]] \simeq [[B]]$

(b) $[[A \rightsquigarrow B]] \simeq f$ and $[[\Gamma]] \vdash_{\text{map}} f : [[A]] \to [[B]]$

Preservation of typing, together with catch up lemmas, and a backward simulation lemma, would then allow to lift bidirectional conversion derivations in MLTT$_{map}$ between the translation of terms from MLTT$_{coe}$. The use of bidirectional conversion is essential here to remain at each step within the translation of MLTT$_{coe}$ terms.
CONJECTURE D.12 (EMBEDDING). `[—] embeds $MLTT_{coe}$ into $MLTT_{map}$: well-typed $MLTT_{coe}$ terms translate to well-typed $MLTT_{map}$ terms, preserving and reflecting conversion.
CONJECTURE D.12 (EMBEDDING). `[—] embeds $MLTT_{coe}$ into $MLTT_{map}$: well-typed $MLTT_{coe}$ terms translate to well-typed $MLTT_{map}$ terms, preserving and reflecting conversion.