Type Theory with Records — Core Foundations

[BP83] [Coo23] [ML84] [Mon73]

Type-theoretic foundations for TTR, organized by conceptual role:

Types & Judgments: IType, PredType/Ppty, records (DepRecordType, SituationRec), IsTrue/IsFalse. Subtyping uses Lean's built-in Coe typeclass.

Type Operations: MeetType = Prod, JoinType = Sum (native Lean), Restriction = Subtype (A11.7), record merges (symmetric = Prod, asymmetric; A11.3), StringType, TypeAct.

Modal Type Systems: ModalTypeSystem (Bool-valued, Ch1 Def 54), bridge to W → Bool.

Grammar: Cat, GSign, PSRule, phrase structure rules, lexical signs.

Compositional Semantics: Ppty, Quant, semCommonNoun, semPropName, ExistWitness, semIndefArt, semBe, propExtension, existPQ.

TTR replaces possible worlds with types as the bearers of propositional content. A type is "true" when it has a witness (is inhabited) and "false" when empty. Unlike sets, types are intensional: two types can have the same witnesses yet remain distinct (groundhog ≠ woodchuck even if co-extensional).

Native Lean type usage

TTR Concept	Lean Encoding
a : T judgment	Native typing
Predicate types	E → Type (PredType/Ppty)
Meet types	T₁ × T₂ (Prod)
Join types	Sum T₁ T₂
Restriction (A11.7)	{ x : T // P x } (Subtype)
Symmetric merge (A11.3)	T₁ × T₂ (Prod)
Dependent records	structure
Fixed-point types	(x : E) × P x (Sigma)
IsTrue/IsFalse	Nonempty T/IsEmpty T

§ 1.2 Perception as type assignment

Perceiving an object involves classifying it as being of a type. In symbols: a : T — a judgement that a is of type T. This is Lean's native typing judgement, so no new definition is needed.

The key philosophical point: you cannot perceive something without ascribing some type to it, even if very general (Thing, Entity).

§ 1.3 System of basic types (Cooper Def 1)

A system of basic types TYPE_B = ⟨Type, A⟩ where:

• Type is a non-empty set of types
• A assigns to each type its set of witnesses
• Types are intensional: distinct types may share all witnesses

In Lean, Type u already provides the universe of types, and each type T : Type u has its collection of terms. The key TTR feature that Lean does capture is intensionality at the Prop level: propext identifies logically equivalent propositions, but at Type two types can be equivalent (T ≃ S) yet not definitionally equal.

For the purposes of connecting to linguistic theory, we introduce a lightweight wrapper that makes TTR's intensional type identity explicit.

structure Semantics.TypeTheoretic.IType : Type 1

An intensional type: a named type that carries identity beyond its extension. §1.3: "there is nothing which prevents two types from being associated with exactly the same set of objects" — types are intensional.

The name field distinguishes types even when they have the same carrier. This models the groundhog/woodchuck distinction: same animals, different types.

• carrier : Type

  The underlying Lean type (extension carrier)

• name : String

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

def Semantics.TypeTheoretic.instReprIType.repr : IType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprIType : Repr IType

Equations

• Semantics.TypeTheoretic.instReprIType = { reprPrec := Semantics.TypeTheoretic.instReprIType.repr }

def Semantics.TypeTheoretic.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 Semantics.TypeTheoretic.IType.intEq (T₁ T₂ : IType) : Prop

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

Equations

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

def Semantics.TypeTheoretic.IType.meet (T₁ T₂ : IType) : IType

Meet of intensional types: compose carriers and names. Intensional identity is preserved through meet, so compositional expressions built from distinct atomic types remain distinct.

Equations

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

def Semantics.TypeTheoretic.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 Semantics.TypeTheoretic.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. This is the formal content of Cooper's claim that types are not sets.

§ 1.4.1 Predicate types (ptypes)

A ptype P(a₁,...,aₙ) is a type constructed from a predicate and arguments. Witnesses are situations/events in which the predicate holds of the arguments.

In Lean, this is naturally modeled as dependent function application: given P : α → Type (a one-place predicate-as-type-constructor), P a is the ptype whose witnesses are proofs/situations of P a.

@[reducible, inline]

abbrev Semantics.TypeTheoretic.PredType (E : Type) : Type 1

A predicate type constructor: maps entities to types (of situations). PredType E is a one-place predicate over entities of type E. The resulting type p e is the type of situations witnessing p of e.

Equations

• Semantics.TypeTheoretic.PredType E = (E → Type)

@[reducible, inline]

abbrev Semantics.TypeTheoretic.PredType2 (E : Type) : Type 1

A two-place predicate type constructor (relations).

Equations

• Semantics.TypeTheoretic.PredType2 E = (E → E → Type)

@[reducible, inline]

abbrev Semantics.TypeTheoretic.ptype {E : Type} (P : PredType E) (a : E) : Type

A ptype: the type of situations where predicate P holds of argument a. §1.4.1, Def 7: if Arity(P) = ⟨T₁,...,Tₙ⟩ and aᵢ : Tᵢ, then P(a₁,...,aₙ) ∈ PType.

Equations

• Semantics.TypeTheoretic.ptype P a = P a

@[reducible, inline]

abbrev Semantics.TypeTheoretic.ptype2 {E : Type} (P : PredType2 E) (a b : E) : Type

A relational ptype: P(a,b) for a two-place predicate.

Equations

• Semantics.TypeTheoretic.ptype2 P a b = P a b

def Semantics.TypeTheoretic.typeFromPred {E : Type} (P : PredType E) (a : E) : Prop

The relationship between basic types and predicates (Cooper §1.4.1, ex 10): a : Dog iff there exists a situation e witnessing dog(a). This connects basic types (like Dog) to predicate types.

Equations

• Semantics.TypeTheoretic.typeFromPred P a = Nonempty (P a)

§ 1.4.3 Record types

A record type is a collection of labelled fields where each field specifies a type. Fields may be dependent: the type of a later field can depend on the values in earlier fields.

Records (witnesses of record types) are labelled sets of values matching the field types.

In Lean, structure declarations are record types. We don't re-implement the infrastructure — we identify Lean structures with TTR records and prove the key properties Cooper establishes.

structure Semantics.TypeTheoretic.SimpleRecordType2 (T₁ T₂ : Type) : Type

A simple (non-dependent) record type with two fields. Models §1.4.3, ex (18a): [ x : Ind, y : Ind, e : hug(x,y)] but without dependency (the hug field's type doesn't reference x,y).

• fst : T₁
• snd : T₂

structure Semantics.TypeTheoretic.DepRecordType (T₁ : Type) (T₂ : T₁ → Type) : Type

A dependent record type: the second field's type depends on the first. This captures Cooper's dependent fields (§1.4.3.1, ex 25): [ x : Ind, c₁ : boy(x)] where the type of c₁ depends on which individual x is.

• fst : T₁
• snd : T₂ self.fst

structure Semantics.TypeTheoretic.SituationRec (E : Type) (R : E → E → Type) : Type

A situation record: the canonical TTR record type for event semantics. Models §1.4.3, ex (18a): [ x : Ind, y : Ind, e : hug(x,y)]

• x : E
• y : E
• evt : R self.x self.y

§ 1.4.3.5 Subtyping

Record type T₁ is a subtype of T₂ (T₁ ⊑ T₂) iff every witness of T₁ is also a witness of T₂, regardless of what is assigned to the basic types and ptypes (Cooper Def 55 — this is a modal/universal notion).

For record types specifically, T₁ ⊑ T₂ when T₁ has all the fields of T₂ (plus possibly more). More fields = more specific = subtype.

This is the reverse of what you might expect from set inclusion: the type with MORE constraints has FEWER witnesses.

Subtyping via Lean's Coe

Subtyping T₁ ⊑ T₂ (§1.4.3.5, Def 55) is Lean's Coe T₁ T₂ — a coercive subtyping mechanism with implicit elaboration insertion. This matches [CL20]'s preferred coercive subtyping (paper §2.4, p. 39: subsumptive subtyping "cannot be employed for an MTT"; coercive subtyping is the suitable mechanism). Composition through Coe chains via Lean's CoeHTCT; no explicit Trans registration needed.

structure Semantics.TypeTheoretic.BoyAndDog (E : Type) (Boy Dog : E → Prop) : Type

Record type with more fields is a subtype of one with fewer fields. ex (53): [x:Ind, c₁:boy(x), y:Ind, c₂:dog(y), e:hug(x,y)] is a subtype of [x:Ind, c₁:boy(x), y:Ind, c₂:dog(y)].

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

structure Semantics.TypeTheoretic.BoyHugsDog (E : Type) (Boy Dog : E → Prop) (Hug : E → E → Prop) extends Semantics.TypeTheoretic.BoyAndDog E Boy Dog : Type

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

BoyHugsDog ⊑ BoyAndDog (more fields → subtype). The projection is BoyHugsDog.toBoyAndDog, automatically generated by Lean's extends. We do not register this as a Coe instance — the extra parameter Hug is in the source but not the target, so the elaborator cannot synthesize the instance from a BoyAndDog-typed context. Consumers project explicitly via .toBoyAndDog.

§ 1.5 Propositions as types

The central semantic thesis of TTR: types play the role of propositions.

• A type is true when it is inhabited (has a witness).
• A type is false when it is empty (has no witness).
• hug(a,b) is true iff there exists a situation of that type.

This connects to [ML84]'s propositions-as-types and to constructive mathematics' proof-by-witness.

@[reducible, inline]

abbrev Semantics.TypeTheoretic.IsTrue (T : Type) : Prop

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

Equations

• Semantics.TypeTheoretic.IsTrue T = Nonempty T

@[reducible, inline]

abbrev Semantics.TypeTheoretic.IsFalse (T : Type) : Prop

A TTR type is "false" (empty).

Equations

• Semantics.TypeTheoretic.IsFalse T = IsEmpty T

theorem Semantics.TypeTheoretic.true_false_exclusive (T : Type) : ¬(IsTrue T ∧ IsFalse T)

Truth and falsity are exclusive.

theorem Semantics.TypeTheoretic.IType.meet_true_iff (T₁ T₂ : IType) : IsTrue (T₁.meet T₂).carrier ↔ IsTrue T₁.carrier ∧ IsTrue T₂.carrier

IType.meet truth = conjunction of component truth.

theorem Semantics.TypeTheoretic.IType.join_true_iff (T₁ T₂ : IType) : IsTrue (T₁.join T₂).carrier ↔ IsTrue T₁.carrier ∨ IsTrue T₂.carrier

IType.join truth = disjunction of component truth.

theorem Semantics.TypeTheoretic.subtype_preserves_truth {T₁ T₂ : Type} [Coe T₁ T₂] (hT : IsTrue T₁) : IsTrue T₂

Subtypes preserve truth: if T₁ ⊑ T₂ (Coe T₁ T₂) and T₁ is true, then T₂ is true.

theorem Semantics.TypeTheoretic.supertype_preserves_falsity {T₁ T₂ : Type} [Coe T₁ T₂] (hF : IsFalse T₂) : IsFalse T₁

Supertypes preserve falsity: if T₁ ⊑ T₂ (Coe T₁ T₂) and T₂ is false, then T₁ is false.

PLift helper

propT p is a readable alias for PLift p, used throughout TTR when embedding a Prop into Type (e.g., propT (x = y) instead of PLift (x = y)).

@[reducible, inline]

abbrev Semantics.TypeTheoretic.propT (p : Prop) : Type

Lift a proposition to a type. Alias for PLift.

Equations

• Semantics.TypeTheoretic.propT p = PLift p

Bridge to Set

Cooper's world-indexed propositions: at each world w, a proposition corresponds to a type that may or may not be inhabited. This is exactly Set W = W → Prop — at each world, we get a Prop, which in CIC is a type (in Sort 0).

The bridge: Set W is a family of TTR types indexed by "possibilities" (worlds). The proposition is true at w iff the type p w is inhabited.

theorem Semantics.TypeTheoretic.prop'_true_iff_inhabited {W : Type u_1} (p : Set W) (w : W) : p w ↔ Nonempty (propT (p w))

A Set W proposition is TTR-true at world w iff the Prop is inhabited.

Bridge to Intensional.Intension

An Intension W τ is a function from worlds to extensions. In TTR terms, this is a type family indexed by possibilities in a modal type system (Cooper Def 54). When τ = Prop, an intension is exactly a world-indexed TTR proposition.

theorem Semantics.TypeTheoretic.intension_prop_is_ttr_prop (W : Type u_1) : Intensional.Intension W Prop = Set W

An intension of Prop is a world-indexed family of TTR propositions.

Modal type systems (Cooper Def 54)

A modal system of complex types TYPE_MC is a family of type systems indexed by "possibilities" M ∈ M. Basic types and predicates are shared across possibilities, but witness assignments vary.

This is structurally a Kripke model: each possibility assigns extensions to predicates, just as each world assigns truth values.

We formalize the connection: a modal type system over W possibilities with Bool-valued predicates is exactly a (W → Bool).

@[reducible, inline]

abbrev Semantics.TypeTheoretic.ModalTypeSystem (W Pred : Type) : Type

A modal type system: for each possibility and predicate, whether the predicate has witnesses. §1.4.3.5, Def 54.

Equations

• Semantics.TypeTheoretic.ModalTypeSystem W Pred = (W → Pred → Bool)

def Semantics.TypeTheoretic.ModalTypeSystem.toBProp {W Pred : Type} (mts : ModalTypeSystem W Pred) (P : Pred) : W → Bool

A predicate in a modal type system yields a W → Bool.

Equations

• mts.toBProp P w = mts w P

def Semantics.TypeTheoretic.ModalTypeSystem.subtypeBProp {W Pred : Type} (mts : ModalTypeSystem W Pred) (P₁ P₂ : Pred) : Prop

Subtyping in a modal type system: T₁ ⊑ T₂ iff at every possibility where T₁ has witnesses, T₂ also has witnesses. This is exactly propositional entailment. Def 55.

Equations

• mts.subtypeBProp P₁ P₂ = ∀ (w : W), mts w P₁ = true → mts w P₂ = true

theorem Semantics.TypeTheoretic.modal_subtype_eq_entailment {W Pred : Type} (mts : ModalTypeSystem W Pred) (P₁ P₂ : Pred) : mts.subtypeBProp P₁ P₂ ↔ {w : W | mts.toBProp P₁ w = true} ⊆ {w : W | mts.toBProp P₂ w = true}

Modal subtyping = propositional entailment (the bridge theorem).

Bridge: IType + ModalTypeSystem → Intensional.Intension

An IType, viewed through a Bool-valued modal type system (Def 54), induces an intension (W → Bool). Whether this intension is rigid (constant across all possibilities) corresponds exactly to Intensional.Intension.IsRigid — connecting Cooper's Ch1 intensional types to the framework-agnostic intension machinery.

def Semantics.TypeTheoretic.IType.toIntension {W : Type} (mts : ModalTypeSystem W String) (T : IType) : Intensional.Intension W Bool

An IType in a modal type system induces an intension. At each possibility w, the type either has witnesses (true) or not (false). Def 54: possibilities index witness assignments.

Equations

• Semantics.TypeTheoretic.IType.toIntension mts T = mts.toBProp T.name

theorem Semantics.TypeTheoretic.IType.rigid_iff_isRigid {W : Type} (mts : ModalTypeSystem W String) (T : IType) : (toIntension mts T).IsRigid ↔ ∀ (w₁ w₂ : W), mts w₁ T.name = mts w₂ T.name

An IType's intension is rigid iff it has constant witness status across all possibilities. Bridges Ch1 intensional types to IsRigid.

theorem Semantics.TypeTheoretic.IType.coext_not_intEq {W : Type} (mts : ModalTypeSystem W String) (T₁ T₂ : IType) (_hCoExt : (toIntension mts T₁).CoExtensional (toIntension mts T₂)) (hNames : T₁.name ≠ T₂.name) : ¬T₁.intEq T₂

Intensionally distinct ITypes can have co-extensional intensions: the groundhog/woodchuck phenomenon at the modal level.

§ 2.2 String theory of events

Events have temporal extent and can be decomposed into strings (sequences) of sub-events. A game of fetch decomposes into: pick_up ⌢ throw ⌢ run_after ⌢... In TTR, a string type T⁺ is the type of non-empty strings of events of type T. We model this with lists, which Lean handles natively.

structure Semantics.TypeTheoretic.StringType (T : Type) : Type

A string type: a non-empty sequence of typed events. §2.2: events decompose into strings of sub-events. The field ne ensures non-emptiness (TTR uses T⁺, not T*).

• events : List T
• ne : self.events ≠ []

def Semantics.TypeTheoretic.StringType.concat {T : Type} (s₁ s₂ : StringType T) : StringType T

String concatenation: combining two event strings. §2.2, string concatenation s₁ ⌢ s₂.

Equations

• s₁ ⌢ s₂ = { events := s₁.events ++ s₂.events, ne := ⋯ }

def Semantics.TypeTheoretic.«term_⌢_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.TypeTheoretic.StringType.concat_assoc {T : Type} (s₁ s₂ s₃ : StringType T) : (s₁ ⌢ s₂ ⌢ s₃).events = (s₁ ⌢ (s₂ ⌢ s₃)).events

Concatenation is associative (strings form a semigroup).

def Semantics.TypeTheoretic.StringType.singleton {T : Type} (t : T) : StringType T

A single-element string (singleton event).

Equations

• Semantics.TypeTheoretic.StringType.singleton t = { events := [t], ne := ⋯ }

§ 2.3.1 Type acts

Agents interact with types through three fundamental acts:

• Judge: classify an observed object as being of a type (a : T)
• Query: ask whether an object is of a type (a : T?)
• Create: bring into existence a witness of a type

These correspond to the three basic speech acts: assertion, question, command. §2.3.1, ex (30–32).

inductive Semantics.TypeTheoretic.TypeAct : Type

The three fundamental type acts. §2.3.1.

• judge : TypeAct
• query : TypeAct
• create : TypeAct

def Semantics.TypeTheoretic.instReprTypeAct.repr : TypeAct → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprTypeAct : Repr TypeAct

Equations

• Semantics.TypeTheoretic.instReprTypeAct = { reprPrec := Semantics.TypeTheoretic.instReprTypeAct.repr }

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqTypeAct : DecidableEq TypeAct

Equations

• Semantics.TypeTheoretic.instDecidableEqTypeAct x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

§ 2.3.3 Meet and join types (Cooper ex 42, 47)

Meet types (T₁ ∧ T₂): a witness must be of BOTH types simultaneously. Join types (T₁ ∨ T₂): a witness is of EITHER type.

These are the type-theoretic analogues of conjunction and disjunction, and they correspond exactly to Lean's Prod and Sum.

@[reducible, inline]

abbrev Semantics.TypeTheoretic.MeetType (T₁ T₂ : Type) : Type

Meet type: a : T₁ ∧ T₂ iff a : T₁ and a : T₂. §2.6, Def 97. In Lean, this is T₁ × T₂. We introduce an alias to make the TTR connection explicit.

Equations

• Semantics.TypeTheoretic.MeetType T₁ T₂ = (T₁ × T₂)

@[reducible, inline]

abbrev Semantics.TypeTheoretic.JoinType (T₁ T₂ : Type) : Type

Join type: a : T₁ ∨ T₂ iff a : T₁ or a : T₂. §2.3.3, ex (47). In Lean, this is Sum T₁ T₂.

Equations

• Semantics.TypeTheoretic.JoinType T₁ T₂ = (T₁ ⊕ T₂)

theorem Semantics.TypeTheoretic.meet_true_of_both {T₁ T₂ : Type} (h₁ : IsTrue T₁) (h₂ : IsTrue T₂) : IsTrue (MeetType T₁ T₂)

Meet of inhabited types is inhabited.

theorem Semantics.TypeTheoretic.join_true_of_left {T₁ T₂ : Type} (h : IsTrue T₁) : IsTrue (JoinType T₁ T₂)

Join is inhabited if either component is.

theorem Semantics.TypeTheoretic.join_true_of_right {T₁ T₂ : Type} (h : IsTrue T₂) : IsTrue (JoinType T₁ T₂)

Meet/Join subtyping (ex 98c,d and §2.3.3) is captured by Lean's native Prod.fst/Prod.snd (projection out of meet) and Sum.inl/Sum.inr (injection into join). Per mathlib idiom we do not register these as Coe instances — the (MeetType T₁ T₂) ⊑ T₁ shape leaves the other component (T₂) unrecoverable from the target type alone, so the elaborator cannot synthesize the instance. Consumers use the projections/injections explicitly.

theorem Semantics.TypeTheoretic.meet_true_iff {T₁ T₂ : Type} : IsTrue (MeetType T₁ T₂) ↔ IsTrue T₁ ∧ IsTrue T₂

Meet preserves truth in both directions (iff). The type-theoretic analogue of conjunction introduction + elimination.

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

Join preserves truth in both directions (iff). The type-theoretic analogue of disjunction introduction + elimination.

Appendix A11.7: Restriction (T ∥ r)

Appendix A11.7: a restriction of type T by predicate r is the type of objects of T satisfying r. This is exactly Lean's native Subtype (refinement type): { x : T // P x }.

Using Lean's Subtype directly gives us the full API for free: .val projects the underlying value, .property gives the proof.

@[reducible, inline]

abbrev Semantics.TypeTheoretic.Restriction (T : Type) (P : T → Prop) : Type

Cooper's restriction T ∥ r = Lean's Subtype: the type of elements of T satisfying predicate P. Appendix A11.7.

Equations

• Semantics.TypeTheoretic.Restriction T P = { x : T // P x }

Restriction (T ∥ P) ⊑ T: every restricted element projects to the base type via Subtype.val. Per mathlib idiom we do not register this as a generic Coe (Restriction T P) T instance because Lean cannot infer P from the target T alone; consumers use .val explicitly.

theorem Semantics.TypeTheoretic.restriction_true_iff {T : Type} {P : T → Prop} : IsTrue (Restriction T P) ↔ ∃ (x : T), P x

Truth of a restriction requires both: an element AND the predicate.

theorem Semantics.TypeTheoretic.restriction_implies_base {T : Type} {P : T → Prop} (h : IsTrue (Restriction T P)) : IsTrue T

Restriction strengthens: if T ∥ P is true, the base type T is also true (via .val projection).

Appendix A11.3: Record merges

Appendix A11.3 defines two kinds of record merge:

• Symmetric merge μ(T₁, T₂): the type with fields from both records. This is MeetType T₁ T₂ = T₁ × T₂ (Lean's Prod).
• Asymmetric merge μ_asym(T₁, T₂): T₂ fields override T₁ fields. Modeled as a base-override pair.

theorem Semantics.TypeTheoretic.symmetric_merge_is_meet (T₁ T₂ : Type) : MeetType T₁ T₂ = (T₁ × T₂)

Symmetric merge is meet (product type). A11.3: μ(T₁, T₂) combines all fields of both records.

def Semantics.TypeTheoretic.symmetric_merge_comm (T₁ T₂ : Type) : MeetType T₁ T₂ ≃ MeetType T₂ T₁

Symmetric merge is commutative (up to equivalence).

Equations

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

def Semantics.TypeTheoretic.merge_unit_right (T : Type) : MeetType T Unit ≃ T

Merging with Unit is identity (up to equivalence). A11.3: the empty record type acts as a merge identity.

Equations

• Semantics.TypeTheoretic.merge_unit_right T = { toFun := Prod.fst, invFun := fun (t : T) => (t, ()), left_inv := ⋯, right_inv := ⋯ }

structure Semantics.TypeTheoretic.AsymMerge (T₁ T₂ : Type) : Type

Asymmetric merge: T₂ fields override T₁ fields. A11.3: μ_asym(T₁, T₂) takes T₁ as base and T₂ as override. Accessors prefer override fields when both provide the same label.

• base : T₁

  The base record

• override : T₂

  The override record (its fields take priority)

def Semantics.TypeTheoretic.asymMerge_unit_override (T : Type) : AsymMerge T Unit ≃ T

Asymmetric merge with Unit override is equivalent to the base.

Equations

• Semantics.TypeTheoretic.asymMerge_unit_override T = { toFun := Semantics.TypeTheoretic.AsymMerge.base, invFun := fun (t : T) => { base := t, override := () }, left_inv := ⋯, right_inv := ⋯ }

§ 2.5 Signs (Cooper ex 70)

A sign pairs a speech event with its content.

structure Semantics.TypeTheoretic.TTRSign (Phon Cont : Type) : Type

A TTR sign: a pairing of speech event type and content type. §2.5, ex (70). The phonological-form field is named phon (broader linguistic terminology; Cooper writes "s-event" interchangeably).

• phon : Phon
• cont : Cont

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprTTRSign {Phon✝ Cont✝ : Type} [Repr Phon✝] [Repr Cont✝] : Repr (TTRSign Phon✝ Cont✝)

Equations

• Semantics.TypeTheoretic.instReprTTRSign = { reprPrec := Semantics.TypeTheoretic.instReprTTRSign.repr }

def Semantics.TypeTheoretic.instReprTTRSign.repr {Phon✝ Cont✝ : Type} [Repr Phon✝] [Repr Cont✝] : TTRSign Phon✝ Cont✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqTTRSign {Phon✝ Cont✝ : Type} [DecidableEq Phon✝] [DecidableEq Cont✝] : DecidableEq (TTRSign Phon✝ Cont✝)

Equations

• Semantics.TypeTheoretic.instDecidableEqTTRSign = Semantics.TypeTheoretic.instDecidableEqTTRSign.decEq

def Semantics.TypeTheoretic.instDecidableEqTTRSign.decEq {Phon✝ Cont✝ : Type} [DecidableEq Phon✝] [DecidableEq Cont✝] (x✝ x✝¹ : TTRSign Phon✝ Cont✝) : Decidable (x✝ = x✝¹)

Equations

• Semantics.TypeTheoretic.instDecidableEqTTRSign.decEq { phon := a, cont := a_1 } { phon := b, cont := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

theorem Semantics.TypeTheoretic.TTRSign.ext {Phon Cont : Type} {s t : TTRSign Phon Cont} (hphon : s.phon = t.phon) (hcont : s.cont = t.cont) : s = t

Extensionality for TTR signs.

theorem Semantics.TypeTheoretic.TTRSign.ext_iff {Phon Cont : Type} {s t : TTRSign Phon Cont} : s = t ↔ s.phon = t.phon ∧ s.cont = t.cont

def Semantics.TypeTheoretic.TTRSign.map {Phon Cont Phon' Cont' : Type} (f : Phon → Phon') (g : Cont → Cont') (s : TTRSign Phon Cont) : TTRSign Phon' Cont'

Map both fields of a TTR sign — the Bifunctor.bimap analogue.

Equations

• Semantics.TypeTheoretic.TTRSign.map f g s = { phon := f s.phon, cont := g s.cont }

@[simp]

theorem Semantics.TypeTheoretic.TTRSign.map_phon {Phon Cont Phon' Cont' : Type} (f : Phon → Phon') (g : Cont → Cont') (s : TTRSign Phon Cont) : (map f g s).phon = f s.phon

@[simp]

theorem Semantics.TypeTheoretic.TTRSign.map_cont {Phon Cont Phon' Cont' : Type} (f : Phon → Phon') (g : Cont → Cont') (s : TTRSign Phon Cont) : (map f g s).cont = g s.cont

@[simp]

theorem Semantics.TypeTheoretic.TTRSign.map_id {Phon Cont : Type} (s : TTRSign Phon Cont) : map id id s = s

§ 3.2 Hierarchical constituent structure

Events have hierarchical structure beyond flat string types.

inductive Semantics.TypeTheoretic.BusEvent : Type

Events in a bus trip. §3.2, ex (1–2).

• waitAtBusstop : BusEvent
• busArrive : BusEvent
• getOnBus : BusEvent
• travelOnBus : BusEvent
• getOffBus : BusEvent

def Semantics.TypeTheoretic.instReprBusEvent.repr : BusEvent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprBusEvent : Repr BusEvent

Equations

• Semantics.TypeTheoretic.instReprBusEvent = { reprPrec := Semantics.TypeTheoretic.instReprBusEvent.repr }

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqBusEvent : DecidableEq BusEvent

Equations

• Semantics.TypeTheoretic.instDecidableEqBusEvent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.TypeTheoretic.getBus : StringType BusEvent

GetBus = WaitAtBusstop ⌢ BusArrive ⌢ GetOnBus. Cooper §3.2, ex (2).

Equations

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

theorem Semantics.TypeTheoretic.busTripDecomp : [BusEvent.waitAtBusstop, BusEvent.busArrive, BusEvent.getOnBus, BusEvent.travelOnBus, BusEvent.getOffBus] = (getBus ⌢ StringType.singleton BusEvent.travelOnBus ⌢ StringType.singleton BusEvent.getOffBus).events

BusTrip decomposes as GetBus ⌢ TravelOnBus ⌢ GetOffBus. Cooper §3.2, ex (1).

§ 3.3 Syntactic categories

§3.3, ex (12): Cat is a basic type with witnesses s, np, det, n, v, vp — the categories needed for the English fragment.

inductive Semantics.TypeTheoretic.Cat : Type

Syntactic categories for Cooper's English fragment. §3.3, ex (12).

• s : Cat
• np : Cat
• det : Cat
• n : Cat
• v : Cat
• vp : Cat

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprCat : Repr Cat

Equations

• Semantics.TypeTheoretic.instReprCat = { reprPrec := Semantics.TypeTheoretic.instReprCat.repr }

def Semantics.TypeTheoretic.instReprCat.repr : Cat → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqCat : DecidableEq Cat

Equations

• Semantics.TypeTheoretic.instDecidableEqCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.TypeTheoretic.Cat.isLexical : Cat → Bool

Whether a category is lexical (word-level) vs phrasal.

Equations

• Semantics.TypeTheoretic.Cat.n.isLexical = true
• Semantics.TypeTheoretic.Cat.v.isLexical = true
• Semantics.TypeTheoretic.Cat.det.isLexical = true
• Semantics.TypeTheoretic.Cat.s.isLexical = false
• Semantics.TypeTheoretic.Cat.np.isLexical = false
• Semantics.TypeTheoretic.Cat.vp.isLexical = false

def Semantics.TypeTheoretic.Cat.toUPOS? : Cat → Option UD.UPOS

Bridge: TTR Cat → UD UPOS for lexical categories.

Equations

• Semantics.TypeTheoretic.Cat.n.toUPOS? = some UD.UPOS.NOUN
• Semantics.TypeTheoretic.Cat.v.toUPOS? = some UD.UPOS.VERB
• Semantics.TypeTheoretic.Cat.det.toUPOS? = some UD.UPOS.DET
• Semantics.TypeTheoretic.Cat.s.toUPOS? = none
• Semantics.TypeTheoretic.Cat.np.toUPOS? = none
• Semantics.TypeTheoretic.Cat.vp.toUPOS? = none

theorem Semantics.TypeTheoretic.cat_lexical_has_upos (c : Cat) (h : c.isLexical = true) : c.toUPOS?.isSome = true

Lexical categories always have a UPOS mapping.

inductive Semantics.TypeTheoretic.GSign (Phon Cont : Type) : Type

A grammatical sign with syntactic structure. §3.3, ex (11).

• mk {Phon Cont : Type} (phon : Phon) (cat : Cat) (daughters : List (GSign Phon Cont)) (cont : Cont) : GSign Phon Cont

def Semantics.TypeTheoretic.GSign.phon {Phon Cont : Type} : GSign Phon Cont → Phon

Equations

• (Semantics.TypeTheoretic.GSign.mk e cat daughters cont).phon = e

def Semantics.TypeTheoretic.GSign.cat {Phon Cont : Type} : GSign Phon Cont → Cat

Equations

• (Semantics.TypeTheoretic.GSign.mk e cat daughters cont).cat = cat

def Semantics.TypeTheoretic.GSign.daughters {Phon Cont : Type} : GSign Phon Cont → List (GSign Phon Cont)

Equations

• (Semantics.TypeTheoretic.GSign.mk e cat daughters cont).daughters = daughters

def Semantics.TypeTheoretic.GSign.cont {Phon Cont : Type} : GSign Phon Cont → Cont

Equations

• (Semantics.TypeTheoretic.GSign.mk e cat daughters cont).cont = cont

def Semantics.TypeTheoretic.GSign.isLexical {Phon Cont : Type} (s : GSign Phon Cont) : Bool

Whether a sign is lexical (NoDaughters = empty daughter string).

Equations

• s.isLexical = s.daughters.isEmpty

def Semantics.TypeTheoretic.GSign.toTTRSign {Phon Cont : Type} (s : GSign Phon Cont) : TTRSign Phon Cont

Project out the Ch2 sign (dropping syntactic structure).

Equations

• s.toTTRSign = { phon := s.phon, cont := s.cont }

def Semantics.TypeTheoretic.lexSign {Phon Cont : Type} (phon : Phon) (c : Cat) (cont : Cont) : GSign Phon Cont

Create a lexical sign (no daughters). §3.3, ex (18).

Equations

• Semantics.TypeTheoretic.lexSign phon c cont = Semantics.TypeTheoretic.GSign.mk phon c [] cont

theorem Semantics.TypeTheoretic.lexSign_isLexical {Phon Cont : Type} (phon : Phon) (c : Cat) (cont : Cont) : (lexSign phon c cont).isLexical = true

Lexical signs have no daughters by construction.

§ 3.3 Phrase structure rules

structure Semantics.TypeTheoretic.PSRule : Type

A phrase structure rule: mother category and ordered daughter categories. §3.3, ex (27).

• mother : Cat
• daughters : List Cat

def Semantics.TypeTheoretic.instReprPSRule.repr : PSRule → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprPSRule : Repr PSRule

Equations

• Semantics.TypeTheoretic.instReprPSRule = { reprPrec := Semantics.TypeTheoretic.instReprPSRule.repr }

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqPSRule : DecidableEq PSRule

Equations

• Semantics.TypeTheoretic.instDecidableEqPSRule = Semantics.TypeTheoretic.instDecidableEqPSRule.decEq

def Semantics.TypeTheoretic.instDecidableEqPSRule.decEq (x✝ x✝¹ : PSRule) : Decidable (x✝ = x✝¹)

Equations

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

def Semantics.TypeTheoretic.rule_S_NP_VP : PSRule

S → NP VP. §3.3, ex (29).

Equations

• Semantics.TypeTheoretic.rule_S_NP_VP = { mother := Semantics.TypeTheoretic.Cat.s, daughters := [Semantics.TypeTheoretic.Cat.np, Semantics.TypeTheoretic.Cat.vp] }

def Semantics.TypeTheoretic.rule_NP_Det_N : PSRule

NP → Det N.

Equations

• Semantics.TypeTheoretic.rule_NP_Det_N = { mother := Semantics.TypeTheoretic.Cat.np, daughters := [Semantics.TypeTheoretic.Cat.det, Semantics.TypeTheoretic.Cat.n] }

def Semantics.TypeTheoretic.rule_VP_V_NP : PSRule

VP → V NP.

Equations

• Semantics.TypeTheoretic.rule_VP_V_NP = { mother := Semantics.TypeTheoretic.Cat.vp, daughters := [Semantics.TypeTheoretic.Cat.v, Semantics.TypeTheoretic.Cat.np] }

def Semantics.TypeTheoretic.fragmentRules : List PSRule

The complete set of phrase structure rules for Cooper's fragment.

Equations

• Semantics.TypeTheoretic.fragmentRules = [Semantics.TypeTheoretic.rule_S_NP_VP, Semantics.TypeTheoretic.rule_NP_Det_N, Semantics.TypeTheoretic.rule_VP_V_NP]

theorem Semantics.TypeTheoretic.fragment_rules_binary (r : PSRule) : r ∈ fragmentRules → r.daughters.length = 2

All fragment rules are binary (two daughters).

def Semantics.TypeTheoretic.ruleDaughters {Phon Cont : Type} (rule : PSRule) (phon : Phon) (cont : Cont) (daus : List (GSign Phon Cont)) : GSign Phon Cont

Build a phrasal sign from a rule and daughters.

Equations

• Semantics.TypeTheoretic.ruleDaughters rule phon cont daus = Semantics.TypeTheoretic.GSign.mk phon rule.mother daus cont

theorem Semantics.TypeTheoretic.ruleDaughters_not_lexical {Phon Cont : Type} (rule : PSRule) (phon : Phon) (cont : Cont) (d : GSign Phon Cont) (ds : List (GSign Phon Cont)) : (ruleDaughters rule phon cont (d :: ds)).isLexical = false

Phrasal signs (with at least one daughter) are not lexical.

§ 3.4 Property and quantifier types

§3.4 introduces the semantic type hierarchy:

• Ppty = [x:Ind] → RecType: maps individuals to situation types (properties)
• Quant = Ppty → RecType: maps properties to types (quantifiers)

These are the TTR analogues of Montague's ⟨e,t⟩ and ⟨⟨e,t⟩,t⟩.

@[reducible, inline]

abbrev Semantics.TypeTheoretic.Ppty (E : Type) : Type 1

A property type: maps an individual to a type of situations. §3.4, ex (30): Ppty = [x:Ind] → RecType. Alias for PredType E. Montague type: ⟨e,t⟩.

Equations

• Semantics.TypeTheoretic.Ppty E = Semantics.TypeTheoretic.PredType E

@[reducible, inline]

abbrev Semantics.TypeTheoretic.Quant (E : Type) : Type 1

A quantifier type: maps a property to a type. §3.4: Quant = Ppty → RecType. Montague type: ⟨⟨e,t⟩,t⟩ — a generalized quantifier.

Equations

• Semantics.TypeTheoretic.Quant E = (Semantics.TypeTheoretic.Ppty E → Type)

theorem Semantics.TypeTheoretic.ppty_eq_predType (E : Type) : Ppty E = PredType E

Bridge: TTR Ppty is structurally identical to PredType from §1.4.1.

§ 3.4 Compositional semantics functions

def Semantics.TypeTheoretic.semCommonNoun {E : Type} (p : E → Type) : Ppty E

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

Equations

• Semantics.TypeTheoretic.semCommonNoun p = p

def Semantics.TypeTheoretic.semPropName {E : Type} (a : E) : Quant E

Proper name content as a generalized quantifier. §3.4, ex (33): SemPropName(a) = λP:Ppty. P([x=a]).

Equations

• Semantics.TypeTheoretic.semPropName a P = P a

structure Semantics.TypeTheoretic.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 Semantics.TypeTheoretic.semIndefArt {E : Type} (restr : Ppty E) : Quant E

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

Equations

• Semantics.TypeTheoretic.semIndefArt restr scope = Semantics.TypeTheoretic.ExistWitness E restr scope

def Semantics.TypeTheoretic.semBe {E : Type} (Q : Quant E) : Ppty E

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

Equations

• Semantics.TypeTheoretic.semBe Q x = Q fun (y : E) => Semantics.TypeTheoretic.propT (x = y)

§ 3.4 Property extension and existential quantification

def Semantics.TypeTheoretic.propExtension {E : Type} (P : Ppty E) (a : E) : Prop

Property extension: whether an individual has property P. §3.4, ex (46).

Equations

• Semantics.TypeTheoretic.propExtension P a = Nonempty (P a)

def Semantics.TypeTheoretic.existPQ {E : Type} (P Q : Ppty E) : Prop

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

Equations

• Semantics.TypeTheoretic.existPQ P Q = ∃ (a : E), Nonempty (P a) ∧ Nonempty (Q a)

theorem Semantics.TypeTheoretic.existPQ_iff_witness {E : Type} (P Q : Ppty E) : existPQ P Q ↔ Nonempty (ExistWitness E P Q)

existPQ is equivalent to inhabitation of ExistWitness.

theorem Semantics.TypeTheoretic.existPQ_eq_exists {E : Type} (P Q : E → Prop) : (existPQ (fun (e : E) => propT (P e)) fun (e : E) => propT (Q e)) ↔ ∃ (a : E), P a ∧ Q a

Bridge: TTR existPQ reduces to classical ∃ when properties are Prop-valued.

Proposition granularity: Set W vs TTR types

[CCGS25] §2 argue that the choice of proposition type determines what distinctions a semantic theory can make. We formalize the granularity hierarchy:

IType (finest) > Type (medium) > Set W (coarsest)

• Set W identifies all propositions with the same truth conditions
• TTR types distinguish propositions that are merely co-extensional
• IType adds intensional identity (name-based distinction)

The key consequence: attitude verbs that need to distinguish Hesperus-beliefs from Phosphorus-beliefs cannot use Set W — they need IType.

theorem Semantics.TypeTheoretic.prop_collapses_intensional_distinctions (W : Type u_1) : ∃ (T₁ : IType) (T₂ : IType), ¬T₁.intEq T₂ ∧ ∀ (embed : IType → Set W), (∀ (T : IType) (w : W), embed T w ↔ Nonempty T.carrier) → ∀ (w : W), embed T₁ w ↔ embed T₂ w

Possible-worlds propositions collapse TTR distinctions: two ITypes with different names but same carrier map to the same Prop. This is why Set W is too coarse for attitude reports.

theorem Semantics.TypeTheoretic.ttr_strictly_finer_than_worlds : (∃ (T₁ : IType) (T₂ : IType), T₁.extEquiv T₂ ∧ ¬T₁.intEq T₂) ∧ ∀ (W : Type) (p q : Set W), p = q → ∀ (w : W), p w ↔ q w

TTR types are strictly finer than Set W: there exist types that TTR distinguishes but Set W cannot. (This is ext_equiv_not_implies_int_eq restated in terms of the granularity hierarchy.)