diff --git a/Linglib/Semantics/Composition/Assignment.lean b/Linglib/Semantics/Composition/Assignment.lean
index cf08939266..17549f7589 100644
--- a/Linglib/Semantics/Composition/Assignment.lean
+++ b/Linglib/Semantics/Composition/Assignment.lean
@@ -6,33 +6,26 @@ public import Mathlib.Logic.Function.DependsOn
 /-!
 # Assignment-relative denotations
 
-This file defines the denotation of binders relative to a variable assignment `g : ℕ → E`, which
-gives each index a value. In the textbook of Heim and Kratzer, the Traces and Pronouns Rule has a
-pronoun or trace with index `n` denote `g n`, the evaluation `Function.eval n` of the assignment,
-and Predicate Abstraction has a binder at `n` abstract over the value of `n` by updating `g`. An
-assignment-relative denotation in `α` is a function `Assignment E → α`, a computation of Lean's
-reader monad `ReaderM (Assignment E)`. Charlow factors the standard theory through this monad: its
-`pure`, `<*>` and `joinM` are his lift `ρ`, application `⊛` and flattener `μ`, and `lambdaAbsG` is
-his categorematic abstraction `Λᵢ`.
-
-The indices a denotation reads are those it depends on, in the sense of mathlib's `DependsOn`. An
-abstraction over `n` reads the indices its body reads other than `n`, and abstracting over an
-index the body does not read gives a constant function.
+A *variable assignment* gives each index a value. A pronoun or trace with index $n$ denotes the
+value it gives $n$, by Heim and Kratzer's Traces and Pronouns Rule, and a binder with index $n$
+abstracts over that value, by Predicate Abstraction; Charlow factors both through the reader monad.
+An abstraction over $n$ [reads the indices its body reads other than $n$](##dependsOn_lambdaAbsG),
+and abstracting over an index the body does not read
+[gives a constant function](##lambdaAbsG_eq_const_iff).
 
 ## Main definitions
 
-* `lambdaAbsG`: abstraction over an index.
-
-## Main results
-
-* `dependsOn_lambdaAbsG`: abstraction over `n` removes `n` from the indices a body depends on.
-* `lambdaAbsG_eq_const_iff`: abstraction over `n` is constant at every assignment exactly when
-  the body does not depend on `n`.
+* `Montague.lambdaAbsG`: abstraction over an index.
 
 ## Implementation notes
 
-Assignments are total, where Heim and Kratzer's are partial, so a pronoun denotes at every
-assignment. Nothing fixes `E` to entities: at an assignment of situations, a pronoun is a
+An assignment is a function `g : ℕ → E`, and a pronoun with index `n` denotes `g n`, the
+evaluation `Function.eval n` of the assignment. An assignment-relative denotation in `α` is a
+function `Assignment E → α`, a computation of Lean's `ReaderM (Assignment E)`, whose `pure`, `<*>`
+and `joinM` are Charlow's lift `ρ`, application `⊛` and flattener `μ`, and `lambdaAbsG` is his
+`Λᵢ`. The indices a denotation reads are those it depends on in the sense of mathlib's
+`DependsOn`. Assignments are total, where Heim and Kratzer's are partial, so a pronoun denotes at
+every assignment. Nothing fixes `E` to entities: at an assignment of situations, a pronoun is a
 situation pronoun.
 
 ## References
@@ -50,8 +43,8 @@ open scoped Assignment
 
 variable {E α : Type*} {n : ℕ}
 
-/-- `lambdaAbsG n body` is the abstraction of `body` over index `n`, which at the assignment `g`
-maps `x` to the value of `body` at `g[n ↦ x]`. -/
+/-- The abstraction of `body` over the index `n`: at the assignment `g` it maps `x` to the value
+of `body` at `g[n ↦ x]`. -/
 def lambdaAbsG (n : ℕ) (body : Assignment E → α) : Assignment E → E → α :=
   fun g x ↦ body (g[n ↦ x])
 
diff --git a/Linglib/Semantics/Composition/Coordination.lean b/Linglib/Semantics/Composition/Coordination.lean
index 349429e1b6..b52a434007 100644
--- a/Linglib/Semantics/Composition/Coordination.lean
+++ b/Linglib/Semantics/Composition/Coordination.lean
@@ -6,26 +6,27 @@ public import Linglib.Semantics.Composition.Tree
 /-!
 # Coordination in the composition engine
 
-This file adds coordination to the composition engine of `Composition/Tree.lean` as a binary
-mode beside functional application, intensional application and predicate modification. Two
-sisters of the same conjoinable type combine by what their coordinator denotes on the pair,
-`Coordinator.denote`, in the pointwise complete Boolean algebra of that type, which the mode
-finds at runtime through `Ty.Domain.completeBooleanAlgebra?`. Predicate modification is the
-conjunctive case at `⟨e,t⟩`, so the engine's modification mode already agrees with the
-coordinator's denotation.
+Two sisters of the same conjoinable type, a type that ends in $t$, can combine by coordination:
+their coordinator's denotation applies to the pair in the pointwise Boolean algebra of the type,
+so that *and* conjoins truth values, predicates and quantifiers alike. Coordination is a mode
+beside functional application, intensional application and predicate modification, and
+predicate modification is
+[the conjunctive case at the type of predicates](##combine?_eq_coordinate?_of_conjunctive), so
+the engine's modification mode agrees with what *and* denotes.
 
 ## Main definitions
 
 * `Coordinator.coordinate?`: the coordination mode.
 
-## Main results
+## Implementation notes
 
-* `Coordinator.combine?_eq_coordinate?_of_conjunctive`: predicate modification is conjunctive
-  coordination at `⟨e,t⟩`.
+The mode finds the Boolean algebra of its daughters' type at run time, through
+`Ty.Domain.completeBooleanAlgebra?`; `Coordinator.denote` is the coordinator's denotation.
 
 ## References
 
 * [heim-kratzer-1998]
+* [partee-rooth-1983]
 -/
 
 @[expose] public section
@@ -34,9 +35,9 @@ namespace Coordinator
 
 open Montague
 
-/-- `coordinate? c d1 d2` combines two sisters of the same conjoinable type by what the
-coordinator `c` denotes on the pair, in the complete Boolean algebra of their type, threaded
-through the effect `M`, and is `none` on sisters of different or non-conjoinable types. -/
+/-- The coordination of two sisters of the same conjoinable type by what the coordinator `c`
+denotes on the pair, in the complete Boolean algebra of their type and through the effect `M`;
+`none` on sisters of different or non-conjoinable types. -/
 def coordinate? {E W : Type} {M : Type → Type} [Applicative M] (c : Coordinator)
     (d1 d2 : Denotation E W M) : Option (Denotation E W M) :=
   if h : d1.1 = d2.1 then
diff --git a/Linglib/Semantics/Composition/EventIdentification.lean b/Linglib/Semantics/Composition/EventIdentification.lean
index 34f38739a3..a13d500f06 100644
--- a/Linglib/Semantics/Composition/EventIdentification.lean
+++ b/Linglib/Semantics/Composition/EventIdentification.lean
@@ -3,35 +3,26 @@ module
 public import Linglib.Semantics.Modification.Basic
 
 /-!
-# Event Identification
+# Event identification
 
-This file defines Event Identification, the composition principle by which Kratzer adds an
-argument-introducing head to a predicate of events. The head denotes a relation between
-individuals and events, the predicate a set of events, and the two combine by conjunction at the
-event, leaving the individual argument open: an agent head and *feed the dog* yield the relation
-that holds of an individual and an event when the individual is the agent of the event and the
-event is a feeding of the dog. Event Identification is meet with the predicate lifted to a
-relation constant in the individual, so it is the relational counterpart of predicate
-modification, and repeated applications chain conditions on the same event.
+*Event identification* is Kratzer's rule for adding an argument-introducing head to a predicate
+of events: the head's relation between individuals and events and the predicate's set of events
+combine by conjunction at the event, leaving the individual open. It is
+[meet with the predicate lifted to a relation](##eventIdentification_eq_inf), the relational
+counterpart of predicate modification, and
+[two applications conjoin their predicates](##eventIdentification_eventIdentification).
 
 ## Main definitions
 
 * `ArgumentStructure.eventIdentification`: the combination of a relation and a predicate.
 
-## Main results
-
-* `eventIdentification_eq_inf`, `eventIdentification_eq_comp`: Event Identification is meet
-  with the lifted predicate, and predicate modification of each section of the relation.
-* `eventIdentification_eventIdentification`: two applications conjoin the predicates.
-* `eventIdentification_eq_bot_iff`: the result is empty exactly when, for every individual, the
-  relation's events and the predicate's are disjoint.
-
 ## Implementation notes
 
 Kratzer's rule is partial: it is undefined when the two inputs restrict the event to disjoint
-sorts, actions and states. Here it is total, and such inputs yield the empty relation
-(`eventIdentification_eq_bot_iff`). The carrier is any pair of types, so that the type-driven
-composition engine, whose events share the domain of individuals, uses the same operation.
+sorts, actions and states. Here it is total, and such inputs
+[yield the empty relation](##eventIdentification_eq_bot_iff). The carrier is any pair of types,
+so that the type-driven composition engine, whose events share the domain of individuals, uses
+the same operation.
 
 ## References
 
diff --git a/Linglib/Semantics/Composition/Extensional.lean b/Linglib/Semantics/Composition/Extensional.lean
index d9549fea19..ca1377c838 100644
--- a/Linglib/Semantics/Composition/Extensional.lean
+++ b/Linglib/Semantics/Composition/Extensional.lean
@@ -6,29 +6,14 @@ public import Linglib.Logic.Modal.Defs
 /-!
 # Extensional operators
 
-An operator on intensions is *extensional* at an index when the value it yields there depends only
-on the extension of its argument at that index. Negation is extensional: whether *it is not
-raining* is true at a world depends only on whether *it is raining* is true there. Necessity is
-not, since whether *it must be raining* is true at a world depends on whether *it is raining* is
-true at the worlds accessible from it. Among adjectives, which map properties to properties,
-*gray* is extensional and *skillful* is not: where the cobblers are exactly the darts players, the
-gray cobblers are the gray darts players, but the skillful cobblers need not be the skillful darts
-players.
-
-An operator is extensional exactly when it is
-[a function on extensions applied index by index](##isExtensional_iff_exists_eq_piMap). At an
-index where it is extensional, an operator
-[gives the same value on an intension and on the constant intension with the same
-extension](##isExtensionalAt_iff_forall_const), and so
-[cannot tell a variable it binds from one fixed at that index](##isExtensionalAt_iff_forall_diag):
-a situation variable bound under negation reads as if it were free. The truth-functional
-connectives are extensional, and so are composites of extensional operators.
-
-In general the value of an operator at an index depends on its argument at some set of indices,
-and the operator is extensional there when that set can be taken to be the index alone. Necessity
-in a Kripke frame depends at a world on
-[exactly the worlds accessible from it](##ModalLogic.dependsOn_box_iff), so it is
-[extensional only at a world that accesses no world but itself](##isExtensionalAt_box_iff).
+An operator on intensions is *extensional* at an index when its value there depends only on its
+argument's extension there: negation is extensional, necessity is not, and among adjectives
+*gray* is and *skillful* is not. An operator is extensional exactly when it is
+[a function on extensions applied index by index](##isExtensional_iff_exists_eq_piMap), and at an
+index where it is extensional it
+[cannot tell a variable it binds from one fixed there](##isExtensionalAt_iff_forall_diag).
+Necessity is [extensional only at a world that accesses no world but
+itself](##isExtensionalAt_box_iff).
 
 ## Main definitions
 
diff --git a/Linglib/Semantics/Composition/FirstOrder.lean b/Linglib/Semantics/Composition/FirstOrder.lean
index a3c363c0f5..cc8611aab1 100644
--- a/Linglib/Semantics/Composition/FirstOrder.lean
+++ b/Linglib/Semantics/Composition/FirstOrder.lean
@@ -10,13 +10,12 @@ public import Mathlib.Tactic.FinCases
 /-!
 # The first-order fragment of type-driven composition
 
-The first-order constants over a signature are its constant and relation symbols, the
-determiners *every*, *some* and *no*, negation, conjunction and disjunction. Every logical form
-over them reads back to a first-order formula whose realization is the logical form's
-denotation. The readback evaluates the logical form in a syntactic model built from mathlib's
-terms and bounded formulas, and a logical relation with the standard model proves it sound, so
-first-order consequence between readbacks is entailment between trees, as
-`Semantics/Dynamic/DRS/Reduction.lean` shows for DRT.
+A logical form built only from names, predicates, the determiners *every*, *some* and *no*, and
+the truth-functional connectives reads back to a first-order formula with the same truth
+conditions, [soundly](##realizes_readback). So
+[a tree holds exactly where its readback is true](##holdsAt_iff_realizeAt),
+[entailment between trees is first-order consequence](##models_imp_iff_entails), and
+[families of trees satisfy compactness](##holdsAt_compactness).
 
 ## Main definitions
 
@@ -27,19 +26,10 @@ first-order consequence between readbacks is entailment between trees, as
 * `Term.readback`, `Term.toFormula`: the readback of a logical form.
 * `Ty.Realizes`: the logical relation between the syntactic and the standard model.
 
-## Main results
-
-* `Term.realizes_readback`: a logical form's readback realizes its denotation whenever the
-  readbacks of its constants realize theirs.
-* `Term.realizeAt_toFormula`: a first-order logical form denotes the realization of its readback.
-* `PhraseStructure.Tree.holdsAt_iff_realizeAt`, `PhraseStructure.Tree.holdsAt_of_models`,
-  `PhraseStructure.Tree.models_imp_iff_entails`, `PhraseStructure.Tree.holdsAt_compactness`: a
-  tree holds (`PhraseStructure.Tree.HoldsAt`) where its readback is realized, entailment between
-  trees is first-order consequence, and families of trees satisfy compactness.
-
 ## Implementation notes
 
-The syntactic model is indexed by the number of bound variables in scope, and gives truth values
+The syntactic model is built from mathlib's terms and bounded formulas, and indexed by the
+number of bound variables in scope, and gives truth values
 and functions at every larger number, so a determiner binds the next de Bruijn variable of
 `BoundedFormula` without computing a fresh name. Formulas are never carried to more bound
 variables, since `BoundedFormula.castLE` keeps the index an inner quantifier binds. *Most* is not
diff --git a/Linglib/Semantics/Composition/Mode.lean b/Linglib/Semantics/Composition/Mode.lean
index d438137485..94a1960183 100644
--- a/Linglib/Semantics/Composition/Mode.lean
+++ b/Linglib/Semantics/Composition/Mode.lean
@@ -3,37 +3,36 @@ module
 public import Linglib.Semantics.Composition.Ty
 public import Linglib.Semantics.Composition.EventIdentification
 public import Linglib.Semantics.Modification.Basic
+public import Linglib.Semantics.Composition.Extensional
 
 /-!
 # Composition modes
 
-A *composition mode* of type `Mode σ₁ σ₂ τ` composes a left daughter of type `σ₁` and a right
-daughter of type `σ₂` into a mother of type `τ`. The modes are Heim and Kratzer's, with the
-intensional application of von Fintel and Heim and the event identification of Kratzer;
-functional application, intensional application and event identification come in both orders.
-The daughters' types select the mode (`Ty.mode?`): the first that applies among functional
-application, intensional application, predicate modification and event identification.
-
-A mode denotes an operation on the denotation domains (`Mode.eval`). Under an applicative effect a
-mode composes the daughters' computations in linear order, whichever daughter is the function
-(`Mode.evalM`). In any family of values indexed by types, `Mode.combine?` composes two values by
-the mode their types select.
+A *composition mode* is a rule by which the meanings of two sisters combine into the meaning of
+their mother, selected by the daughters' types: functional application, predicate modification,
+Kratzer's event identification, and von Fintel and Heim's intensional application, which gives a
+function its argument's intension rather than its value. Relative to a world, intensional
+application on daughters that do not vary with the world sees only a constant intension, and it
+[agrees with the general case on every argument exactly when the function is
+extensional](##forall_eval_intensionalLeft_eq_iff).
 
 ## Main definitions
 
-* `Montague.Mode`: the composition modes as typed binary operations.
+* `Montague.Mode`: the composition modes, typed by the two daughters and the mother.
 * `Montague.Ty.mode?`, `Montague.Ty.combine?`: the mode two daughters' types select, and the type
   they compose to.
-* `Montague.Mode.eval`, `Montague.Mode.evalM`: the denotation of a mode, pure and under an
-  applicative effect.
-* `Montague.Mode.combine?`: composition by the selected mode in a family of values.
+* `Montague.Mode.eval`: composition of daughters that do not vary with the world.
+* `Montague.Mode.intension`: the mother's intension from the daughters' intensions.
+* `Montague.Mode.evalM`: composition under an applicative effect.
+* `Montague.Mode.combine?`: composition, by the mode their types select, in a family of values.
 
-## Main results
+## Implementation notes
 
-* `Montague.Mode.combine?_map`: composing commutes with every map of families that commutes with
-  the modes.
-* `Montague.Mode.combine?_map_fst`: the type of a composed value is `Ty.combine?` of the
-  daughters' types.
+The daughters' types select the first mode that applies among functional application,
+intensional application, predicate modification and event identification. In any family of
+values indexed by types, [composing commutes with every map of families that commutes with the
+modes](##combine?_map), and [the type of the result depends only on the daughters'
+types](##combine?_map_fst).
 
 ## References
 
@@ -47,7 +46,7 @@ the mode their types select.
 namespace Montague
 
 /-- The composition modes, typed by the two daughters and the mother, are functional application,
-intensional application of a daughter expecting an intension to the rigid intension of its sister
+intensional application of a daughter expecting an intension to the intension of its sister
 ([von-fintel-heim-2011]), predicate modification of two predicates of one sort, and event
 identification of a role head with a predicate of eventualities, Kratzer's (23) ([kratzer-1996]).
 All but predicate modification come in both orders. -/
@@ -149,8 +148,10 @@ theorem functionalLeft?_self_fn (σ τ : Ty) : functionalLeft? σ (σ ⇒ τ) =
 
 variable {E W : Type} {S : Sorts} {σ₁ σ₂ τ : Ty}
 
-/-- The denotation of a mode is application, application to the rigid intension of the argument,
-intersection of two predicates, or event identification. -/
+/-- The denotation of a mode is application, application to the constant intension of the
+argument, intersection of two predicates, or event identification. The constant intension is the
+argument's intension when the argument does not vary with the world; `Mode.intension` is the
+general case. -/
 @[simp] def eval : Mode σ₁ σ₂ τ → Ty.Domain E W σ₁ S → Ty.Domain E W σ₂ S → Ty.Domain E W τ S
   | functionalLeft, f, a => f a
   | functionalRight, a, f => f a
@@ -160,6 +161,35 @@ intersection of two predicates, or event identification. -/
   | eventIdentificationLeft, f, p => ArgumentStructure.eventIdentification f p
   | eventIdentificationRight, p, f => ArgumentStructure.eventIdentification f p
 
+/-- The intension of the mother, given the intensions of the daughters. At each world functional
+application, predicate modification and event identification compose the daughters' values there,
+and intensional application applies the function's value there to the argument's whole intension
+([von-fintel-heim-2011]'s Intensional Functional Application). -/
+@[simp] def intension :
+    Mode σ₁ σ₂ τ → (W → Ty.Domain E W σ₁ S) → (W → Ty.Domain E W σ₂ S) → W → Ty.Domain E W τ S
+  | functionalLeft, f, a => fun w ↦ f w (a w)
+  | functionalRight, a, f => fun w ↦ f w (a w)
+  | intensionalLeft, f, a => fun w ↦ f w a
+  | intensionalRight, a, f => fun w ↦ f w a
+  | predicateModification, p, q => fun w ↦ Modifier.intersective (p w) (q w)
+  | eventIdentificationLeft, f, p => fun w ↦ ArgumentStructure.eventIdentification (f w) (p w)
+  | eventIdentificationRight, p, f => fun w ↦ ArgumentStructure.eventIdentification (f w) (p w)
+
+/-- On daughters that do not vary with the world, the mother's intension is constant at the
+mode's denotation. -/
+@[simp] theorem intension_const (m : Mode σ₁ σ₂ τ) (a : Ty.Domain E W σ₁ S)
+    (b : Ty.Domain E W σ₂ S) (w : W) : m.intension (fun _ ↦ a) (fun _ ↦ b) w = m.eval a b := by
+  cases m <;> rfl
+
+/-- Applying a function to the constant intension of its argument's value at `w` agrees with
+intensional application at `w` for every argument exactly when the function, read as an operator
+on intensions, is extensional at `w`. -/
+theorem forall_eval_intensionalLeft_eq_iff {σ τ : Ty} {f : W → (W → Ty.Domain E W σ S) →
+    Ty.Domain E W τ S} {w : W} :
+    (∀ a, intensionalLeft.intension f a w = intensionalLeft.eval (f w) (a w)) ↔
+      IsExtensionalAt (fun a w' ↦ f w' a) w :=
+  isExtensionalAt_iff_forall_const.symm
+
 /-- The denotation of a mode under an applicative effect, which runs the left daughter's
 computation first. -/
 def evalM {M : Type → Type} [Applicative M] (m : Mode σ₁ σ₂ τ) (a : M (Ty.Domain E W σ₁ S))
diff --git a/Linglib/Semantics/Composition/Model.lean b/Linglib/Semantics/Composition/Model.lean
index bfcac434ec..531fa0b399 100644
--- a/Linglib/Semantics/Composition/Model.lean
+++ b/Linglib/Semantics/Composition/Model.lean
@@ -4,25 +4,28 @@ public import Linglib.Semantics.Composition.Ty
 public import Mathlib.ModelTheory.Basic
 
 /-!
-# Model-theoretic semantics for type-driven composition
+# Models for type-driven composition
 
-A composition model is a mathlib first-order structure on one entity domain at each world of a
-world set. The symbols of the signature denote what the structure gives them, read off through
-`Structure.funMap` and `Structure.RelMap` as DRT reads off the truth of atomic conditions
-(`Semantics/Dynamic/DRS/`), and world dependence stays in the `.intens` types. The words of a
-first-order fragment translate to these symbols (`Composition/FirstOrder.lean`).
+A *model* for a first-order fragment has a domain of individuals, a set of worlds, and at each
+world an interpretation of the fragment's names and predicates: a name denotes an individual
+there, and a predicate the individuals, or pairs of individuals, that it holds of there. The
+individuals are the same at every world, as in a constant-domain Kripke model, while what a
+predicate holds of varies from world to world. The words of a first-order fragment translate to
+the model's symbols in `Composition/FirstOrder.lean`.
 
 ## Main definitions
 
-* `Model`: an entity domain `E`, worlds `W`, and a structure `interp w` at each world.
-* `Model.const`, `Model.pred₁`, `Model.pred₂`: the denotations of a constant and of unary
-  and binary relation symbols at a world.
+* `Montague.Model`: an entity domain `E`, worlds `W`, and a structure `interp w` at each world.
+* `Montague.Model.const`, `Montague.Model.pred₁`, `Montague.Model.pred₂`: the denotations of a
+  constant and of unary and binary relation symbols at a world.
 
 ## Implementation notes
 
-`interp : W → L.Structure E` carries structures as terms rather than instances, since a
-world-indexed family of structures on one carrier cannot be instance-based; formulas are
-realized at a world by `Formula.RealizeAt m.interp w`. The concrete toy model of
+The interpretation at a world is a mathlib first-order structure `L.Structure E`, carried as a
+term rather than an instance, since a family of structures on one carrier indexed by worlds
+cannot be found by instance search. Symbols are read off through `Structure.funMap` and
+`Structure.RelMap`, as DRT reads off the truth of atomic conditions (`Semantics/Dynamic/DRS/`),
+and a formula is realized at a world by `Formula.RealizeAt m.interp w`. The concrete toy model of
 `Studies/HeimKratzer1998` follows mathlib's concrete-language idiom.
 
 ## References
diff --git a/Linglib/Semantics/Composition/Partial.lean b/Linglib/Semantics/Composition/Partial.lean
index 6006f9fbaf..675bff6d87 100644
--- a/Linglib/Semantics/Composition/Partial.lean
+++ b/Linglib/Semantics/Composition/Partial.lean
@@ -7,19 +7,13 @@ public import Linglib.Semantics.Composition.Tree
 /-!
 # Partial interpretation
 
-This file is Heim and Kratzer's composition engine on partial denotations. A function denotes a
-partial function, mathlib's `PFun`, whose domain is the definedness condition the book attaches
-to a lexical entry, and a node denotes a `Part` value of its type, defined when its daughters are
-and the function among them is defined at its argument. The engine evaluates the term a tree
-translates to (`PhraseStructure.Tree.translate`), so it composes by the same modes as the total
-engine (`Montague.Mode.evalPartial`); a trace denotes the value of its index and a binder
-abstracts over its index, the abstract being a partial function that is undefined wherever the
-body is. Predicate Abstraction therefore needs no distributor.
-
-The book's distinction between uninterpretability and presupposition failure (§4.4.4) is the
-difference between the engine returning no denotation and returning an undefined one:
-`Uninterpretable` is decided by the types of the leaves alone (`uninterpretable_congr`), and
-`PresupFailure` asks after the denotations.
+A word with a definedness condition, such as the definite article, denotes a partial function in
+Heim and Kratzer. A node has a value only where its daughters do and the function among them is
+defined at its argument, and a sentence that composes but has no value suffers presupposition
+failure, as distinct from uninterpretability, where the types do not compose.
+[Every mode is strict](##dom_right_of_dom_evalPartial), and on a lexicon lifting a total one
+[the partial engine's values lift the total engine's](##interpPartial_lifts), so such a lexicon
+[has no presupposition failure](##not_presupFailure_of_lifts).
 
 ## Main definitions
 
@@ -32,25 +26,18 @@ difference between the engine returning no denotation and returning an undefined
 * `Montague.Ty.Lifts`, `Montague.Denotation.Lifts`: the relation of a total denotation to a
   partial one lifting it, with `Montague.Ty.Domain.toPartial` the lift at a first-order type.
 
-## Main results
-
-* `Montague.Mode.dom_left_of_dom_evalPartial`, `Montague.Mode.dom_right_of_dom_evalPartial`:
-  every mode is strict, so no word turns an undefined argument into a defined value.
-* `PhraseStructure.Tree.uninterpretable_congr`: uninterpretability depends on the leaves' types
-  alone.
-* `PhraseStructure.Tree.interpPartial_lifts`: on a lexicon lifting a total one the partial
-  engine's values lift the pure engine's, every mode preserving the lift
-  (`Montague.Mode.lifts_evalPartial`), so such a lexicon has no presupposition failure
-  (`PhraseStructure.Tree.not_presupFailure_of_lifts`).
-
 ## Implementation notes
 
-`Ty.PDomain` interprets a function type by the partial functions `a → Part b`, with partiality
-inside the arrow: the call-by-value monadic interpretation of the types at `Part`, of which
-`Ty.Domain` is the case at `Id`. The effectful engine of `Composition/Tree.lean` at `M = Part` is
-a different engine, with partiality outside the arrow, `Part (a → b)`. There a Fregean definite,
-defined on some predicates and undefined on others, has no value, and Predicate Abstraction would
-be defined only where the body is defined at every entity.
+A partial function is mathlib's `PFun`, and a node denotes a `Part` value of its type. The engine
+evaluates the term a tree translates to (`PhraseStructure.Tree.translate`), so Predicate
+Abstraction needs no distributor; uninterpretability is the engine returning no denotation, and
+presupposition failure its returning an undefined one. `Ty.PDomain` interprets a function type by
+the partial functions `a → Part b`, with partiality inside the arrow: the call-by-value monadic
+interpretation of the types at `Part`, of which `Ty.Domain` is the case at `Id`. The effectful
+engine of `Composition/Tree.lean` at `M = Part` is a different engine, with partiality outside the
+arrow, `Part (a → b)`. There a Fregean definite, defined on some predicates and undefined on
+others, has no value, and Predicate Abstraction would be defined only where the body is defined
+at every entity.
 
 ## References
 
diff --git a/Linglib/Semantics/Composition/Term.lean b/Linglib/Semantics/Composition/Term.lean
index a7d7616bf2..0283550940 100644
--- a/Linglib/Semantics/Composition/Term.lean
+++ b/Linglib/Semantics/Composition/Term.lean
@@ -5,35 +5,28 @@ public import Linglib.Semantics.Composition.Mode
 public import Linglib.Semantics.Composition.Assignment
 
 /-!
-# Terms of the composition modes
+# Logical forms as terms
 
-A logical form is a term: the constants its words translate to, the variables of type `e` its
-traces bind, the abstraction over such a variable, and the composition of two terms by a mode
-(`Montague.Term`). Every interpretation of the trees is an evaluation of their terms: the
-denotation under an assignment of the variables (`Montague.Term.eval`), whose variable and
-abstraction cases are Heim and Kratzer's Traces and Pronouns Rule and Predicate Abstraction; the
-denotation under an applicative effect, where abstraction needs the effect to distribute over
-functions (`Montague.Term.evalM`); and the partial denotation of `Composition/Partial.lean`. Trees translate
-to terms in `Composition/Tree.lean`.
+A logical form is a term, built from the constants its words translate to, variables for the
+individuals its traces denote, abstraction, and composition by a mode. Its denotation under an
+assignment follows [the Traces and Pronouns Rule](##eval_var) and
+[Predicate Abstraction](##eval_lam), and its intension, under words interpreted as intensions, is
+its denotation at every world; the denotation is
+[the case of words that do not vary with the world](##intension_const_interp). Under an effect,
+such as a set of readings, a term denotes a computation.
 
 ## Main definitions
 
 * `Montague.Term`: the terms over a signature of constants.
 * `Montague.Term.eval`, `Montague.Term.evalM`: the denotation of a term, pure and under an
   applicative effect.
-
-## Main results
-
-* `Montague.Term.eval_var`, `Montague.Term.eval_lam`: a variable denotes the value of its index and
-  an abstraction by `lambdaAbsG`.
-* `Montague.Term.evalM_id`: at the identity effect, evaluation is the pure denotation.
-* `Montague.Term.evalM_congr_of_agree`: a term's denotation depends on the assignment only at its
-  free variables.
+* `Montague.Term.intension`: the intension of a term, its denotation at each world.
 
 ## Implementation notes
 
 Variables are named by the trace indices, so a binder with index `n` translates to the
-abstraction over the variable `n`, and translation needs no fresh names.
+abstraction over the variable `n`, and translation needs no fresh names. Trees translate to terms
+in `Composition/Tree.lean`, and the partial denotation of a term is in `Composition/Partial.lean`.
 
 Under an effect, the body of an abstraction is a computation at each entity, and the abstract is
 the computation of a function that `Distributive` gives. Scope effects such as continuations do
@@ -46,6 +39,7 @@ more than the constant functions (`SetM.not_preservesConst`).
 
 * [heim-kratzer-1998]
 * [montague-1973]
+* [von-fintel-heim-2011]
 * [kratzer-shimoyama-2002]
 * [shan-2004]
 * [charlow-2020]
@@ -73,7 +67,7 @@ namespace Term
 
 variable {K K' : Ty → Type*}
 
-/-- Rename the constants of a term. -/
+/-- The term with its constants renamed by `f`. -/
 def map (f : ∀ {ty : Ty}, K ty → K' ty) : {ty : Ty} → Term K ty → Term K' ty
   | _, const c => const (f c)
   | _, var n => var n
@@ -120,9 +114,34 @@ theorem eval_lam (I : ∀ {ty : Ty}, K ty → Ty.Domain E W ty S) (g : Assignmen
     {τ : Ty} (b : Term K τ) : (lam n b).eval I g = lambdaAbsG n (fun g' ↦ b.eval I g') g :=
   rfl
 
-/-- `evalM I g t` is the denotation of `t` under an applicative effect, given an interpretation
-`I` of the constants as computations and an assignment `g`. A composition runs its left daughter
-first, and an abstraction distributes the effect over the entities. -/
+/-- The intension of a term under an interpretation `I` of the constants as intensions and an
+assignment of the variables: at each world, a constant denotes its intension's value there and a
+composition composes the daughters' intensions by its mode (`Mode.intension`). -/
+def intension (I : ∀ {ty : Ty}, K ty → W → Ty.Domain E W ty S) (g : Assignment E) :
+    {ty : Ty} → Term K ty → W → Ty.Domain E W ty S
+  | _, const c => I c
+  | _, var n => fun _ ↦ g n
+  | _, lam n b => fun w x ↦ intension I (g[n ↦ x]) b w
+  | _, comp m l r => m.intension (intension I g l) (intension I g r)
+
+/-- Under constants that do not vary with the world, a term's intension is constant at its
+denotation, so the evaluation `eval` is the case of a lexicon of rigid intensions. -/
+@[simp] theorem intension_const_interp (I : ∀ {ty : Ty}, K ty → Ty.Domain E W ty S)
+    (g : Assignment E) {ty : Ty} (t : Term K ty) (w : W) :
+    t.intension (fun c _ ↦ I c) g w = t.eval I g := by
+  induction t generalizing g w with
+  | const c => rfl
+  | var n => rfl
+  | lam n b ih => funext x; exact ih _ w
+  | comp m l r ihl ihr =>
+    simp only [intension, eval]
+    rw [show l.intension (fun c _ ↦ I c) g = fun _ ↦ l.eval I g from funext (ihl g),
+      show r.intension (fun c _ ↦ I c) g = fun _ ↦ r.eval I g from funext (ihr g),
+      Mode.intension_const]
+
+/-- The denotation of a term under an applicative effect, given an interpretation `I` of the
+constants as computations and an assignment `g`. A composition runs its left daughter first, and
+an abstraction distributes the effect over the entities. -/
 def evalM {M : Type → Type} [Applicative M] [Distributive M]
     (I : ∀ {ty : Ty}, K ty → M (Ty.Domain E W ty S)) (g : Assignment E) :
     {ty : Ty} → Term K ty → Option (M (Ty.Domain E W ty S))
@@ -150,6 +169,15 @@ theorem eval_map (I : ∀ {ty : Ty}, K' ty → Ty.Domain E W ty S) (f : ∀ {ty
   | lam n b ih => funext x; exact ih _
   | comp m l r ihl ihr => simp only [map, eval, ihl, ihr]
 
+theorem intension_map (I : ∀ {ty : Ty}, K' ty → W → Ty.Domain E W ty S)
+    (f : ∀ {ty : Ty}, K ty → K' ty) (g : Assignment E) {ty : Ty} (t : Term K ty) :
+    (t.map f).intension I g = t.intension (fun c ↦ I (f c)) g := by
+  induction t generalizing g with
+  | const c => rfl
+  | var n => rfl
+  | lam n b ih => funext w x; exact congrFun (ih _) w
+  | comp m l r ihl ihr => simp only [map, intension, ihl, ihr]
+
 theorem evalM_map {M : Type → Type} [Applicative M] [Distributive M]
     (I : ∀ {ty : Ty}, K' ty → M (Ty.Domain E W ty S)) (f : ∀ {ty : Ty}, K ty → K' ty)
     (g : Assignment E) {ty : Ty} (t : Term K ty) :
diff --git a/Linglib/Semantics/Composition/Tree.lean b/Linglib/Semantics/Composition/Tree.lean
index 9ae6c86d3c..31567ee8b8 100644
--- a/Linglib/Semantics/Composition/Tree.lean
+++ b/Linglib/Semantics/Composition/Tree.lean
@@ -4,45 +4,39 @@ public import Linglib.Syntax.Tree.Basic
 public import Linglib.Semantics.Composition.Term
 
 /-!
-# Type-driven interpretation
+# Type-driven interpretation of trees
 
-This file interprets phrase-structure trees by type-driven composition over an effect functor
-`M`. A tree translates to a term of the composition modes (`PhraseStructure.Tree.translate`), and
-its denotation is the evaluation of that term (`PhraseStructure.Tree.interp`), as in Montague's
-theory of translation. The modes are Heim and Kratzer's, with the intensional application of von
-Fintel and Heim and the event identification of Kratzer; the effect functor follows Bumford and
-Charlow. Translation is the only type-driven step, and Predicate Abstraction distributes the
-effect over the entities (`Distributive`).
+Type-driven interpretation gives each node of a tree the meaning that the mode its daughters'
+types select makes of its daughters' meanings, with traces and binders interpreted by an
+assignment as in Heim and Kratzer. As in Montague's theory of translation,
+[a tree's denotation is the evaluation of the term it translates to](##interp_eq_eval_translate),
+and [it depends on the assignment only at the tree's free traces](##interp_congr_of_agree).
+Denotations may be computations under an effect, after Bumford and Charlow, and under a lexicon of
+intensions a tree has an intension, [constant at its denotation when no word varies with the
+world](##intension_const).
 
 ## Main definitions
 
-* `Montague.Lexicon`: a string-keyed lexicon of effectful denotations.
+* `Montague.Lexicon`: a lexicon of effectful denotations, keyed by strings.
 * `PhraseStructure.Tree.translate`: the term a tree translates to.
-* `PhraseStructure.Tree.interp`: the denotation of a tree under an assignment, the evaluation of
-  its term; a binary node composes by the mode `Montague.Ty.mode?` selects.
-* `PhraseStructure.Tree.ty?`: the type a tree composes to, from the types of its leaves alone.
+* `PhraseStructure.Tree.interp`: the denotation of a tree under an assignment.
+* `PhraseStructure.Tree.ty?`: the type a tree composes to, from the types of its words alone.
 * `PhraseStructure.Tree.readings`: the readings of a tree under a lexicon of sets of readings.
 * `PhraseStructure.Tree.HoldsAt`: the truth of a tree under a lexicon and an assignment.
-
-## Main results
-
-* `interp_eq_eval_translate`: a tree's denotation is the evaluation of its term.
-* `interp_map_fst`: the type of a tree's denotation is the type `ty?` computes.
-* `interp_congr_of_agree` and its corollaries: Heim and Kratzer's theorems on variable binding.
-* `readings_eq_of_choice`, `mem_readings_node_binary`: readings extend the engine and compose
-  pointwise.
-* `translate_map_const`, `translate_rel`: translation respects renaming and relating constants.
+* `PhraseStructure.Tree.intension`: the intension of a tree under a lexicon of intensions.
 
 ## Implementation notes
 
 The tree operations live in the namespace `PhraseStructure.Tree`, so that `t.interp lex g` works.
-Binary nodes sequence effects left to right, whichever daughter is the function, so at
-`M = Cont R` the engine derives surface scope only: inverse scope needs an evaluation order
-chosen per node, which the engine does not provide (`Studies/Barker2002.lean` marks each rule
-with a permutation of its daughters). Predicate Abstraction needs the effect to distribute over
-functions, `(E → M (Ty.Domain ty)) → M (E → Ty.Domain ty)`. The abstraction's fallback value
-`valueAt` is never reached, since types do not depend on the assignment. The category of a node
-is ignored, composition being type-driven.
+Translation is the only type-driven step, and translation respects renaming and relating
+constants (`translate_map_const`, `translate_rel`). Binary nodes sequence effects left to right,
+whichever daughter is the function, so at `M = Cont R` the engine derives surface scope only:
+inverse scope needs an evaluation order chosen per node, which the engine does not provide
+(`Studies/Barker2002.lean` marks each rule with a permutation of its daughters). Predicate
+Abstraction needs the effect to distribute over functions,
+`(E → M (Ty.Domain ty)) → M (E → Ty.Domain ty)`. The abstraction's fallback value `valueAt` is
+never reached, since types do not depend on the assignment. The category of a node is ignored,
+composition being type-driven.
 
 ## References
 
@@ -114,7 +108,7 @@ section Translate
 
 variable {C : Type} {K : Ty → Type*} {L : Type*}
 
-/-- Translate the tree `t` into a term by the composition principles of [heim-kratzer-1998]. A
+/-- The term a tree translates to, by the composition principles of [heim-kratzer-1998]. A
 terminal goes to its word's constant, a non-branching node to its daughter's term, a binary node to
 its daughters' terms composed by the mode their types select, a trace to the variable of its index,
 and a binder to the abstraction over that variable. -/
@@ -835,6 +829,43 @@ theorem interp_eq_eval_translate (I : ∀ {ty : Ty}, K ty → Ty.Domain E W ty S
 
 end Translation
 
+/-! ### Intensions -/
+
+section Intension
+
+variable {C : Type} {K : Ty → Type*} {L : Type*} {E W : Type} {S : Sorts}
+
+/-- The intension of a tree under a lexicon of intensions and an assignment, the intension of its
+term ([von-fintel-heim-2011]). -/
+def intension (lex : L → Option (Σ ty, W → Ty.Domain E W ty S)) (g : Assignment E)
+    (t : Tree C L) : Option (Σ ty, W → Ty.Domain E W ty S) :=
+  (translate (K := fun ty ↦ W → Ty.Domain E W ty S) lex t).map fun d ↦
+    ⟨d.1, d.2.intension (fun c ↦ c) g⟩
+
+theorem intension_eq_intension_translate (I : ∀ {ty : Ty}, K ty → W → Ty.Domain E W ty S)
+    (lex : L → Option (Σ ty, K ty)) (g : Assignment E) (t : Tree C L) :
+    intension (fun w ↦ (lex w).map fun c ↦ ⟨c.1, I c.2⟩) g t =
+      (translate lex t).map fun d ↦ ⟨d.1, d.2.intension I g⟩ := by
+  simp only [intension, translate_map_const]
+  cases translate lex t with
+  | none => rfl
+  | some d => simp [Term.intension_map]
+
+/-- Under a lexicon of rigid intensions, a tree's intension is constant at its denotation. -/
+theorem intension_const (lex : L → Option (Σ ty, Ty.Domain E W ty S)) (g : Assignment E)
+    (t : Tree C L) :
+    intension (fun x ↦ (lex x).map fun d ↦ ⟨d.1, fun _ ↦ d.2⟩) g t =
+      (interp (M := Id) lex g t).map fun d ↦ ⟨d.1, fun _ ↦ d.2⟩ := by
+  have h : interp (M := Id) lex g t = (translate lex t).map fun d ↦ ⟨d.1, d.2.eval (fun c ↦ c) g⟩ :=
+    by simpa [Sigma.eta] using
+      interp_eq_eval_translate (K := fun ty ↦ Ty.Domain E W ty S) (fun c ↦ c) lex g t
+  rw [intension_eq_intension_translate (K := fun ty ↦ Ty.Domain E W ty S) (fun c _ ↦ c), h]
+  cases translate lex t with
+  | none => rfl
+  | some d =>
+    simp only [Option.map_some]; congr; funext w; exact Term.intension_const_interp _ _ _ w
+
+end Intension
 
 /-! ### Truth -/
 
diff --git a/Linglib/Semantics/Composition/Ty.lean b/Linglib/Semantics/Composition/Ty.lean
index 2483af8fc4..1b9040dd11 100644
--- a/Linglib/Semantics/Composition/Ty.lean
+++ b/Linglib/Semantics/Composition/Ty.lean
@@ -6,26 +6,29 @@ public import Mathlib.Order.CompleteBooleanAlgebra
 /-!
 # Semantic types and denotation domains
 
-Montague's semantic types and their denotation domains. `Ty` has Montague's `e`, `t`, `⟨a,b⟩`
-and `⟨s,a⟩` together with the degree, cardinality and eventuality sorts of later work, and
-`Ty.Domain E W ty S` is the domain of possible denotations of a type, given an entity type `E`
-and an index type `W`, as in Montague's universal grammar, and the carriers `S` of the later
-sorts. Functions denote in function spaces and intensions in `W`-indexed families, so a
-denotation is an ordinary Lean term and composition is function application.
-
-`Ty.Domain` is reducible: a denotation of type `⟨e,t⟩` *is* an `E → Prop` to every tactic and
-instance, and the pointwise Boolean algebra of a type that ends in `t` is mathlib's `Pi`
-instance. `Ty.Domain.completeBooleanAlgebra?` computes that algebra, which is complete, by
-recursion on the type, for the composition engine's runtime type dispatch.
+In Montague semantics every expression has a *semantic type*, which fixes the kind of thing it
+denotes: an individual ($e$), a truth value ($t$), a function from denotations of type $a$ to
+denotations of type $b$ ($\langle a,b\rangle$), or an *intension* ($\langle s,a\rangle$), a
+function from worlds to denotations of type $a$. Later work adds sorts for degrees, cardinalities,
+and events and states. Each type has a *domain* of possible denotations, built from a set of
+individuals and a set of worlds, and the domain of a type that ends in $t$ is a Boolean algebra,
+pointwise.
 
 ## Main definitions
 
-* `Ty`: semantic types.
-* `Sorts`: the carriers of the degree and eventuality sorts.
-* `Ty.Domain E W ty S`: the denotation domain of `ty`.
-* `Denotation E W M S`: a semantic type with an `M`-computation in its domain.
-* `Ty.Domain.completeBooleanAlgebra?`: the pointwise complete Boolean algebra of a conjoinable
-  type, `none` on a type that does not end in `t`.
+* `Montague.Ty`: semantic types.
+* `Montague.Sorts`: the carriers of the degree and eventuality sorts.
+* `Montague.Ty.Domain E W ty S`: the denotation domain of `ty`.
+* `Montague.Denotation E W M S`: a semantic type with an `M`-computation in its domain.
+* `Montague.Ty.Domain.completeBooleanAlgebra?`: the pointwise complete Boolean algebra of a
+  type that ends in `t`, `none` on any other type.
+
+## Implementation notes
+
+`Ty.Domain` is reducible: a denotation of type `⟨e,t⟩` *is* an `E → Prop` to every tactic and
+instance, and the Boolean algebra of a type that ends in `t` is mathlib's `Pi` instance.
+`Ty.Domain.completeBooleanAlgebra?` computes that algebra by recursion on the type, for the
+composition engine's dispatch on types at run time.
 
 ## References
 
diff --git a/Linglib/Semantics/Composition/WithAlternatives.lean b/Linglib/Semantics/Composition/WithAlternatives.lean
index 5502a6e37f..9b9e833f5e 100644
--- a/Linglib/Semantics/Composition/WithAlternatives.lean
+++ b/Linglib/Semantics/Composition/WithAlternatives.lean
@@ -17,27 +17,27 @@ A meaning in alternative semantics is a pair: an ordinary denotation, and a set
 that focus features and operators manipulate while leaving the ordinary denotation alone.
 `WithAlternatives` is that pair. It is the product of the identity monad and the set monad, so the
 two-dimensional recursion of alternative semantics is `<$>` and `<*>` of a lawful `Monad`, and the
-two dimensions are its two monad morphisms. The monad lives in one universe; binary composition
-across universes is `WithAlternatives.map₂`, the same composition with `Set.image2` as its
-alternatives.
+two dimensions are its two monad morphisms: an application's ordinary value is the
+application of the ordinary values, and
+[its alternatives are the applications of the alternatives](##mem_alternatives_seq).
+[Composition does not depend on the order of the daughters](##seq_eq_bind_seq_pure), so an
+application can bind its argument first, and
+[a Given function contributes only its ordinary value](##Given.alternatives_seq).
 
 ## Main definitions
 
-* `WithAlternatives` — an ordinary value together with the alternatives it evokes
-* `WithAlternatives.unfeatured`, `WithAlternatives.focused` — the meanings of an unfocused and
-  of an F-marked expression, evoking only their own value and every value respectively
-* `WithAlternatives.WellFormed` — the containment constraint: the alternatives include the
-  ordinary value
-* `WithAlternatives.Given` — the alternatives have collapsed to a singleton
-* `WithAlternatives.map₂` — binary composition, alternatives composed pointwise
+* `WithAlternatives`: an ordinary value together with the alternatives it evokes.
+* `WithAlternatives.unfeatured`, `WithAlternatives.focused`: the meanings of an unfocused and of
+  an F-marked expression, evoking only their own value and every value respectively.
+* `WithAlternatives.WellFormed`: the containment constraint, that the alternatives include the
+  ordinary value.
+* `WithAlternatives.Given`: the alternatives have collapsed to a singleton.
+* `WithAlternatives.map₂`: binary composition, alternatives composed pointwise.
 
-## Main results
+## Implementation notes
 
-* `ordinary_seq`, `mem_alternatives_seq` — the two dimensions of Hamblin composition
-* `alternatives_seq` — the alternatives of an application are those of the `Set` applicative
-* `CommApplicative WithAlternatives`, `seq_eq_bind_seq_pure` — composition does not depend on the
-  order of the daughters, so an application can bind its argument first
-* `Given.alternatives_seq` — a Given function contributes only its ordinary value
+The monad lives in one universe; binary composition across universes is `WithAlternatives.map₂`,
+the same composition with `Set.image2` as its alternatives.
 
 ## References
 
@@ -54,8 +54,8 @@ alternatives.
 structure WithAlternatives (α : Type*) where
   /-- The denotation the expression would have with no focus on it. -/
   ordinary : α
-  /-- The alternatives, which by Rooth's containment constraint include the ordinary value — see
-  `WellFormed`, kept a predicate rather than a field so that the composition engine below is a
+  /-- The alternatives the expression evokes. Rooth's containment constraint, that they include
+  the ordinary value, is the predicate `WellFormed` rather than a field, so that composition is a
   `Monad`. -/
   alternatives : Set α
 
diff --git a/Linglib/Semantics/Composition/Writer.lean b/Linglib/Semantics/Composition/Writer.lean
index 2eb832ad8b..cd7014a5a2 100644
--- a/Linglib/Semantics/Composition/Writer.lean
+++ b/Linglib/Semantics/Composition/Writer.lean
@@ -8,20 +8,15 @@ public import Mathlib.Control.Monad.Writer
 A computation of the writer monad `Writer ω` yields a value and logs output in `ω`. Giorgolo and
 Asudeh model conventional implicature this way, in Shan's monadic program: the value of an
 expression is its at-issue content, the log collects the side-issue propositions of its parts,
-`pure` logs nothing and `bind` appends the logs. Forgetting the log is a monad morphism to `Id`,
-and `bind` only extends the log, so content flows from the at-issue dimension into the side-issue
-one and never back.
+`pure` logs nothing and `bind` appends the logs. [Forgetting the log](##val_bind) is a monad
+morphism to `Id`, and [`bind` only extends the log](##log_prefix_bind), so content flows from the
+at-issue dimension into the side-issue one and never back.
 
 ## Main definitions
 
 * `Writer.val`, `Writer.log`: the value and the log of a computation.
 * `WriterT.instLawfulMonadList`: the monad laws for list logs, over any lawful monad.
 
-## Main results
-
-* `Writer.val_pure`, `Writer.val_bind`: forgetting the log is a monad morphism.
-* `Writer.log_prefix_bind`: the log of `m` is a prefix of the log of `m >>= f`.
-
 ## Implementation notes
 
 * Mathlib's two `Monad` instances on `Writer ω`, for `[Monoid ω]` and for
@@ -60,7 +55,7 @@ namespace Writer
 
 variable {ω A B : Type u}
 
-/-- `Writer.mk a w` is the computation with value `a` and log `w`. -/
+/-- The computation with value `a` and log `w`. -/
 protected def mk (a : A) (w : ω) : Writer ω A := WriterT.mk (a, w)
 
 /-- The value of a computation is the first component of its run. -/
diff --git a/Studies/HeimKratzer1998.lean b/Studies/HeimKratzer1998.lean
index c67a719541..183cd86244 100644
--- a/Studies/HeimKratzer1998.lean
+++ b/Studies/HeimKratzer1998.lean
@@ -18,13 +18,20 @@ denotations, with a Fregean definite article that may leave a node undefined. Th
 engines `Tree.interp` and `Tree.interpPartial` implement these rules. Here the book's rules are
 transcribed as interpretation relations that the engines extend, and the engines are run on the
 toy model for the book's definite descriptions (Chapter 4), relative clauses (Chapter 5) and
-quantifier scope (Chapter 7).
+quantifier scope (Chapter 7). For attitude reports (Chapter 12) the interpretation is relative to a
+world (`Tree.intension`), and Intensional Functional Application feeds *believes* the intension of
+its complement, so that *Mary believes Jan is loyal* and *Jan is loyal*, *Dick is deceitful* can
+be true while *Mary believes Dick is deceitful* is false. Interpreted at one world, a complement of
+*believes* is its truth value, and the verb's complement is a nonextensional context exactly when
+the subject's beliefs leave open another world.
 
 ## Implementation notes
 
 The toy fragment's words stand in for the book's: *student who sleeps* for *house which is
 empty*, *every person sees some person* for "Some publisher offended every linguist". With
-`interpTy .t = Prop` the engines produce truth conditions as propositions.
+`interpTy .t = Prop` the engines produce truth conditions as propositions. In Chapter 12 *is* is
+the identity on predicates, the book's emptiness of *is*, and (11d) is the falsity of (10) at the
+actual world, since the fragment has no negation.
 
 ## References
 
@@ -786,4 +793,90 @@ example (g : Assignment ToyEntity) :
 
 end LogicalForm
 
+/-! ### Intensional semantics (Chapter 12)
+
+The interpretation function depends on a world as well as an assignment, predicates vary with
+the world, and an attitude verb is necessity along what its subject believes, knows or hopes,
+taking a proposition of type `⟨s,t⟩`. Intensional Functional Application feeds the verb its
+complement's intension, which `Tree.intension` computes. -/
+
+section Intensional
+
+open ModalLogic SetRel
+
+variable {E W : Type} (loyal deceitful : W → E → Prop) (believes : E → SetRel W W)
+  (mary jan dick : E)
+
+/-- The fragment's words as intensions: names are constant, *loyal* and *deceitful* are easy
+predicates, *is* is empty, and *believes* is necessity along what its subject believes. -/
+def intensionalLexicon : String → Option (Σ ty, W → Ty.Domain E W ty)
+  | "Mary" => some ⟨.e, fun _ ↦ mary⟩
+  | "Jan" => some ⟨.e, fun _ ↦ jan⟩
+  | "Dick" => some ⟨.e, fun _ ↦ dick⟩
+  | "is" => some ⟨(.e ⇒ .t) ⇒ .e ⇒ .t, fun _ P ↦ P⟩
+  | "loyal" => some ⟨.e ⇒ .t, fun w x ↦ loyal w x⟩
+  | "deceitful" => some ⟨.e ⇒ .t, fun w x ↦ deceitful w x⟩
+  | "believes" => some ⟨.intens .t ⇒ .e ⇒ .t, fun w p x ↦ □[believes x] p w⟩
+  | _ => none
+
+/-- *Jan is loyal*. -/
+def janIsLoyal : Tree Unit String := .bin (.leaf "Jan") (.bin (.leaf "is") (.leaf "loyal"))
+
+/-- *Dick is deceitful*. -/
+def dickIsDeceitful : Tree Unit String :=
+  .bin (.leaf "Dick") (.bin (.leaf "is") (.leaf "deceitful"))
+
+/-- *Mary believes Jan is loyal*. -/
+def maryBelievesJanIsLoyal : Tree Unit String :=
+  .bin (.leaf "Mary") (.bin (.leaf "believes") janIsLoyal)
+
+/-- *Mary believes Dick is deceitful*. -/
+def maryBelievesDickIsDeceitful : Tree Unit String :=
+  .bin (.leaf "Mary") (.bin (.leaf "believes") dickIsDeceitful)
+
+-- (8), p. 308: true at `w` iff Jan is loyal at every world compatible with what Mary believes
+-- in `w`
+theorem intension_maryBelievesJanIsLoyal (g : Assignment E) :
+    Tree.intension (intensionalLexicon loyal deceitful believes mary jan dick) g
+      maryBelievesJanIsLoyal = some ⟨.t, fun w ↦ □[believes mary] (loyal · jan) w⟩ :=
+  rfl
+
+-- p. 300: interpreted at the lexicon's values at one world, a complement of *believes* is its
+-- truth value, so two true complements make the reports agree
+theorem interp_maryBelieves_eq {w : W} (g : Assignment E) (h : loyal w jan ↔ deceitful w dick) :
+    let lex := fun s ↦ (intensionalLexicon loyal deceitful believes mary jan dick s).map
+      fun d ↦ (⟨d.1, d.2 w⟩ : Denotation E W)
+    Tree.interp lex g maryBelievesJanIsLoyal = Tree.interp lex g maryBelievesDickIsDeceitful := by
+  change (some ⟨.t, □[believes mary] (fun _ ↦ loyal w jan) w⟩ : Option (Denotation E W)) =
+    some ⟨.t, □[believes mary] (fun _ ↦ deceitful w dick) w⟩
+  rw [propext h]
+
+/-- An attitude verb's complement is a nonextensional context at `w` exactly when the subject's
+attitude at `w` leaves open a world other than `w`, so the truth value of the complement fixes the
+report only for a subject who rules out every other world (p. 300). -/
+theorem believes_isExtensionalAt_iff {x : E} {w : W} :
+    Montague.IsExtensionalAt (fun p w' ↦ □[believes x] p w') w ↔ ∀ v, w ~[believes x] v → v = w :=
+  Montague.isExtensionalAt_box_iff
+
+/-- The two worlds of the model for (11). -/
+inductive Ch12World | actual | other
+
+/-- The individuals of the model for (11). -/
+inductive Ch12Person | mary | jan | dick
+
+/-- (11), p. 309: Jan is loyal and Dick deceitful at the actual world, Mary believes that Jan is
+loyal, and she does not believe that Dick is deceitful, since her beliefs leave open a world where
+he is not. -/
+theorem janIsLoyal_dickIsDeceitful_maryBelieves (g : Assignment Ch12Person) :
+    let lex := intensionalLexicon (W := Ch12World) (fun _ x ↦ x = .jan)
+      (fun w x ↦ w = .actual ∧ x = .dick) (fun _ ↦ Set.univ) .mary .jan .dick
+    (∃ p, Tree.intension lex g janIsLoyal = some ⟨.t, p⟩ ∧ p .actual) ∧
+      (∃ p, Tree.intension lex g dickIsDeceitful = some ⟨.t, p⟩ ∧ p .actual) ∧
+      (∃ p, Tree.intension lex g maryBelievesJanIsLoyal = some ⟨.t, p⟩ ∧ p .actual) ∧
+      ∃ p, Tree.intension lex g maryBelievesDickIsDeceitful = some ⟨.t, p⟩ ∧ ¬ p .actual :=
+  ⟨⟨_, rfl, rfl⟩, ⟨_, rfl, rfl, rfl⟩, ⟨_, rfl, fun _ _ ↦ rfl⟩,
+    ⟨_, rfl, fun h ↦ nomatch (h .other trivial).1⟩⟩
+
+end Intensional
+
 end HeimKratzer1998
diff --git a/references.bib b/references.bib
index 07a1eef24e..be3227149b 100644
--- a/references.bib
+++ b/references.bib
@@ -10841,7 +10841,7 @@ @misc{von-fintel-heim-2011
   subfield  = {semantics/modality},
   role      = {cited},
   validated = {true},
-  sources   = {Semantics/Composition/Tree.lean;Semantics/Intensional/Rigidity.lean}
+  sources   = {Semantics/Composition/Mode.lean;Semantics/Composition/Term.lean;Semantics/Composition/Tree.lean}
 }
 @misc{von-fintel-2012,
   author    = {von Fintel, Kai},