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