Chatzikyriakidis & Luo (2020): MTT semantics via coercive subtyping

[CL20]

Modern Type Theory (MTT) analysis where common nouns denote types, not predicates, and subtyping is coercive — A ≤_c B whenever there is a unique implicit coercion c : A → B that the elaborator inserts on demand (paper §2.4, eqs. CA/CD on p. 40).

Coercive vs subsumptive. C&L explicitly reject subsumptive subtyping for MTT (p. 39): "subsumptive subtyping is incompatible with some key properties of modern type theories and, as a consequence, cannot be employed for an MTT." This file uses Lean's Coe typeclass, which is the canonical coercive-subtyping mechanism (value-level coercion functions, automatic elaboration-time insertion).

Coherence. Paper p. 40 fn 18 requires unique coercions between any two types. Lean's typeclass resolution picks an instance by priority rather than enforcing uniqueness; coherence is therefore the file author's responsibility, documented via CoherentCoercion Props below.

Main definitions

• Paper §3.2.1 CNs-as-types: Human, Book as inductive types.
• Paper §3.2.2 eq. 3.30-3.33 paradigm: Man = Σx:Human.male(x), heavy_book = Σx:Book.heavy(x), read : Human → Book → Prop, with read john_man warAndPeace_heavy well-typed via projective coercive subtyping.
• CoherentCoercion A B: Prop axiom stating any two Coe paths from A to B agree (paper coherence requirement, not enforced by Lean — proved per-instance).

References

• [CL20] §2.4 (coercive subtyping), §3.2.1 (CNs as types), §3.2.2 (subtyping in MTT-semantics, esp. eq. 3.30-3.33 and projective subtyping at eq. 3.33).

Paper §3.2.1: CNs as types

inductive ChatzikyriakidisLuo2020.Human : Type

• john : Human
• mary : Human
• bob : Human

@[implicit_reducible]

instance ChatzikyriakidisLuo2020.instDecidableEqHuman : DecidableEq Human

Equations

• ChatzikyriakidisLuo2020.instDecidableEqHuman x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ChatzikyriakidisLuo2020.instReprHuman : Repr Human

Equations

• ChatzikyriakidisLuo2020.instReprHuman = { reprPrec := ChatzikyriakidisLuo2020.instReprHuman.repr }

def ChatzikyriakidisLuo2020.instReprHuman.repr : Human → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive ChatzikyriakidisLuo2020.Book : Type

• warAndPeace : Book
• hamlet : Book

@[implicit_reducible]

instance ChatzikyriakidisLuo2020.instDecidableEqBook : DecidableEq Book

Equations

• ChatzikyriakidisLuo2020.instDecidableEqBook x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChatzikyriakidisLuo2020.instReprBook.repr : Book → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ChatzikyriakidisLuo2020.instReprBook : Repr Book

Equations

• ChatzikyriakidisLuo2020.instReprBook = { reprPrec := ChatzikyriakidisLuo2020.instReprBook.repr }

Paper §3.2.2: projective subtyping via Σ-types

