Cooper (2023) Ch. 6 — Modality and Intensionality without Possible Worlds

[Coo23] [Aus61] [Bar89] [Kra91]

[Coo23] Chapter 6 extends the modal type system framework from Ch1 with Prop-valued modal systems, topoi (replacing accessibility relations), Box/Diamond type constructors, Austinian/Russellian propositions, believe/know via long-term memory, points of view, and intensional transitive verbs.

This study formalises Ch. 6 directly. It was formerly substrate at Semantics/TypeTheoretic/Modality.lean but is genuinely a single-paper Cooper-textbook replication: only ChatzikyriakidisEtAl2025 (intentional identity) consumed it externally.

Layer 2 — Semantics: ModalSystem (Ch6, Prop) + bridge to ModalTypeSystem (Ch1, Bool), Topos ≃ Parametric Type (unified), NecTopos, PossTopos, Box/Diamond.

Bridges:

• ModalTypeSystem ↔ ModalSystem (Bool ↔ Prop)
• ModalSystem ↔ AccessRel (Kripke accessibility)
• know = believe + veridicality (abstract doxastic bridge)
• Topos → induced necessity/possibility (abstract Kratzer bridge)

§ 6.2–6.3 Modal type systems — extended

Chapter 1 introduced ModalTypeSystem (Def 54) with Bool-valued predicate assignments. Chapter 6 builds on this with four modal notions, each in restrictive (all possibilities share the type) and inclusive (some possibility has the type) variants.

A modal system of complex types TYPE_MC is a family of type systems indexed by "possibilities" where basic types and predicates are shared but witness assignments vary. §6.3, (1)–(4).

structure Cooper2023Ch6.Possibility (Ty Obj : Type) : Type

A possibility in a modal type system: an assignment of witnesses to types. Each possibility maps types (represented as Ty) to their set of witnesses. §6.3: possibilities differ in which objects witness which types.

The available field tracks which types are recognized in this possibility. Not every type need exist in every possibility — a type can be absent from a possibility entirely, which is distinct from being present but unwitnessed. This distinction is what separates inclusive from restrictive modal notions.

• available : Ty → Prop

  Which types are recognized (available) in this possibility. A type may be available without having witnesses (empty extension).

• witnesses : Ty → Obj → Prop

  Whether object a witnesses type T in this possibility

structure Cooper2023Ch6.ModalSystem (Ty Obj : Type) : Type 1

A modal system of complex types: a family of possibilities. §6.3, Def A9: TYPE_MC = ⟨Type_M, BType, ⟨PType_M⟩,...⟩_{M ∈ M}. The possibilities share the same types but differ in witness assignments.

• Poss : Type

  The index type for possibilities

• poss : self.Poss → Possibility Ty Obj

  The family of possibilities

def Cooper2023Ch6.ModalSystem.hasType {Ty Obj : Type} (ms : ModalSystem Ty Obj) (p : ms.Poss) (T : Ty) : Prop

Whether type T is available (recognized) in possibility p. §6.3: T ∈ Type_M means T is a type in the system associated with M.

Equations

• ms.hasType p T = (ms.poss p).available T

def Cooper2023Ch6.ModalSystem.ext {Ty Obj : Type} (ms : ModalSystem Ty Obj) (p : ms.Poss) (T : Ty) : Obj → Prop

Extension of a type in a possibility: the set of witnesses. §6.3, (1a): {a | a :{TYPE{M_i}} T}.

Equations

• ms.ext p T = (ms.poss p).witnesses T

Restrictive modal notions (§6.3, (1)/(3))

These quantify over ALL possibilities.

def Cooper2023Ch6.nec_equiv_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : Prop

Restrictive necessary equivalence: T₁ ≈_r T₂ iff they have the same extension in all possibilities. §6.3, (1a).

Equations

• Cooper2023Ch6.nec_equiv_r ms T₁ T₂ = ∀ (p : ms.Poss), ms.ext p T₁ = ms.ext p T₂

def Cooper2023Ch6.nec_subtype_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : Prop

Restrictive subtype: T₁ ⊑_r T₂ iff T₁'s extension ⊆ T₂'s in all possibilities. §6.3, (1b).

Equations

• Cooper2023Ch6.nec_subtype_r ms T₁ T₂ = ∀ (p : ms.Poss) (a : Obj), ms.ext p T₁ a → ms.ext p T₂ a

def Cooper2023Ch6.nec_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Restrictive necessity: T is necessary iff it has witnesses in all possibilities. §6.3, (1c).

Equations

• Cooper2023Ch6.nec_r ms T = ∀ (p : ms.Poss), ∃ (a : Obj), ms.ext p T a

def Cooper2023Ch6.poss_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Restrictive possibility: T is possible iff it has witnesses in some possibility. §6.3, (1d).

Equations

• Cooper2023Ch6.poss_r ms T = ∃ (p : ms.Poss) (a : Obj), ms.ext p T a

Inclusive modal notions (§6.3, (2)/(4))

These quantify over possibilities where the type is available (recognized in the type system), not merely over those where it has witnesses. This distinction is the key difference from the previous (buggy) version, which used "has witnesses" as the guard — making nec_i a tautology.

§6.3, (2): "T ∈ Type_M" means the type is available in possibility M, which is strictly weaker than having witnesses there.

def Cooper2023Ch6.nec_equiv_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : Prop

Inclusive necessary equivalence: T₁ ≈_i T₂ iff for all possibilities where both types are available, they have the same extension. §6.3, (2a).

Equations

• Cooper2023Ch6.nec_equiv_i ms T₁ T₂ = ∀ (p : ms.Poss), ms.hasType p T₁ → ms.hasType p T₂ → ms.ext p T₁ = ms.ext p T₂

def Cooper2023Ch6.nec_subtype_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : Prop

Inclusive subtype: T₁ ⊑_i T₂ iff for all possibilities where both are available, T₁'s extension ⊆ T₂'s. §6.3, (2b).

Equations

• Cooper2023Ch6.nec_subtype_i ms T₁ T₂ = ∀ (p : ms.Poss), ms.hasType p T₁ → ms.hasType p T₂ → ∀ (a : Obj), ms.ext p T₁ a → ms.ext p T₂ a

def Cooper2023Ch6.nec_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Inclusive necessity: T is necessary iff it has witnesses in all possibilities where T is available. §6.3, (2c).

This is strictly weaker than nec_r: a type can be inclusively necessary without being restrictively necessary, if there are possibilities where the type is simply not available.

Equations

• Cooper2023Ch6.nec_i ms T = ∀ (p : ms.Poss), ms.hasType p T → ∃ (a : Obj), ms.ext p T a

def Cooper2023Ch6.poss_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Inclusive possibility: T is possible iff some possibility both has T available and has a witness. §6.3, (2d).

Equations

• Cooper2023Ch6.poss_i ms T = ∃ (p : ms.Poss), ms.hasType p T ∧ ∃ (a : Obj), ms.ext p T a

