Exercise _† not doable

[PiotrJander]

The statement in question is not (quite) provable.

Firstly, we are asked to formalise the translation _†. As a total function, _† must have a case for each constructor of the source language, for example, it would map S.zerotoT.zero.

But now we have that S.zero † ≡ T.zero but we don't have S.zero † ~ T.zero because the irrelevant constructors are omitted from the _~_ relation on purpose.

What would work is the following:

†≡→~ : ∀ {Γ A}
    → (M : Γ S.⊢ A)
    → {N : Γ T.⊢ A}
    → SimulationRelevant M
    → M † ≡ N
      ------------
    → M ~ N

where SimulationRelevant is a predicate on source terms which excludes the irrelevant constructors.

Let me know if this makes sense, and if so, I am happy to make a pull request.

[wadler]

Good point. Probably a better way forward is to change the problem to just show that M ~ N implies M † ≡ N.

[capn-freako]

#551 may be relevant.