Man := Σx:Human.male(x) (paper eq. 2.41); Man ≤_π₁ Human (eq. 2.42, p. 41) — the first projection is the coercion. In Lean, this is {h : Human // Male h} with Coe ... Human via Subtype.val.

def ChatzikyriakidisLuo2020.Male : Human → Prop

Equations

• ChatzikyriakidisLuo2020.Male ChatzikyriakidisLuo2020.Human.john = True
• ChatzikyriakidisLuo2020.Male ChatzikyriakidisLuo2020.Human.mary = False
• ChatzikyriakidisLuo2020.Male ChatzikyriakidisLuo2020.Human.bob = True

@[reducible, inline]

abbrev ChatzikyriakidisLuo2020.Man : Type

Equations

• ChatzikyriakidisLuo2020.Man = { h : ChatzikyriakidisLuo2020.Human // ChatzikyriakidisLuo2020.Male h }

@[implicit_reducible]

instance ChatzikyriakidisLuo2020.instCoeManHuman : Coe Man Human

Equations

• ChatzikyriakidisLuo2020.instCoeManHuman = { coe := Subtype.val }

def ChatzikyriakidisLuo2020.Heavy : Book → Prop

Heavy : Book → Prop; heavy_book := Σx:Book.heavy(x) (paper §3.2.2, eq. 3.31).

Equations

• ChatzikyriakidisLuo2020.Heavy ChatzikyriakidisLuo2020.Book.warAndPeace = True
• ChatzikyriakidisLuo2020.Heavy ChatzikyriakidisLuo2020.Book.hamlet = False

@[reducible, inline]

abbrev ChatzikyriakidisLuo2020.HeavyBook : Type

Equations

• ChatzikyriakidisLuo2020.HeavyBook = { b : ChatzikyriakidisLuo2020.Book // ChatzikyriakidisLuo2020.Heavy b }

@[implicit_reducible]

instance ChatzikyriakidisLuo2020.instCoeHeavyBookBook : Coe HeavyBook Book

Equations

• ChatzikyriakidisLuo2020.instCoeHeavyBookBook = { coe := Subtype.val }

Paper eq. 3.30-3.33 paradigm: read john W&P

def ChatzikyriakidisLuo2020.read : Human → Book → Prop

Paper §3.2.2: read : Human → Book → Prop.

Equations

• ChatzikyriakidisLuo2020.read x✝¹ x✝ = True

def ChatzikyriakidisLuo2020.johnMan : Man

johnMan : Man (John is a Man = a male Human).

Equations

• ChatzikyriakidisLuo2020.johnMan = ⟨ChatzikyriakidisLuo2020.Human.john, trivial⟩

def ChatzikyriakidisLuo2020.warAndPeaceHeavy : HeavyBook

warAndPeaceHeavy : HeavyBook (War & Peace is a heavy book).

Equations

• ChatzikyriakidisLuo2020.warAndPeaceHeavy = ⟨ChatzikyriakidisLuo2020.Book.warAndPeace, trivial⟩

theorem ChatzikyriakidisLuo2020.read_johnMan_wpHeavy_expanded : read johnMan.val warAndPeaceHeavy.val = read johnMan.val warAndPeaceHeavy.val

The expanded form: applying the explicit coercions yields the same term Lean's elaborator produces implicitly (paper rule CD, p. 40: f(a) = f(c(a))).

Coherence (paper p. 41 fn 18)

class ChatzikyriakidisLuo2020.CoherentCoercion (A B : Type) [Coe A B] : Prop

Coherence of coercions between two types: any two Coe-derived coercion functions agree. Lean's typeclass resolution does not enforce this (it picks by priority); the user declares and proves coherence on a case-by-case basis.

• coh (c₁ c₂ : A → B) : c₁ = Coe.coe → c₂ = Coe.coe → c₁ = c₂

instance ChatzikyriakidisLuo2020.instCoherentCoercionManHuman : CoherentCoercion Man Human

The Man-to-Human coercion is trivially coherent: there is only one Coe instance declared.

instance ChatzikyriakidisLuo2020.instCoherentCoercionHeavyBookBook : CoherentCoercion HeavyBook Book

The HeavyBook-to-Book coercion is trivially coherent.

Paper §3.2.2: subtyping propagates through function types

C&L p. 55: if A' ≤ A and B ≤ B', then A → B ≤ A' → B' (contravariance + covariance). In Lean this is automatic — any f : Human → Prop accepts m : Man via Coe insertion.

def ChatzikyriakidisLuo2020.Talks : Human → Prop

Equations

• ChatzikyriakidisLuo2020.Talks x✝ = True

Failure case: missing coercion is a type error

The paper's selectional-restriction argument: if there is no Coe Book Human, then Talks warAndPeace fails to elaborate. Lean's type error IS the paper's "category mistake" (paper §3.2.1, table 3.1 commentary). The following would not typecheck:

example : Prop := Talks Book.warAndPeace