Andreas Abel and Jean-Philippe Bernardy,
A Unified View of Modalities in Type Systems,
ICFP 2020.
Section 5: Substitution Lemma
=============================
Lemma 5.1: Operator application ... distributes over ... (3) meet (`(γ ∧ δ)Ψ = γΨ ∧ δΨ`).
This isn't true. But by monotonicity, we have `(γ ∧ δ)Ψ ≤ γΨ ∧ δΨ`.
Section 8.1: On Church Encodings
================================
2021-05-22:
Our modification of Hasegawa's proof [1994] is wrong, here is the correction:
In the absence of the identity extension lemma (IEL) we cannot always
prove (set-theoretic) equalities by parametricity. However, we can
take `⟦A⟧` as definition fo extensional equality on set `⦅A⦆` and
prove that elements are `⟦A⟧`-related.
Thus, while we get `⦅unwrap (wrap t)⦆ = ⦅t⦆` by simplification, in the
opposite direction we can only prove `⦅wrap (unwrap t)⦆ ⟦Wrap A⟧ ⦅t⦆`.
To this end, assume monotypes `B` and `B'` and a relation
`R ⊆ ⦅B⦆ × ⦅B'⦆`, and further functions `k ∈ ⦅A⦆ → ⦅B⦆` and `k' ∈ ⦅A⦆ → ⦅B'⦆`
with `k (⟦A⟧ → R) k'`. We then have to show:
⦅Λβ.λk. k (t A (λx.x))⦆ ⦅B⦆ k R ⦅t⦆ ⦅B'⦆ k'
which simplifies to
k (⦅t⦆ ⦅A⦆ id) R ⦅t⦆ ⦅B'⦆ k'.
The fundamental lemma yields
⦅t⦆ ⟦∀β. (A ⊸ β) ⊸ β⟧ ⦅t⦆
which we instantiate to types `A` and `B'` and relation `R' ⊆ ⦅A⦆ × ⦅B'⦆` defined by
a R' b' ⇔ k(a) R b'.
Note that `id (⟦A⟧ → R') k'` because `k (⟦A⟧ → R) k'`.
This gives
⦅t⦆ ⦅A⦆ id R' ⦅t⦆ ⦅B'⦆ k'
which by definition is our goal
k (⦅t⦆ ⦅A⦆ id) R ⦅t⦆ ⦅B'⦆ k'.
□