theorem Cooper2023Ch6.restrictive_subtype_implies_inclusive {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : nec_subtype_r ms T₁ T₂ → nec_subtype_i ms T₁ T₂

Restrictive ⊑_r entails inclusive ⊑_i. §6.3, paragraph after (2): "if any of the restrictive definitions holds... then the corresponding inclusive definition will also hold."

theorem Cooper2023Ch6.restrictive_nec_implies_inclusive {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : nec_r ms T → nec_i ms T

Restrictive necessity entails inclusive necessity.

theorem Cooper2023Ch6.poss_i_implies_poss_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : poss_i ms T → poss_r ms T

Inclusive possibility implies restrictive possibility (drop the availability condition).

theorem Cooper2023Ch6.poss_r_implies_poss_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) (hcoh : ∀ (p : ms.Poss) (a : Obj), ms.ext p T a → ms.hasType p T) : poss_r ms T → poss_i ms T

Restrictive possibility implies inclusive possibility when witnessing implies availability (the standard coherence condition).

Bridge: ModalTypeSystem (Ch1) ↔ ModalSystem (Ch6)

Ch1's ModalTypeSystem is Bool-valued (finite, decidable). Ch6's ModalSystem is Prop-valued (more general). These conversion functions connect the two formalizations.

def Semantics.TypeTheoretic.ModalTypeSystem.toModalSystem {W Pred : Type} (mts : ModalTypeSystem W Pred) (Obj : Type) : Cooper2023Ch6.ModalSystem Pred Obj

Embed a Ch1 Bool-valued modal type system into a Ch6 Prop-valued modal system. Each predicate becomes a type; an object witnesses the type iff mts w P = true. All predicates are available in all possibilities (Bool-valued systems don't distinguish availability from witnessing).

Equations

• mts.toModalSystem Obj = { Poss := W, poss := fun (w : W) => { available := fun (x : Pred) => True, witnesses := fun (P : Pred) (x : Obj) => mts w P = true } }

def Cooper2023Ch6.ModalSystem.toModalTypeSystem {Ty Obj : Type} (ms : ModalSystem Ty Obj) [dec : (p : ms.Poss) → (T : Ty) → Decidable (∃ (a : Obj), ms.ext p T a)] : Semantics.TypeTheoretic.ModalTypeSystem ms.Poss Ty

Project a Ch6 Prop-valued modal system back to Ch1 Bool when witnesses are decidable. Requires a decision procedure for whether each type has a witness.

Equations

• ms.toModalTypeSystem p T = if ∃ (a : Obj), ms.ext p T a then true else false

theorem Semantics.TypeTheoretic.ModalTypeSystem.roundtrip {W Pred : Type} (mts : ModalTypeSystem W Pred) (w : W) (P : Pred) : ((mts.toModalSystem Unit).poss w).witnesses P () ↔ mts w P = true

Roundtrip: embedding then projecting back preserves the Bool-valued system.

Bridge: ModalSystem ↔ Intensional.BAccessRel

A Cooper modal system induces a Kripke accessibility relation for each type T: R_T(p₁, p₂) holds iff every witness of T in p₁ is also a witness in p₂. This connects TTR's type-indexed modality to standard Kripke semantics.

def Cooper2023Ch6.ModalSystem.toAccessRel {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : ms.Poss → ms.Poss → Prop

Given a type T, derive a Kripke accessibility relation from a modal system. R_T(p₁, p₂) iff the extension of T at p₂ includes the extension at p₁. This makes □T at p = "T has witnesses in all R_T-accessible possibilities".

Equations

• ms.toAccessRel T p₁ p₂ = ∀ (a : Obj), ms.ext p₁ T a → ms.ext p₂ T a

theorem Cooper2023Ch6.nec_r_iff_forall_exists {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : nec_r ms T ↔ ∀ (p : ms.Poss), ∃ (a : Obj), ms.ext p T a

TTR necessity (nec_r) for type T is equivalent to: for all possibilities, T has witnesses. This is □T evaluated at the universal frame.

theorem Cooper2023Ch6.poss_r_iff_exists {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : poss_r ms T ↔ ∃ (p : ms.Poss) (a : Obj), ms.ext p T a

TTR possibility (poss_r) for type T is equivalent to: some possibility has a witness of T. This is ◇T evaluated at the universal frame.

theorem Cooper2023Ch6.ModalSystem.toAccessRel_refl {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) (p : ms.Poss) : ms.toAccessRel T p p

The derived accessibility relation is reflexive (every possibility includes its own witnesses).

§ 6.4 Box and Diamond type constructors

If T is a type, then □_r T, □_i T, ◇_r T, ◇_i T are types. □T is non-empty iff T is necessary; ◇T is non-empty iff T is possible. §6.4, (5)–(11).

def Cooper2023Ch6.BoxR {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Box type (necessity): □T is inhabited iff T is necessary in the modal system. §6.4, (5)–(7). A witness of □T is a proof that T has witnesses in all (restrictive) or relevant (inclusive) possibilities.

Equations

• Cooper2023Ch6.BoxR ms T = Cooper2023Ch6.nec_r ms T

def Cooper2023Ch6.BoxI {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Equations

• Cooper2023Ch6.BoxI ms T = Cooper2023Ch6.nec_i ms T

def Cooper2023Ch6.DiamondR {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Diamond type (possibility): ◇T is inhabited iff T is possible. §6.4, (5), (9).

Equations

• Cooper2023Ch6.DiamondR ms T = Cooper2023Ch6.poss_r ms T

def Cooper2023Ch6.DiamondI {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Equations

• Cooper2023Ch6.DiamondI ms T = Cooper2023Ch6.poss_i ms T

theorem Cooper2023Ch6.BoxR_implies_BoxI {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : BoxR ms T → BoxI ms T

□_r T → □_i T (restrictive box implies inclusive box).

theorem Cooper2023Ch6.DiamondI_implies_DiamondR {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : DiamondI ms T → DiamondR ms T

◇_i T → ◇_r T (inclusive diamond implies restrictive diamond).

theorem Cooper2023Ch6.DiamondR_implies_DiamondI {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) (hcoh : ∀ (p : ms.Poss) (a : Obj), ms.ext p T a → ms.hasType p T) : DiamondR ms T → DiamondI ms T

◇_r T → ◇_i T when witnessing implies availability.

theorem Cooper2023Ch6.BoxR_implies_DiamondR {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) (hne : Nonempty ms.Poss) : BoxR ms T → DiamondR ms T

□_r T → ◇_r T when the modal system has at least one possibility. The D axiom of modal logic.

§ 6.4 Topoi

A topos maps situations (of a background type) to types (the foreground). Topoi replace accessibility relations between possible worlds: they encode rules (epistemic, deontic) that license inferences from situations to types.

§6.4, (20): τ : Topos has bg : Type and fg : (bg → Type). τ(s) = τ.fg(s).

@[reducible, inline]

abbrev Cooper2023Ch6.Topos : Type (u_1 + 1)

A topos: a dependent type mapping background situations to foreground types. §6.4, (20): if τ : Topos, then τ has Bg : Type, fg : (Bg → Type). Topoi replace Kratzer's conversational backgrounds (modal base + ordering source) in the analysis of modality.

Definitionally Parametric Type (Discourse.lean §4.3): Topos's background- plus-foreground shape and Parametric Type's Bg/fg fields coincide. We adopt the abbrev so Cooper's §6.4 modality machinery and the §4.3 parametric content pattern share one underlying record.

Equations

• Cooper2023Ch6.Topos = Semantics.TypeTheoretic.Parametric Type

def Cooper2023Ch6.Topos.apply (τ : Topos) (s : τ.Bg) : Type

Apply a topos to a background situation: τ(s) = τ.fg(s). §6.4: τ(s) to represent τ.fg(s).

Equations

• τ.apply s = τ.fg s

Action rules with topoi (§6.4, (21)–(22))

Topoi are used with action rules:

• Epistemically: if s : τ.Bg, then infer there is something of type τ(s)
• Deontically: if s : τ.Bg, then an agent is allowed/obliged to create τ(s)

def Cooper2023Ch6.Topos.epistemicInference (τ : Topos) (s : τ.Bg) : Prop

Epistemic use of a topos: from a situation of the background type, infer the existence of something of the foreground type. §6.4, (21).

Equations

• τ.epistemicInference s = Nonempty (τ.fg s)

inductive Cooper2023Ch6.DeonticKind : Type

Deontic modality kind: affordance (allowed) vs obligation (obliged).

• affordance : DeonticKind
• obligation : DeonticKind

def Cooper2023Ch6.instReprDeonticKind.repr : DeonticKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cooper2023Ch6.instReprDeonticKind : Repr DeonticKind

Equations

• Cooper2023Ch6.instReprDeonticKind = { reprPrec := Cooper2023Ch6.instReprDeonticKind.repr }

@[implicit_reducible]

instance Cooper2023Ch6.instDecidableEqDeonticKind : DecidableEq DeonticKind

Equations

• Cooper2023Ch6.instDecidableEqDeonticKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Necessity and possibility with topoi (§6.4, (23)–(24), version 4)

The final version of nec/poss uses topoi instead of an "ideal" type:

• nec(T, B, τ): s witnesses T's necessity w.r.t. background B and topos τ iff s :_p B, B ⊑ τ.Bg, and τ(s) ⊑ T
• poss(T, B, τ): s witnesses T's possibility w.r.t. B and τ iff s :_p B, B ⊑ τ.Bg, and τ(s) is compatible with T

@[reducible, inline]

abbrev Cooper2023Ch6.modalSubtype (B T : Type) : Prop

Subtyping in a modal type system: B ⊑_T T means all witnesses of B are also witnesses of T. §6.4: B ⊑_𝕋 τ.Bg.

Equations

• Cooper2023Ch6.modalSubtype B T = ∀ (x : B), Nonempty T

def Cooper2023Ch6.Compatible (T₁ T₂ : Type) : Prop

Compatibility: T₁ ⊤⊤ T₂ iff their meet is non-empty — there exists something of both types simultaneously. §6.4, (17).

Equations

• Cooper2023Ch6.Compatible T₁ T₂ = Nonempty (T₁ × T₂)

structure Cooper2023Ch6.NecTopos (T B : Type) (τ : Topos) : Type u_1

Witness condition for necessity with topoi (version 4). §6.4, (23): s :_p nec(T, B, τ) iff s :_p B, B ⊑_𝕋 τ.Bg, and τ(s) ⊑_𝕋 T.

We model this as: given a background witness s, a proof that the background subtypes the topos domain, and a coercion from s to the topos domain, the foreground τ(coerce(s)) is a subtype of T.

• sit : B

  A witness of the background type

• coerce : B → τ.Bg

  Coercion from background to topos domain

• sub : τ.fg (self.coerce self.sit) → T

  The topos applied at the coerced situation subtypes T

structure Cooper2023Ch6.PossTopos (T B : Type) (τ : Topos) : Type u_1

Witness condition for possibility with topoi (version 4). §6.4, (24): s :_p poss(T, B, τ) iff s :_p B, B ⊑_𝕋 τ.Bg, and τ(s) ⊤⊤ T. Possibility requires compatibility rather than subtyping.

• sit : B

  A witness of the background type

• coerce : B → τ.Bg

  Coercion from background to topos domain

• compat : Compatible (τ.fg (self.coerce self.sit)) T

  The topos applied at the coerced situation is compatible with T

def Cooper2023Ch6.necTopos_implies_possTopos {T B : Type} {τ : Topos} (hn : NecTopos T B τ) (hne : Nonempty (τ.fg (hn.coerce hn.sit))) : PossTopos T B τ

Necessity implies possibility (version 4): if T is necessary w.r.t. B and τ, and the topos foreground at the situation is non-empty, then T is possible.

Equations

• Cooper2023Ch6.necTopos_implies_possTopos hn hne = { sit := hn.sit, coerce := hn.coerce, compat := ⋯ }

Abstract bridge: Topos ↔ conversational background

Cooper's topoi parallel Kratzer's conversational backgrounds:

• A topos τ maps situations (bg) to types (fg): τ : bg → Type
• A conversational background f maps worlds to prop sets: f : W → Set Prop

Both serve as the contextual parameter determining modal flavor. Cooper explicitly notes (§6.4): "Topoi replace accessibility relations between possible worlds... encoding rules that license inferences."

The structural correspondence:

• Topos bg ↔ conversational background's domain (situations ↔ worlds)
• Topos fg ↔ propositions in the modal base (both constrain what's possible)
• NecTopos ↔ □ under a particular modal base
• PossTopos ↔ ◇ under a particular modal base

Full bridge importing Kratzer.lean is deferred to Theories/TTR/.

def Cooper2023Ch6.Topos.inducedNec (τ : Topos) : Prop

A topos induces a notion of necessity: for all situations of background type, the foreground type is inhabited. This parallels Kratzer's □ under a modal base.

Equations

• τ.inducedNec = ∀ (s : τ.Bg), Nonempty (τ.fg s)

def Cooper2023Ch6.Topos.inducedPoss (τ : Topos) : Prop

A topos induces possibility: some situation of background type has an inhabited foreground. This parallels Kratzer's ◇ under a modal base.

Equations

• τ.inducedPoss = ∃ (s : τ.Bg), Nonempty (τ.fg s)

theorem Cooper2023Ch6.Topos.nec_implies_poss (τ : Topos) (hne : Nonempty τ.Bg) (hn : τ.inducedNec) : τ.inducedPoss

Topos-induced necessity implies possibility (when the background is inhabited). The topos analogue of the D axiom (□p → ◇p).

Topos ↔ ModalSystem bridge

A topos τ : (bg → Type) induces a single-type modal system where:

• Possibilities are the situations (τ.Bg)
• There is one distinguished type (Unit)
• A possibility s has the type witnessed iff τ.fg(s) is inhabited

This connects Cooper's topos-based modality to the ModalSystem framework from §6.3. The induced accessibility relation is universal — every situation is accessible from every other — because topoi encode what follows at each situation rather than which situations are accessible. This is the formal content of Cooper's claim (§6.4) that "topoi replace accessibility relations between possible worlds."

def Cooper2023Ch6.Topos.toModalSystem (τ : Topos) : ModalSystem Unit Unit

Convert a topos to a single-type modal system. Possibilities are the background situations; the single type is witnessed at possibility s iff τ.fg(s) is inhabited.

Equations

• τ.toModalSystem = { Poss := τ.Bg, poss := fun (s : τ.Bg) => { available := fun (x : Unit) => True, witnesses := fun (x x_1 : Unit) => Nonempty (τ.fg s) } }

theorem Cooper2023Ch6.Topos.inducedNec_iff_nec_r (τ : Topos) : τ.inducedNec ↔ nec_r τ.toModalSystem ()

Topos-induced necessity = restrictive necessity in the derived modal system. ∀ s, Nonempty (τ.fg s) ↔ nec_r (τ.toModalSystem) ().

theorem Cooper2023Ch6.Topos.inducedPoss_iff_poss_r (τ : Topos) : τ.inducedPoss ↔ poss_r τ.toModalSystem ()

Topos-induced possibility = restrictive possibility in the derived modal system. ∃ s, Nonempty (τ.fg s) ↔ poss_r (τ.toModalSystem) ().

theorem Cooper2023Ch6.Topos.allAvailable (τ : Topos) (s : τ.Bg) : τ.toModalSystem.hasType s ()

All types are available in every possibility of a topos-derived system. This means inclusive and restrictive modal notions coincide for topoi — the distinction only matters when some types are absent from some possibilities.

theorem Cooper2023Ch6.Topos.nec_r_iff_nec_i (τ : Topos) : nec_r τ.toModalSystem () ↔ nec_i τ.toModalSystem ()

For a topos-derived modal system, nec_r = nec_i (restrictive = inclusive). Since every type is available in every possibility, the inclusive guard is vacuous.

theorem Cooper2023Ch6.Topos.accessRel_refl (τ : Topos) (s : τ.Bg) : τ.toModalSystem.toAccessRel () s s

The accessibility relation induced by a topos is reflexive: every situation is accessible from itself.

theorem Cooper2023Ch6.Topos.accessRel_characterization (τ : Topos) (s₁ s₂ : τ.Bg) : τ.toModalSystem.toAccessRel () s₁ s₂ ↔ Nonempty (τ.fg s₁) → Nonempty (τ.fg s₂)

The accessibility relation induced by a topos is: s₁ R s₂ iff whenever τ.fg(s₁) is inhabited, so is τ.fg(s₂). This captures Cooper's insight (§6.4) that the modal content is carried by the topos foreground rather than by the accessibility structure — the relation between situations is derived from the type-theoretic content, not stipulated as a primitive.

Broccoli example (§6.4, (25)–(31))

"Mary should eat her broccoli" — deontic (children must eat food on their plate) vs bouletic (children eat food they love). §6.4.

Two topoi τ₁ and τ₂ with the same foreground (eat) but different backgrounds:

• τ₁ (deontic): child has food on plate → child eats that food
• τ₂ (bouletic): child loves food → child eats that food

inductive Cooper2023Ch6.BrocInd : Type

Individuals in the broccoli scenario.

• broccoli : BrocInd
• mary : BrocInd
• plate : BrocInd

@[implicit_reducible]

instance Cooper2023Ch6.instReprBrocInd : Repr BrocInd

Equations

• Cooper2023Ch6.instReprBrocInd = { reprPrec := Cooper2023Ch6.instReprBrocInd.repr }

def Cooper2023Ch6.instReprBrocInd.repr : BrocInd → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cooper2023Ch6.instDecidableEqBrocInd : DecidableEq BrocInd

Equations

• Cooper2023Ch6.instDecidableEqBrocInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch6.isBroccoli : BrocInd → Prop

Predicates for the broccoli scenario.

Equations

• Cooper2023Ch6.isBroccoli x✝ = (x✝ = Cooper2023Ch6.BrocInd.broccoli)

def Cooper2023Ch6.isChild : BrocInd → Prop

Equations

• Cooper2023Ch6.isChild x✝ = (x✝ = Cooper2023Ch6.BrocInd.mary)

def Cooper2023Ch6.isPlate : BrocInd → Prop

Equations

• Cooper2023Ch6.isPlate x✝ = (x✝ = Cooper2023Ch6.BrocInd.plate)

def Cooper2023Ch6.isFood : BrocInd → Prop

Equations

• Cooper2023Ch6.isFood x✝ = (x✝ = Cooper2023Ch6.BrocInd.broccoli)

def Cooper2023Ch6.have_ : BrocInd → BrocInd → Prop

Relations in the broccoli scenario.

Equations

• Cooper2023Ch6.have_ y z = (y = Cooper2023Ch6.BrocInd.mary ∧ z = Cooper2023Ch6.BrocInd.plate)

def Cooper2023Ch6.on_ : BrocInd → BrocInd → Prop

Equations

• Cooper2023Ch6.on_ x z = (x = Cooper2023Ch6.BrocInd.broccoli ∧ z = Cooper2023Ch6.BrocInd.plate)

def Cooper2023Ch6.love_ : BrocInd → BrocInd → Prop

Equations

• Cooper2023Ch6.love_ y x = (y = Cooper2023Ch6.BrocInd.mary ∧ x = Cooper2023Ch6.BrocInd.broccoli)

def Cooper2023Ch6.eat_ : BrocInd → BrocInd → Prop

Equations

• Cooper2023Ch6.eat_ y x = (y = Cooper2023Ch6.BrocInd.mary ∧ x = Cooper2023Ch6.BrocInd.broccoli)

structure Cooper2023Ch6.BroccoliBase : Type

The base situation type B for "Mary should eat her broccoli". §6.4, (26): [x=b:Ind, c₁:broccoli(x), y=m:Ind, c₂:child(y), z=p:Ind, c₃:plate(z), e₁:have(y,z), e₂:on(x,z), e₃:love(y,x)]

• x : BrocInd
• hx : isBroccoli self.x
• y : BrocInd
• hy : isChild self.y
• z : BrocInd
• hz : isPlate self.z
• e₁ : have_ self.y self.z
• e₂ : on_ self.x self.z
• e₃ : love_ self.y self.x

structure Cooper2023Ch6.DeonticBg : Type

The background type for τ₁ (deontic): food on child's plate. §6.4, (28a) background.

• x : BrocInd
• c₁ : isFood self.x
• y : BrocInd
• c₂ : isChild self.y
• z : BrocInd
• c₃ : isPlate self.z
• e₁ : have_ self.y self.z
• e₂ : on_ self.x self.z

structure Cooper2023Ch6.BouleticBg : Type

The background type for τ₂ (bouletic): food the child loves. §6.4, (28b) background.

• x : BrocInd
• c₁ : isFood self.x
• y : BrocInd
• c₂ : isChild self.y
• e₃ : love_ self.y self.x

def Cooper2023Ch6.eatType (y x : BrocInd) : Type

The eating type (foreground of both topoi).

Equations

• Cooper2023Ch6.eatType y x = PLift (Cooper2023Ch6.eat_ y x)

def Cooper2023Ch6.τ_deontic : Topos

Topos τ₁ (deontic): children eat food on their plate. §6.4, (28a).

Equations

• Cooper2023Ch6.τ_deontic = { Bg := Cooper2023Ch6.DeonticBg, fg := fun (r : Cooper2023Ch6.DeonticBg) => Cooper2023Ch6.eatType r.y r.x }

def Cooper2023Ch6.τ_bouletic : Topos

Topos τ₂ (bouletic): children eat food they love. §6.4, (28b).

Equations

• Cooper2023Ch6.τ_bouletic = { Bg := Cooper2023Ch6.BouleticBg, fg := fun (r : Cooper2023Ch6.BouleticBg) => Cooper2023Ch6.eatType r.y r.x }

def Cooper2023Ch6.brocBase : BroccoliBase

A concrete base situation: broccoli on Mary's plate, Mary loves broccoli.

Equations

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

def Cooper2023Ch6.deonticBg : DeonticBg

The deontic background witnesses: food on plate.

Equations

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

def Cooper2023Ch6.bouleticBg : BouleticBg

The bouletic background witnesses: child loves food.

Equations

• Cooper2023Ch6.bouleticBg = { x := Cooper2023Ch6.BrocInd.broccoli, c₁ := ⋯, y := Cooper2023Ch6.BrocInd.mary, c₂ := ⋯, e₃ := Cooper2023Ch6.brocBase._proof_3 }

def Cooper2023Ch6.broccoliDeonticNec : NecTopos (PLift (eat_ BrocInd.mary BrocInd.broccoli)) BroccoliBase τ_deontic

Deontic reading: nec([e:eat(m,b)], T_broc, τ₁). §6.4, (29a): the deontic topos makes eating necessary.

Equations

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

def Cooper2023Ch6.broccolicBouleticNec : NecTopos (PLift (eat_ BrocInd.mary BrocInd.broccoli)) BroccoliBase τ_bouletic

Bouletic reading: nec([e:eat(m,b)], T_broc, τ₂). §6.4, (29b): the bouletic topos also makes eating necessary.

Equations

• Cooper2023Ch6.broccolicBouleticNec = { sit := Cooper2023Ch6.brocBase, coerce := fun (b : Cooper2023Ch6.BroccoliBase) => { x := b.x, c₁ := ⋯, y := b.y, c₂ := ⋯, e₃ := ⋯ }, sub := id }

theorem Cooper2023Ch6.broccoli_both_topoi_yield_eat : (∃ (x : NecTopos (PLift (eat_ BrocInd.mary BrocInd.broccoli)) BroccoliBase τ_deontic), True) ∧ ∃ (x : NecTopos (PLift (eat_ BrocInd.mary BrocInd.broccoli)) BroccoliBase τ_bouletic), True

Both topoi yield the same eating conclusion, but differ in their preconditions: τ₁ requires food on plate (deontic obligation), τ₂ requires child loves food (bouletic desire).

§ 6.5 Intensionality without possible worlds

Propositions as types (not as sets of possible worlds). Two notions:

• Russellian proposition: a type T is "true" iff T is non-empty (inhabited)
• Austinian proposition: a pair ⟨s, T⟩ where s is a situation and T is a type; true iff s : T

§6.5, following [Aus61] and [Bar89].

@[reducible, inline]

abbrev Cooper2023Ch6.RussellianProp : Type 1

A Russellian proposition: identified with its type. True iff the type is inhabited. §6.5.

Equations

• Cooper2023Ch6.RussellianProp = Type

@[reducible, inline]

abbrev Cooper2023Ch6.AustinianProp (S : Type) : Type

An Austinian proposition: a situation paired with a classifying type. §6.5, following [BP83] and [Aus61].

True iff the situation is of the type. The situation and type are independent — the proposition claims that sit is of the situation type, but this need not hold. This is the canonical Austinian proposition type; see also TrueAustinianProp for the always-true special case.

Equations

• Cooper2023Ch6.AustinianProp = Semantics.TypeTheoretic.CheckableAustinian

structure Cooper2023Ch6.TrueAustinianProp : Type 1

A witnessed (always-true) Austinian proposition: a situation–type pair where the situation is bundled with its type, guaranteeing truth by construction. This is a special case — useful when you need to exhibit a true proposition without a separate truth check.

For the general (falsifiable) version, use AustinianProp.

• SitType : Type

  The type (situation type)

• sit : self.SitType

  The situation (witness of the type)

def Cooper2023Ch6.TrueAustinianProp.isTrue (p : TrueAustinianProp) : Prop

A TrueAustinianProp is always true (the situation witnesses the type).

Equations

• p.isTrue = Nonempty p.SitType

def Cooper2023Ch6.TrueAustinianProp.toAustinian (p : TrueAustinianProp) : AustinianProp p.SitType

A TrueAustinianProp embeds into an AustinianProp that is always true.

Equations

• p.toAustinian = { sit := p.sit, sitType := fun (x : p.SitType) => True }

theorem Cooper2023Ch6.TrueAustinianProp.toAustinian_isTrue (p : TrueAustinianProp) : Semantics.TypeTheoretic.CheckableAustinian.isTrue p.toAustinian

The embedded proposition is always true.

theorem Cooper2023Ch6.russellian_true_implies_trueAustinian {T : Type} (h : Semantics.TypeTheoretic.IsTrue T) : ∃ (p : TrueAustinianProp), p.SitType = T

If a Russellian proposition is true, there exists a true Austinian proposition. §6.5: "if a Russellian proposition containing the same type is true, then there is an Austinian proposition which is true."

Structural vs postulated subtyping (§6.5, (50))

Two kinds of subtyping:

• Structural: built into the type theory (e.g., [ℓ₁:T₁, ℓ₂:T₂] ⊑ [ℓ₁:T₁])
• Postulated: added via meaning postulates (e.g., sell(a,b,c) ⊑ buy(c,b,a))

Structural subtyping is hardwired; postulated subtyping is learned/acquired. §6.5, (50).

inductive Cooper2023Ch6.SubtypingKind : Type

Subtyping kind: structural (hardwired) vs postulated (learned). §6.5, (50).

• structural : SubtypingKind
• postulated : SubtypingKind

def Cooper2023Ch6.instReprSubtypingKind.repr : SubtypingKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cooper2023Ch6.instReprSubtypingKind : Repr SubtypingKind

Equations

• Cooper2023Ch6.instReprSubtypingKind = { reprPrec := Cooper2023Ch6.instReprSubtypingKind.repr }

@[implicit_reducible]

instance Cooper2023Ch6.instDecidableEqSubtypingKind : DecidableEq SubtypingKind

Equations

• Cooper2023Ch6.instDecidableEqSubtypingKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Cooper2023Ch6.MeaningPostulate (T₁ T₂ : Type) : Type

A meaning postulate: a declared subtyping relationship between types. §6.5, (50b): sell(a,b,c) ⊑ buy(c,b,a) is a postulated subtyping that does not follow from the structure of the types.

• coerce : T₁ → T₂

  The postulated coercion

• kind : SubtypingKind

  The kind is always postulated

Buy/sell equivalence (§6.5, (50b))

A canonical example of postulated subtyping: the types for selling and buying events are distinct but related by a meaning postulate.

structure Cooper2023Ch6.SellEvent (E : Type) : Type

A sell event: seller sells thing to buyer.

• seller : E
• thing : E
• buyer : E

structure Cooper2023Ch6.BuyEvent (E : Type) : Type

A buy event: buyer buys thing from seller.

• buyer : E
• thing : E
• seller : E

def Cooper2023Ch6.structuralSubtype_example {T₁ T₂ : Type} : T₁ × T₂ → T₁

Structural subtyping example: a record with more fields subtypes one with fewer. §6.5, (50a): [ℓ₁:T₁, ℓ₂:T₂] ⊑ [ℓ₁:T₁].

Equations

• Cooper2023Ch6.structuralSubtype_example = Prod.fst

def Cooper2023Ch6.sellBuyPostulate (E : Type) : MeaningPostulate (SellEvent E) (BuyEvent E)

Postulated subtyping: sell(a,b,c) ⊑ buy(c,b,a). §6.5, (50b).

Equations

• Cooper2023Ch6.sellBuyPostulate E = { coerce := fun (s : Cooper2023Ch6.SellEvent E) => { buyer := s.buyer, thing := s.thing, seller := s.seller } }

def Cooper2023Ch6.buySellPostulate (E : Type) : MeaningPostulate (BuyEvent E) (SellEvent E)

The reverse postulate: buy(a,b,c) ⊑ sell(c,b,a).

Equations

• Cooper2023Ch6.buySellPostulate E = { coerce := fun (b : Cooper2023Ch6.BuyEvent E) => { seller := b.seller, thing := b.thing, buyer := b.buyer } }

theorem Cooper2023Ch6.sell_buy_roundtrip {E : Type} (s : SellEvent E) : (buySellPostulate E).coerce ((sellBuyPostulate E).coerce s) = s

Roundtrip: sell → buy → sell = id (the postulates are inverses).

Believe and know (§6.5, (38)–(41))

Propositional attitudes are analyzed via matching against long-term memory. believe(a, T) is non-empty iff there exists T' in a's long-term memory such that T' ⊑_∼ T (subtype modulo relabelling).

§6.5, (40): e : believe(a, T) iff e : ltm(a, T') and T' ⊑_∼ T

structure Cooper2023Ch6.LTM (Agent : Type) : Type 1

An agent's long-term memory: maps agents to record types (their stored beliefs). §6.5, p.257: "r is a's total information state, then a's long-term memory will be r.ltm."

• memType : Agent → Type

  The type representing the agent's long-term memory

def Cooper2023Ch6.subtypeModRelabel (T₁ T₂ : Type) : Prop

Subtyping modulo relabelling: T₁ ⊑_∼ T₂ iff there is a relabelling η such that T₁ ⊑ [T₂]_η. §6.5, (39). We model this abstractly as the existence of a coercion.

Equations

• Cooper2023Ch6.subtypeModRelabel T₁ T₂ = Nonempty (T₁ → T₂)

def Cooper2023Ch6.believe {Agent : Type} (ltm : LTM Agent) (a : Agent) (T : Type) : Prop

Witness condition for believe(a, T): version (40). §6.5, (40): e : believe(a, T) iff e : ltm(a, T') and T' ⊑_∼ T.

Equations

• Cooper2023Ch6.believe ltm a T = Cooper2023Ch6.subtypeModRelabel (ltm.memType a) T

def Cooper2023Ch6.know {Agent : Type} (ltm : LTM Agent) (a : Agent) (T : Type) : Prop

Knowledge is veridical belief: know(a, T) requires believe(a, T) AND T true. This is a standard characterization; does not give a full definition of 'know' but discusses the connection.

Equations

• Cooper2023Ch6.know ltm a T = (Cooper2023Ch6.believe ltm a T ∧ Semantics.TypeTheoretic.IsTrue T)

theorem Cooper2023Ch6.know_implies_believe {Agent : Type} {ltm : LTM Agent} {a : Agent} {T : Type} : know ltm a T → believe ltm a T

Knowledge implies belief.

theorem Cooper2023Ch6.know_implies_true {Agent : Type} {ltm : LTM Agent} {a : Agent} {T : Type} : know ltm a T → Semantics.TypeTheoretic.IsTrue T

Knowledge implies truth (veridicality).

theorem Cooper2023Ch6.believe_closed_under_subtype {Agent : Type} {ltm : LTM Agent} {a : Agent} {T₁ T₂ : Type} (hb : believe ltm a T₁) (hsub : T₁ → T₂) : believe ltm a T₂

Belief is closed under (modulo-relabelling) subtyping. §6.5, (41): "for any relabelling η of T, s : believe(a, [T]_η)".

Abstract bridge: know = believe + veridicality

TTR's know = believe ∧ IsTrue mirrors the standard doxastic classification:

• know is veridical (factivity: know p → p)
• believe is non-veridical (believe p ↛ p)

This is the abstract pattern that connects to Doxastic.veridical in Semantics.Intensional/Attitude/Doxastic.lean. The full bridge (importing Doxastic) is deferred to a future Theories/TTR/ module.

theorem Cooper2023Ch6.know_iff_believe_and_true {Agent : Type} {ltm : LTM Agent} {a : Agent} {T : Type} : know ltm a T ↔ believe ltm a T ∧ Semantics.TypeTheoretic.IsTrue T

know is exactly believe + veridicality: the two components are independent.

theorem Cooper2023Ch6.believe_not_entails_true : ¬∀ (Agent : Type) (ltm : LTM Agent) (a : Agent) (T : Type), believe ltm a T → Semantics.TypeTheoretic.IsTrue T

Belief does not entail truth: an agent can believe a false type. This shows know is strictly stronger than believe. With memType = Empty, believe holds vacuously for any T (including Empty).

Points of view (§6.5, (55)–(60))

A point of view on a type T is a type T' that shares some labels/fields with T but provides alternative field types. Used for the Hesperus/Phosphorus puzzle and for intensional transitive verbs.

§6.5, (55): pov(T₁, T₂) — T₁ is a point of view on T₂. The key property: a situation can be described from different points of view.

We model this as: T₁ is a point of view on T₂ if there is a way to "merge" T₁ with T₂ (asymmetric merge).

structure Cooper2023Ch6.PointOfView (T₁ T₂ : Type) : Type 1

A point of view: T₁ is an alternative perspective on T₂. §6.5, (55): pov(T₁, T₂) — T₁ shares labels with T₂ but provides alternative field types. The merge field represents asymmetric merge (⊕) of T₂ with T₁.

• Merged : Type

  The result of asymmetric merge: T₂[⊕]T₁

• project : self.Merged → T₂

  The merged type subtypes T₂ (it's a version of T₂ with T₁'s perspective)

def Cooper2023Ch6.extMember {T : Type} (_a : T) : Prop

Extended membership: a :_E T iff a : T or some component of a is of type T. §6.5, (57): a :_E T iff either a : T or for some b ε a, b : T.

Equations

• Cooper2023Ch6.extMember _a = True

def Cooper2023Ch6.extMemberVia {Outer Inner : Type} (a : Outer) (extract : Outer → Inner) (T : Inner → Type) : Prop

Equations

• Cooper2023Ch6.extMemberVia a extract T = Nonempty (T (extract a))

Revised believe with points of view (§6.5, (58))

§6.5, (58) revises the witness condition for believe to account for points of view: e : believe(a, T) if e : ltm(a, T') and T' ⊑_∼ T OR e :_E believe(a, T₁) and e :E pov(T₂, T₁) and T₁[⊕]T₂ ⊑∼ T

def Cooper2023Ch6.believeWithPov {Agent : Type} (ltm : LTM Agent) (a : Agent) (T : Type) : Prop

Revised believe with point-of-view support. §6.5, (58).

Equations

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

theorem Cooper2023Ch6.believe_implies_believeWithPov {Agent : Type} {ltm : LTM Agent} {a : Agent} {T : Type} (h : believe ltm a T) : believeWithPov ltm a T

Direct belief implies belief-with-pov.

Hesperus/Phosphorus puzzle (§6.5, (52)–(53))

The ancients believed Hesperus (evening star) and Phosphorus (morning star) were different objects, but they are both Venus. In TTR, this is modeled via different labels in the long-term memory type: the names are associated with different paths in the record, so believe(ancients, [Hesperus rises in evening]) and believe(ancients, [Phosphorus rises in morning]) are non-trivially different.

inductive Cooper2023Ch6.CelestialBody : Type

• venus : CelestialBody

@[implicit_reducible]

instance Cooper2023Ch6.instReprCelestialBody : Repr CelestialBody

Equations

• Cooper2023Ch6.instReprCelestialBody = { reprPrec := Cooper2023Ch6.instReprCelestialBody.repr }

def Cooper2023Ch6.instReprCelestialBody.repr : CelestialBody → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cooper2023Ch6.instDecidableEqCelestialBody : DecidableEq CelestialBody

Equations

• Cooper2023Ch6.instDecidableEqCelestialBody x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Cooper2023Ch6.AncientsLTM_Before : Type

Ancient's LTM type before learning Hesperus = Phosphorus. §6.5, (52): separate entries for Hesperus and Phosphorus.

• hesperus : CelestialBody
• hesperus_rises_evening : self.hesperus = CelestialBody.venus
• phosphorus : CelestialBody
• phosphorus_rises_morning : self.phosphorus = CelestialBody.venus

structure Cooper2023Ch6.AncientsLTM_Afterextends Cooper2023Ch6.AncientsLTM_Before : Type

Ancient's LTM type after learning they are the same. §6.5, (53): entries unified with identity constraint.

• hesperus : CelestialBody
• hesperus_rises_evening : self.hesperus = CelestialBody.venus
• phosphorus : CelestialBody
• phosphorus_rises_morning : self.phosphorus = CelestialBody.venus
• same : self.hesperus = self.phosphorus

theorem Cooper2023Ch6.ancients_separate_beliefs : ∃ (ltm : AncientsLTM_Before), ltm.hesperus = ltm.phosphorus

Before learning: the ancients can believe separately about Hesperus/Phosphorus. Even though both are Venus, the two record fields are distinct in the type.

@[implicit_reducible]

instance Cooper2023Ch6.instCoeAncientsLTM_AfterAncientsLTM_Before : Coe AncientsLTM_After AncientsLTM_Before

The identity becomes explicit only in the "after" type. Structural consequence: the after-type is a subtype of the before-type (it has more fields/constraints).

Equations

• Cooper2023Ch6.instCoeAncientsLTM_AfterAncientsLTM_Before = { coe := Cooper2023Ch6.AncientsLTM_After.toAncientsLTM_Before }

theorem Cooper2023Ch6.learning_adds_constraint (ltm : AncientsLTM_After) : ltm.hesperus = ltm.phosphorus

Learning Hesperus = Phosphorus is adding a constraint (more fields).

Intensional transitive verbs (§6.5, (63)–(66))

Montague treated intensional verbs (seek, worship) as taking quantifier arguments. Cooper recasts this in TTR: predicates with arity ⟨Ind, Quant⟩ where the quantifier is the object argument.

Key concepts:

• p†: the extensional variant of an intensional predicate
• Meaning postulate (65): p(a, Q) ≈_𝕋 Q(λr:[x:Ind].[e:p†(a,r.x)])
• Success postulate (66): successful(seek(a,Q)) ⊑_𝕋 find(a,Q) (a successful search is a finding)

structure Cooper2023Ch6.IntensionalTV (E : Type) : Type 1

An intensional transitive verb: takes an individual and a quantifier. §6.5, (64): SemTransVerb(T_bg, p) for arity ⟨Ind, Quant⟩ = 'λc:T_bg. λQ:Quant. λr:[x:Ind]. [e : p(r.x, Q)]'

The p† variant is the extensional "dagger" form relating to individuals.

• pred : E → Semantics.TypeTheoretic.Quant E → Type

  The intensional predicate: Ind → Quant → Type

• dagger : E → E → Type

  The extensional dagger variant: Ind → Ind → Type

def Cooper2023Ch6.extensionalMP {E : Type} (itv : IntensionalTV E) (a : E) (Q : Semantics.TypeTheoretic.Quant E) : Prop

Meaning postulate (65) for extensional transitive verbs: p(a, Q) ≈ Q(λr:[x:Ind].[e:p†(a,r.x)]) §6.5, (65).

Equations

• Cooper2023Ch6.extensionalMP itv a Q = Nonempty (itv.pred a Q ≃ Q fun (x : E) => itv.dagger a x)

structure Cooper2023Ch6.SuccessPostulate (E : Type) : Type 1

Success postulate (66): a successful search is a finding. §6.5, (66): successful(seek(a, Q)) ⊑_𝕋 find(a, Q).

• seek : IntensionalTV E
• find : IntensionalTV E
• success (a : E) (Q : Semantics.TypeTheoretic.Quant E) (itv_success : Type) : (itv_success → self.seek.pred a Q) → itv_success → self.find.pred a Q

  If a successful seek is a subtype of find

Worship (§6.5, (69)–(75))

Worship requires:

1. Religious belief (intentionality): the subject believes in the deity
2. Specificity: the religious belief type is a subtype of the quantified type

§6.5, (75): e : worship(a, Q) iff for some T, (1) e : rbelieve(a, T) — a has T as a religious belief (2) T ⊑_∼ Q(λr:[x:Ind].worship†(a, r.x))

def Cooper2023Ch6.rbelieve {Agent : Type} (_ltm : LTM Agent) (rbelType : Agent → Type) (a : Agent) (T : Type) : Prop

Religious belief: a distinguished part of long-term memory. §6.5, (72)–(74).

Equations

• Cooper2023Ch6.rbelieve _ltm rbelType a T = Nonempty (rbelType a → T)

def Cooper2023Ch6.worshipSem {E : Type} (ltm : LTM E) (rbelType : E → Type) (worshipDagger : E → E → Type) (a : E) (Q : Semantics.TypeTheoretic.Quant E) : Prop

Witness condition for worship (§6.5, (75)). e : worship(a, Q) iff for some T: (1) e : rbelieve(a, T) (2) T ⊑_∼ Q(λr:[x:Ind].worship†(a, r.x))

Equations

• Cooper2023Ch6.worshipSem ltm rbelType worshipDagger a Q = ∃ (T : Type), Cooper2023Ch6.rbelieve ltm rbelType a T ∧ Cooper2023Ch6.subtypeModRelabel T (Q fun (x : E) => worshipDagger a x)

Want (§6.5, (88)–(92))

The analysis of want uses desire states (parallel to LTM). want†(a, T) is non-empty iff a's desires include T (the desire type is a subtype of T, modulo relabelling).

§6.5, (90)–(92): want_P and want_Q related to want†; witness condition uses des(a, T') and T' ⊑_∼ T.

structure Cooper2023Ch6.AgentInfoState (Agent : Type) : Type 1

An agent's full information state: long-term memory, religious beliefs, desires. §6.5, (91). Distinct from the Ch4 TotalInfoState which pairs memory with a dialogue gameboard.

• ltm : Agent → Type

  Long-term memory type for each agent

• rbel : Agent → Type

  Religious belief type for each agent

• des : Agent → Type

  Desire type for each agent

def Cooper2023Ch6.desire {Agent : Type} (ais : AgentInfoState Agent) (a : Agent) (T : Type) : Prop

Desire predicate: des(a, T) iff a's desire state subtypes T. §6.5: "e : des(a, T) just in case T is a's desires in e."

Equations

• Cooper2023Ch6.desire ais a T = Cooper2023Ch6.subtypeModRelabel (ais.des a) T

def Cooper2023Ch6.wantDagger {Agent : Type} (ais : AgentInfoState Agent) (a : Agent) (T : Type) : Prop

Witness condition for want†(a, T). §6.5, (92): e : want†(a, T) if for some T', e : des(a, T') and T' ⊑_∼ T.

Equations

• Cooper2023Ch6.wantDagger ais a T = Cooper2023Ch6.desire ais a T

def Cooper2023Ch6.wantWithPov {Agent : Type} (ais : AgentInfoState Agent) (a : Agent) (T : Type) : Prop

want with point of view (§6.5, (92) second clause): e : want†(a, T) if for some T₁, T₂: e :_E want†(a, T₁) e :E pov(T₂, T₁) T₁[⊕]T₂ ⊑∼ T

Equations

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

def Cooper2023Ch6.bookPostulate {E : Type} (book_ : E → Semantics.TypeTheoretic.Quant E → Type) (be_ : E → Type) (a : E) (Q : Semantics.TypeTheoretic.Quant E) : Prop

Book as an intensional verb requiring existence. §6.5, (87): book(a, Q) ⊑_𝕋 Q(λr:[x:Ind].[e:be(r.x)]) This ensures that if a books Q, there is something that exists (be). Unlike seek, book implies existence but not specificity.

Equations

• Cooper2023Ch6.bookPostulate book_ be_ a Q = Nonempty (book_ a Q → Q fun (x : E) => be_ x)

Chapter 6 phenomena

inductive Cooper2023Ch6.TwoPred : Type

A simple two-possibility modal system.

• rain : TwoPred
• snow : TwoPred

@[implicit_reducible]

instance Cooper2023Ch6.instDecidableEqTwoPred : DecidableEq TwoPred

Equations

• Cooper2023Ch6.instDecidableEqTwoPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Cooper2023Ch6.TwoObj : Type

• obj_a : TwoObj
• obj_b : TwoObj

@[implicit_reducible]

instance Cooper2023Ch6.instDecidableEqTwoObj : DecidableEq TwoObj

Equations

• Cooper2023Ch6.instDecidableEqTwoObj x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch6.twoModal : ModalSystem TwoPred TwoObj

Equations

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

theorem Cooper2023Ch6.rain_necessary : nec_r twoModal TwoPred.rain

Rain is necessary (has witnesses in both possibilities).

theorem Cooper2023Ch6.snow_possible : poss_r twoModal TwoPred.snow

Snow is possible but not necessary.

theorem Cooper2023Ch6.snow_not_necessary : ¬nec_r twoModal TwoPred.snow

theorem Cooper2023Ch6.box_rain : BoxR twoModal TwoPred.rain

□_r rain is true.

theorem Cooper2023Ch6.diamond_snow : DiamondR twoModal TwoPred.snow

◇_r snow is true but □_r snow is false.

theorem Cooper2023Ch6.not_box_snow : ¬BoxR twoModal TwoPred.snow

theorem Cooper2023Ch6.snow_not_nec_i : ¬nec_i twoModal TwoPred.snow

When all types are available everywhere (as in twoModal), nec_i and nec_r agree: snow is not inclusively necessary either.

Restrictive vs inclusive distinction

A modal system where snow is only available in one possibility. This demonstrates that nec_i is strictly weaker than nec_r: snow is inclusively necessary (has witnesses wherever available) but not restrictively necessary (not available = not checked).

def Cooper2023Ch6.twoModalRestricted : ModalSystem TwoPred TwoObj

A modal system where snow is only a type in the first possibility. Rain is available everywhere; snow is only available at true.

Equations

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

theorem Cooper2023Ch6.restricted_snow_not_nec_r : ¬nec_r twoModalRestricted TwoPred.snow

Snow is NOT restrictively necessary: no witnesses at false.

theorem Cooper2023Ch6.restricted_snow_nec_i : nec_i twoModalRestricted TwoPred.snow

Snow IS inclusively necessary: the only possibility where snow is available (true) has a witness. The false possibility doesn't have snow as a type, so it's not checked.

theorem Cooper2023Ch6.nec_i_not_implies_nec_r : ¬∀ (Ty Obj : Type) (ms : ModalSystem Ty Obj) (T : Ty), nec_i ms T → nec_r ms T

This is the key result: nec_i does NOT imply nec_r. The inclusive/restrictive distinction is non-trivial.

def Cooper2023Ch6.samSellsBookToKim : SellEvent String

Buy/sell postulated subtyping phenomenon.

Equations

• Cooper2023Ch6.samSellsBookToKim = { seller := "Kim", thing := "Syntactic Structures", buyer := "Sam" }

def Cooper2023Ch6.kimBuysBookFromSam : BuyEvent String

Equations

• Cooper2023Ch6.kimBuysBookFromSam = { buyer := "Sam", thing := "Syntactic Structures", seller := "Kim" }

theorem Cooper2023Ch6.sell_matches_buy : (sellBuyPostulate String).coerce samSellsBookToKim = kimBuysBookFromSam

structure Cooper2023Ch6.SimpleWorld : Type

Belief phenomenon: an agent whose LTM subtypes a type believes it.

• raining : Bool

def Cooper2023Ch6.weatherLTM : LTM Unit

Equations

• Cooper2023Ch6.weatherLTM = { memType := fun (x : Unit) => Cooper2023Ch6.SimpleWorld }

theorem Cooper2023Ch6.agent_believes_weather : believe weatherLTM () SimpleWorld

def Cooper2023Ch6.hesperusType : Type

Point of view phenomenon: Hesperus/Phosphorus with a point of view.

Equations

• Cooper2023Ch6.hesperusType = Cooper2023Ch6.CelestialBody

def Cooper2023Ch6.phosphorusType : Type

Equations

• Cooper2023Ch6.phosphorusType = Cooper2023Ch6.CelestialBody

theorem Cooper2023Ch6.hesperus_phosphorus_same_entity : CelestialBody.venus = CelestialBody.venus

Both resolve to the same entity (Venus) but via different type paths.

Bridge: ModalSystem → Intensional.Intension

TTR's ModalSystem achieves intensionality without Intension W τ: a type T can have different extensions across possibilities, which is exactly what an intension does across worlds.

def Cooper2023Ch6.modalSystem_induces_intension {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Intensional.Intension ms.Poss (Obj → Prop)

A ModalSystem induces an intension for each type: the function mapping each possibility to the type's extension at that possibility.

Equations

• Cooper2023Ch6.modalSystem_induces_intension ms T p = ms.ext p T

def Cooper2023Ch6.ModalSystem.isRigidType {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

A type is rigid in a modal system iff its extension is constant across all possibilities — matching Intensional.Intension.IsRigid.

Equations

• ms.isRigidType T = (Cooper2023Ch6.modalSystem_induces_intension ms T).IsRigid

MeaningPostulate enables belief transfer

A meaning postulate from T₁ to T₂ enables belief transfer: if an agent believes T₁ and there's a postulate T₁ → T₂, then the agent believes T₂.

theorem Cooper2023Ch6.meaningPostulate_transfers_belief {Agent : Type} {ltm : LTM Agent} {a : Agent} {T₁ T₂ : Type} (hb : believe ltm a T₁) (mp : MeaningPostulate T₁ T₂) : believe ltm a T₂

A meaning postulate from T₁ to T₂ enables belief transfer: if an agent believes T₁ and there's a postulate T₁ → T₂, then the agent believes T₂. This connects MeaningPostulate to the doxastic system.

TrueAustinianProp → AustinianProp

TrueAustinianProp carries its own witness (always true by construction). AustinianProp (= CheckableAustinian) is the general case that can be false. This bridge embeds the former into the latter.

def Cooper2023Ch6.cooperToGinzburg (ap : TrueAustinianProp) : AustinianProp ap.SitType

Embed a TrueAustinianProp (always true) into an AustinianProp.

A TrueAustinianProp carries its own witness, so the resulting AustinianProp is always true.

Equations

• Cooper2023Ch6.cooperToGinzburg ap = { sit := ap.sit, sitType := fun (x : ap.SitType) => True }

theorem Cooper2023Ch6.cooperToGinzburg_always_true (ap : TrueAustinianProp) : Semantics.TypeTheoretic.CheckableAustinian.isTrue (cooperToGinzburg ap)

The embedding preserves truth.

Cooper's foundational examples motivating intensional type theory. The groundhog/woodchuck and roundSquare/evenPrimeGt2 pairs demonstrate that TTR distinguishes types with the same extension — the structural commitment underlying all of Ch. 6's intensional content.

def Cooper2023Ch6.groundhog : Semantics.TypeTheoretic.IType

groundhog and woodchuck as intensional types: same carrier, different names. §1.3: types are not sets; two types can share all witnesses yet remain distinct.

Equations

• Cooper2023Ch6.groundhog = { carrier := Unit, name := "groundhog" }

def Cooper2023Ch6.woodchuck : Semantics.TypeTheoretic.IType

Equations

• Cooper2023Ch6.woodchuck = { carrier := Unit, name := "woodchuck" }

theorem Cooper2023Ch6.groundhog_woodchuck_ext_equiv : groundhog.extEquiv woodchuck

They are extensionally equivalent (same carrier).

theorem Cooper2023Ch6.groundhog_ne_woodchuck : ¬groundhog.intEq woodchuck

But they are intensionally distinct (different names). This is Cooper's key point: groundhog ≠ woodchuck in TTR, whereas in extensional set theory {marmota} = {marmota}.

def Cooper2023Ch6.roundSquare : Semantics.TypeTheoretic.IType

round_square and even_prime_gt_2 are both empty but distinct. §1.3: possible worlds cannot distinguish these since both have empty extension at every world. TTR can: they are different types.

Equations

• Cooper2023Ch6.roundSquare = { carrier := Empty, name := "round_square" }

def Cooper2023Ch6.evenPrimeGt2 : Semantics.TypeTheoretic.IType

Equations

• Cooper2023Ch6.evenPrimeGt2 = { carrier := Empty, name := "even_prime_gt_2" }

theorem Cooper2023Ch6.round_square_empty : Semantics.TypeTheoretic.IsFalse roundSquare.carrier

theorem Cooper2023Ch6.even_prime_gt2_empty : Semantics.TypeTheoretic.IsFalse evenPrimeGt2.carrier

theorem Cooper2023Ch6.empty_types_distinct : ¬roundSquare.intEq evenPrimeGt2

inductive Cooper2023Ch6.Ind : Type

Individuals in Cooper's fragment: Dudamel and Beethoven.

• dudamel : Ind
• beethoven : Ind

@[implicit_reducible]

instance Cooper2023Ch6.instReprInd : Repr Ind

Equations

• Cooper2023Ch6.instReprInd = { reprPrec := Cooper2023Ch6.instReprInd.repr }

def Cooper2023Ch6.instReprInd.repr : Ind → ℕ → Std.Format

Equations

• Cooper2023Ch6.instReprInd.repr Cooper2023Ch6.Ind.dudamel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023Ch6.Ind.dudamel")).group prec✝
• Cooper2023Ch6.instReprInd.repr Cooper2023Ch6.Ind.beethoven prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023Ch6.Ind.beethoven")).group prec✝

@[implicit_reducible]

instance Cooper2023Ch6.instDecidableEqInd : DecidableEq Ind

Equations

• Cooper2023Ch6.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Cooper2023Ch6.Conductor : Ind → Type

Predicate "conductor": Dudamel is a conductor.

• mk : Conductor Ind.dudamel

inductive Cooper2023Ch6.Composer : Ind → Type

Predicate "composer": Beethoven is a composer.

• mk : Composer Ind.beethoven

def Cooper2023Ch6.conductorPpty : Semantics.TypeTheoretic.Ppty Ind

"conductor" content: Ppty Ind.

Equations

• Cooper2023Ch6.conductorPpty = Semantics.TypeTheoretic.semCommonNoun Cooper2023Ch6.Conductor

def Cooper2023Ch6.composerPpty : Semantics.TypeTheoretic.Ppty Ind

"composer" content: Ppty Ind.

Equations

• Cooper2023Ch6.composerPpty = Semantics.TypeTheoretic.semCommonNoun Cooper2023Ch6.Composer

def Cooper2023Ch6.dudamelQuant : Semantics.TypeTheoretic.Quant Ind

"Dudamel" content: Quant Ind (GQ).

Equations

• Cooper2023Ch6.dudamelQuant = Semantics.TypeTheoretic.semPropName Cooper2023Ch6.Ind.dudamel

def Cooper2023Ch6.beethovenQuant : Semantics.TypeTheoretic.Quant Ind

"Beethoven" content: Quant Ind (GQ).

Equations

• Cooper2023Ch6.beethovenQuant = Semantics.TypeTheoretic.semPropName Cooper2023Ch6.Ind.beethoven

@[reducible, inline]

abbrev Cooper2023Ch6.aConductor : Semantics.TypeTheoretic.Quant Ind

Step 3: "a conductor" — existential quantifier over conductors.

Equations

• Cooper2023Ch6.aConductor = Semantics.TypeTheoretic.semIndefArt Cooper2023Ch6.conductorPpty

@[reducible, inline]

abbrev Cooper2023Ch6.isAConductor : Semantics.TypeTheoretic.Ppty Ind

Step 5: "is a conductor" — property of being a conductor.

Equations

• Cooper2023Ch6.isAConductor = Semantics.TypeTheoretic.semBe Cooper2023Ch6.aConductor

@[reducible, inline]

abbrev Cooper2023Ch6.dudamelIsAConductor : Type

Step 7: "Dudamel is a conductor" — a proposition (type).

Equations

• Cooper2023Ch6.dudamelIsAConductor = Cooper2023Ch6.dudamelQuant Cooper2023Ch6.isAConductor

def Cooper2023Ch6.dudamelIsAConductorTrue : dudamelIsAConductor

"Dudamel is a conductor" is TRUE (the proposition type is inhabited).

Equations

• Cooper2023Ch6.dudamelIsAConductorTrue = { individual := Cooper2023Ch6.Ind.dudamel, restrWit := Cooper2023Ch6.Conductor.mk, scopeWit := { down := ⋯ } }

@[reducible, inline]

abbrev Cooper2023Ch6.beethovenIsAConductor : Type

The analogous sentence with Beethoven.

Equations

• Cooper2023Ch6.beethovenIsAConductor = Cooper2023Ch6.beethovenQuant Cooper2023Ch6.isAConductor

instance Cooper2023Ch6.instIsFalseBeethovenIsAConductor : Semantics.TypeTheoretic.IsFalse beethovenIsAConductor

"Beethoven is a conductor" is FALSE (the proposition type is empty).

@[reducible, inline]

abbrev Cooper2023Ch6.aComposer : Semantics.TypeTheoretic.Quant Ind

"Beethoven is a composer" — TRUE.

Equations

• Cooper2023Ch6.aComposer = Semantics.TypeTheoretic.semIndefArt Cooper2023Ch6.composerPpty

@[reducible, inline]

abbrev Cooper2023Ch6.isAComposer : Semantics.TypeTheoretic.Ppty Ind

Equations

• Cooper2023Ch6.isAComposer = Semantics.TypeTheoretic.semBe Cooper2023Ch6.aComposer

@[reducible, inline]

abbrev Cooper2023Ch6.beethovenIsAComposer : Type

Equations

• Cooper2023Ch6.beethovenIsAComposer = Cooper2023Ch6.beethovenQuant Cooper2023Ch6.isAComposer

def Cooper2023Ch6.beethovenIsAComposerTrue : beethovenIsAComposer

Equations

• Cooper2023Ch6.beethovenIsAComposerTrue = { individual := Cooper2023Ch6.Ind.beethoven, restrWit := Cooper2023Ch6.Composer.mk, scopeWit := { down := ⋯ } }

§ 3.4 CnstrIsA — Construction-based "is a" (ex 85–92)

Cooper §3.4 shows that TTR can distinguish two analyses of "Dudamel is a conductor" that Montague collapses:

1. Compositional (via semBe + semIndefArt): the content involves existential quantification — ExistWitness Ind Conductor (λ y => propT (d = y)).

2. Construction-based CnstrIsA (§3.4, ex 87): the VP ↟ NP construction makes the VP content equal to the NP content directly — conductor(d).

The two are truth-conditionally equivalent (inhabited iff Dudamel is a conductor) but structurally distinct as types. This structural distinction is unavailable in Montague's system, where truth-conditional equivalence entails identity of denotation.

@[reducible, inline]

abbrev Cooper2023Ch6.cnstrIsA {E : Type} (pred : E → Type) (individual : E) : Type

CnstrIsA: construction-based content for "NP is a CN". §3.4, ex (87): VP → V NP ∧ CnstrIsA. The content is the predicate applied directly to the individual — no existential quantification. §3.4, ex (92a): [ e : conductor(d) ].

Equations

• Cooper2023Ch6.cnstrIsA pred individual = pred individual

@[reducible, inline]

abbrev Cooper2023Ch6.dudamelIsAConductor_cnstr : Type

Construction-based "Dudamel is a conductor" — direct predication.

Equations

• Cooper2023Ch6.dudamelIsAConductor_cnstr = Cooper2023Ch6.cnstrIsA Cooper2023Ch6.Conductor Cooper2023Ch6.Ind.dudamel

def Cooper2023Ch6.dudamelIsAConductor_cnstr_true : dudamelIsAConductor_cnstr

CnstrIsA "Dudamel is a conductor" is TRUE.

Equations

• Cooper2023Ch6.dudamelIsAConductor_cnstr_true = Cooper2023Ch6.Conductor.mk

instance Cooper2023Ch6.instIsFalseCnstrIsAIndConductorBeethoven : Semantics.TypeTheoretic.IsFalse (cnstrIsA Conductor Ind.beethoven)

CnstrIsA "Beethoven is a conductor" is FALSE.

theorem Cooper2023Ch6.cnstrIsA_equiv_compositional (individual : Ind) (pred : Ind → Type) : Nonempty (cnstrIsA pred individual) ↔ Nonempty (Semantics.TypeTheoretic.ExistWitness Ind pred fun (y : Ind) => Semantics.TypeTheoretic.propT (individual = y))

The compositional and construction readings are truth-conditionally equivalent: both inhabited iff the individual has the property.

theorem Cooper2023Ch6.cnstrIsA_intensionally_distinct : ¬{ carrier := cnstrIsA Conductor Ind.dudamel, name := "conductor(d)" }.intEq { carrier := dudamelIsAConductor, name := "exist(conductor, be(d))" }

As ITypes, the compositional and construction readings are intensionally distinct.

@[reducible, inline]

abbrev Cooper2023Ch6.aConductorIsDudamel : Type

"A conductor is Dudamel" — only the compositional reading available.

Equations

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

def Cooper2023Ch6.aConductorIsDudamel_true : aConductorIsDudamel

Equations

• Cooper2023Ch6.aConductorIsDudamel_true = { individual := Cooper2023Ch6.Ind.dudamel, restrWit := Cooper2023Ch6.Conductor.mk, scopeWit := { down := ⋯ } }

theorem Cooper2023Ch6.reversed_equiv_compositional : Nonempty aConductorIsDudamel ↔ Nonempty dudamelIsAConductor

Cooper's Topos ↔ Kratzer's ⟨ModalBase, OrderingSource⟩

Cooper §6.4 explicitly positions topoi as the TTR replacement for Kratzer's conversational backgrounds: "topoi replace accessibility relations between possible worlds." This section makes the replacement claim Lean-checkable by constructing a faithful translation in both directions and proving equivalence on the necessity/possibility operators.

Translation (kratzerToTopos): a Kratzer triple ⟨f, g, w⟩ together with a proposition p induces a topos whose background is the Kratzer best-worlds set (from f/g at w) and whose foreground records membership in p.

Agreement theorem (kratzer_topos_nec_iff): Cooper's Topos.inducedNec on the translated topos coincides with Kratzer's necessity operator. Same for possibility.

Disagreement theorem (ttr_kratzer_collapse_disagree): Cooper's Topos.nec_implies_poss requires Nonempty τ.Bg as a side condition (empty topoi vacuously satisfy inducedNec but cannot satisfy inducedPoss). Kratzer's necessity → possibility (the D axiom) holds under the same side condition (Nonempty (bestWorlds f g w)). The two frameworks AGREE on D-axiom validity gating, contra a naive reading that TTR avoids the D-issue altogether.

This is the load-bearing comparison that previous prose-only deferrals in the Modality docstring (§6.4 prose, "Topoi replace Kratzer's conversational backgrounds...") promised but did not deliver.

def Cooper2023Ch6.kratzerToTopos {W : Type} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (w : W) (p : W → Prop) : Topos

Kratzer-to-Cooper translation. A modal base + ordering source + evaluation world + proposition induces a Cooper topos:

• Background: the Kratzer-best worlds (as a Subtype of W).
• Foreground: PLift of p evaluated at the world.

The Subtype encoding ensures the topos's Bg carries exactly the worlds Kratzer's Best(f,g,w) selects.

Equations

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

theorem Cooper2023Ch6.kratzer_topos_nec_iff {W : Type} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (w : W) (p : W → Prop) : (kratzerToTopos f g w p).inducedNec ↔ Semantics.Modality.Kratzer.necessity f g p w

Agreement on necessity. Cooper's Topos.inducedNec over the Kratzer-derived topos coincides with Kratzer's necessity f g p w.

theorem Cooper2023Ch6.kratzer_topos_poss_iff {W : Type} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (w : W) (p : W → Prop) : (kratzerToTopos f g w p).inducedPoss ↔ Semantics.Modality.Kratzer.possibility f g p w

Agreement on possibility. Cooper's Topos.inducedPoss over the Kratzer-derived topos coincides with Kratzer's possibility f g p w.

theorem Cooper2023Ch6.ttr_kratzer_d_axiom_agree {W : Type} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (w : W) (p : W → Prop) (hne : Nonempty { w' : W // w' ∈ Semantics.Modality.Kratzer.bestWorlds f g w }) : Semantics.Modality.Kratzer.necessity f g p w → Semantics.Modality.Kratzer.possibility f g p w

D axiom shared gating. Cooper's Topos.nec_implies_poss requires Nonempty τ.Bg because empty topoi satisfy inducedNec vacuously but fail inducedPoss. Translated through the bridge, the same side condition is Nonempty (bestWorlds f g w) — exactly when Kratzer's D axiom holds. The two frameworks agree on the side condition, contra a naive reading that one side avoids the issue.

theorem Cooper2023Ch6.ttr_kratzer_modal_arithmetic_agree {W : Type} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (w : W) (p : W → Prop) : ((kratzerToTopos f g w p).inducedNec ↔ Semantics.Modality.Kratzer.necessity f g p w) ∧ ((kratzerToTopos f g w p).inducedPoss ↔ Semantics.Modality.Kratzer.possibility f g p w)

The disagreement is structural, not modal. The bridge proves that TTR Topos-induced modality and Kratzer best-world modality are pointwise equivalent on the same data. So any apparent disagreement between the two frameworks (broccoli case studies, ought/can scenarios) is a disagreement about what counts as the right modal base + ordering source — not about the necessity/possibility primitives themselves.

This refutes the casual reading that "TTR replaces Kratzer's modal backgrounds with topoi" implies a different modal arithmetic. The arithmetic is the same; the framework difference is whether modal data lives in worlds (Kratzer) or situations (Cooper).