Cooper (2023) — the TTR apparatus

[Coo23]

The book's type-theoretic DSL, shared by the chapter files. TTR's metatheory is the ambient type theory: the judgment a : T is Lean's native typing, record types are structures, subtyping is Coe, truth is inhabitation, meet and join are Prod and Sum. This file keeps the book's names for that identification plus the apparatus with genuinely Cooper-specific content: intensional named types (IType, §1.3), parametric — presuppositional — content (Parametric, §4.3), and the compositional entries of §3.4 and §5.6.

Truth as inhabitation (§1.5)

@[reducible, inline]

abbrev Cooper2023.TTR.IsTrue (T : Type) : Prop

A TTR type is "true" (inhabited). §1.5.

Equations

• Cooper2023.TTR.IsTrue T = Nonempty T

@[reducible, inline]

abbrev Cooper2023.TTR.IsFalse (T : Type) : Prop

A TTR type is "false" (empty).

Equations

• Cooper2023.TTR.IsFalse T = IsEmpty T

theorem Cooper2023.TTR.true_false_exclusive (T : Type) : ¬(IsTrue T ∧ IsFalse T)

Truth and falsity are exclusive.

@[reducible, inline]

abbrev Cooper2023.TTR.propT (p : Prop) : Type

Lift a proposition to a type. Alias for PLift.

Equations

• Cooper2023.TTR.propT p = PLift p

Intensional types (§1.3)

Types are intensional: "there is nothing which prevents two types from being associated with exactly the same set of objects". A name-tagged wrapper makes the identity-beyond-extension explicit — the groundhog ~ woodchuck distinction: same animals, different types.

structure Cooper2023.TTR.IType : Type 1

An intensional type: a named type that carries identity beyond its extension (§1.3).

• carrier : Type

  The underlying Lean type (extension carrier)

• name : String

  Intensional identity tag (e.g., a predicate name)

def Cooper2023.TTR.instReprIType.repr : IType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cooper2023.TTR.instReprIType : Repr IType

Equations

• Cooper2023.TTR.instReprIType = { reprPrec := Cooper2023.TTR.instReprIType.repr }

def Cooper2023.TTR.IType.extEquiv (T₁ T₂ : IType) : Prop

Two ITypes are extensionally equivalent when their carriers are equivalent.

Equations

• T₁.extEquiv T₂ = Nonempty (T₁.carrier ≃ T₂.carrier)

def Cooper2023.TTR.IType.intEq (T₁ T₂ : IType) : Prop

Two ITypes are intensionally identical when both name and carrier match.

Equations

• T₁.intEq T₂ = (T₁ = T₂)

def Cooper2023.TTR.IType.meet (T₁ T₂ : IType) : IType

Meet of intensional types: compose carriers and names.

Equations

• T₁.meet T₂ = { carrier := T₁.carrier × T₂.carrier, name := T₁.name ++ " ∧ " ++ T₂.name }

def Cooper2023.TTR.IType.join (T₁ T₂ : IType) : IType

Join of intensional types: sum carriers and compose names.

Equations

• T₁.join T₂ = { carrier := T₁.carrier ⊕ T₂.carrier, name := T₁.name ++ " ∨ " ++ T₂.name }

theorem Cooper2023.TTR.ext_equiv_not_implies_int_eq : ¬∀ (T₁ T₂ : IType), T₁.extEquiv T₂ → T₁.intEq T₂

Core TTR thesis: extensional equivalence does not entail intensional identity — types are not sets.

Meet and join types (§2.3.3, Def 97)

@[reducible, inline]

abbrev Cooper2023.TTR.MeetType (T₁ T₂ : Type) : Type

Meet type: a : T₁ ∧ T₂ iff a : T₁ and a : T₂ — Lean's Prod.

Equations

• Cooper2023.TTR.MeetType T₁ T₂ = (T₁ × T₂)

@[reducible, inline]

abbrev Cooper2023.TTR.JoinType (T₁ T₂ : Type) : Type

Join type: a : T₁ ∨ T₂ iff a : T₁ or a : T₂ — Lean's Sum.

Equations

• Cooper2023.TTR.JoinType T₁ T₂ = (T₁ ⊕ T₂)

theorem Cooper2023.TTR.join_true_iff {T₁ T₂ : Type} : IsTrue (JoinType T₁ T₂) ↔ IsTrue T₁ ∨ IsTrue T₂

Join preserves truth in both directions.

Record-type subtyping (§1.4.3.5, ex 53)

A record type with more fields is a subtype of one with fewer fields (more constraints, fewer witnesses); the projection is the extends-generated forgetful map.

structure Cooper2023.TTR.BoyAndDog (E : Type) (Boy Dog : E → Prop) : Type

ex (53) target: [x:Ind, c₁:boy(x), y:Ind, c₂:dog(y)].

• x : E
• c₁ : Boy self.x
• y : E
• c₂ : Dog self.y

structure Cooper2023.TTR.BoyHugsDog (E : Type) (Boy Dog : E → Prop) (Hug : E → E → Prop) extends Cooper2023.TTR.BoyAndDog E Boy Dog : Type

ex (53) source: the subtype with the additional hug field.

• x : E
• c₁ : Boy self.x
• y : E
• c₂ : Dog self.y
• evt : Hug self.x self.y

Modal type systems (Def 54)

@[reducible, inline]

abbrev Cooper2023.TTR.ModalTypeSystem (W Pred : Type) : Type

