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'.

□