A modal type system: for each possibility and predicate, whether the predicate has witnesses. Def 54; structurally a Kripke model.

Equations

• Cooper2023.TTR.ModalTypeSystem W Pred = (W → Pred → Bool)

Compositional semantics (§3.4)

The semantic type hierarchy: Ppty and Quant are the TTR analogues of Montague's ⟨e,t⟩ and ⟨⟨e,t⟩,t⟩.

@[reducible, inline]

abbrev Cooper2023.TTR.Ppty (E : Type) : Type 1

A property type: maps an individual to a type of situations. §3.4, ex (30).

Equations

• Cooper2023.TTR.Ppty E = (E → Type)

@[reducible, inline]

abbrev Cooper2023.TTR.Quant (E : Type) : Type 1

A quantifier type: maps a property to a type. §3.4.

Equations

• Cooper2023.TTR.Quant E = (Cooper2023.TTR.Ppty E → Type)

def Cooper2023.TTR.semCommonNoun {E : Type} (p : E → Type) : Ppty E

Common noun content: wrap a predicate as a property. §3.4, ex (30).

Equations

• Cooper2023.TTR.semCommonNoun p = p

def Cooper2023.TTR.semPropName {E : Type} (a : E) : Quant E

Proper name content as a generalized quantifier. §3.4, ex (33).

Equations

• Cooper2023.TTR.semPropName a P = P a

structure Cooper2023.TTR.ExistWitness (E : Type) (restr scope : Ppty E) : Type

The existential witness record type. §3.4, ex (37).

• individual : E
• restrWit : restr self.individual
• scopeWit : scope self.individual

def Cooper2023.TTR.semIndefArt {E : Type} (restr : Ppty E) : Quant E

Indefinite article content: maps a restrictor property to a quantifier. §3.4, ex (37).

Equations

• Cooper2023.TTR.semIndefArt restr scope = Cooper2023.TTR.ExistWitness E restr scope

def Cooper2023.TTR.semBe {E : Type} (Q : Quant E) : Ppty E

Copula "be" for predicate nominal constructions. §3.4, ex (78).

Equations

• Cooper2023.TTR.semBe Q x = Q fun (y : E) => Cooper2023.TTR.propT (x = y)

def Cooper2023.TTR.existPQ {E : Type} (P Q : Ppty E) : Prop

Existential quantification as property-extension overlap. §3.4, ex (55).

Equations

• Cooper2023.TTR.existPQ P Q = ∃ (a : E), Nonempty (P a) ∧ Nonempty (Q a)

def Cooper2023.TTR.semUniversal {E : Type} (restr scope : Ppty E) : Type

Universal quantifier as a type. §5.6.

Equations

• Cooper2023.TTR.semUniversal restr scope = ((x : E) → restr x → scope x)

Parametric content (§4.2–4.3)

Content that depends on a context: a background type (the presupposition) paired with a foreground function from satisfying contexts to content.

structure Cooper2023.TTR.Parametric (Content : Type u_1) : Type (max u_1 (u_2 + 1))

Parametric content. §4.3, (14).

• Bg : Type u_2

  Background type — what the context must provide (presupposition)

• fg : self.Bg → Content

  Foreground — content given a context satisfying the background

@[reducible, inline]

abbrev Cooper2023.TTR.PPpty (E : Type) : Type (u_1 + 1)

Parametric property: context-dependent property.

Equations

• Cooper2023.TTR.PPpty E = Cooper2023.TTR.Parametric (Cooper2023.TTR.Ppty E)

def Cooper2023.TTR.Parametric.trivial {Content : Type u_1} (c : Content) : Parametric Content

A trivial parametric content: no presupposition (bg = Unit).

Equations

• Cooper2023.TTR.Parametric.trivial c = { Bg := Unit, fg := fun (x : Unit) => c }

theorem Cooper2023.TTR.Parametric.trivial_fg {Content : Type u_1} (c : Content) (u : Unit) : (trivial c).fg u = c

A trivial parametric content yields the same value for any context.

Assignments (§4.6)

@[reducible, inline]

abbrev Cooper2023.TTR.Assgnmnt (E : Type) : Type

Variable assignment: maps natural-number indices to individuals. Equal to PartialAssign ℕ E; the alias name is retained because the book's prose uses 𝔰/𝔩/𝔯/𝔴/𝔤 as named "assignments" rather than as partial functions, and the inheritance carries the valued/valued_update_at simp set into this file's consumers.

Equations

• Cooper2023.TTR.Assgnmnt E = PartialAssign ℕ E

def Cooper2023.TTR.Assgnmnt.hasBindings {E : Type} (g : Assgnmnt E) (n : ℕ) : Prop

An assignment with at least n bindings (all indices < n defined).

Equations

• g.hasBindings n = ∀ (i : ℕ), i < n → (g i).isSome = true

def Cooper2023.TTR.Assgnmnt.merge {E : Type} (g₁ g₂ : Assgnmnt E) : Assgnmnt E

Merge two assignments (left-biased).

Equations

• g₁.merge g₂ i = (g₁ i).orElse fun (x : Unit) => g₂ i

theorem Cooper2023.TTR.Assgnmnt.merge_empty_left {E : Type} (g : Assgnmnt E) : merge PartialAssign.empty g = g

Merge with empty on the left returns the right assignment.

@[reducible, inline]

abbrev Cooper2023.TTR.PropCntxt : Type 1

Propositional context.

Equations

• Cooper2023.TTR.PropCntxt = Type