The category of contexts

Indexed dynamic semantics is a category: objects are contexts (bases of live discourse referents), morphisms are Transitions, composition is world-pointwise relational composition. The identity and associativity laws are Transition.lean's id_comp/comp_id/comp_assoc.

The presheaf of state fibers is the composite of the possibilities presheaf with the powerset functor — definitionally, in this formulation: the predecessor proved the isomorphism typing states at the possibilities makes it the definition (State.presheaf). Restriction is Set.image along weakening, the ∃-leg of mathlib's Set.image_preimage/Set.preimage_kernImage triple ([Law69b]'s quantifiers as adjoints to weakening, as retold by [Jac99a]). Syntax categories interpret into Ctx (DRS/Category.lean); the fiber at ∅ is [Vel96]'s update semantics.

Main definitions

• Ctx W M V: bundled contexts, with a Category instance whose morphisms are Transitions between the bases.
• possibilities: the presheaf of world–assignment pairs at each granularity — a set-valued indexed category in [Jac99a]'s sense, its maps the semantic face of weakening. Precedent for the states-as-presheaf reading: [AS14].
• State.presheaf: the state fibers — possibilities ⋙ Set.
• possibilities_glue, possibilities_beck_chevalley: the context-lattice square is a pullback of possibilities, so quantification commutes with weakening — the fibers are a hyperdoctrine.
• elementsEquivPoints: the Grothendieck total of the family is the point type — the category of elements is the descent preorder on the points, opposed.

References

• [KvGR11]
• [MvBV11], [AS14]
• [Law69b], [Jac99a]
• [GS91a], [Mus96]

structure DynamicSemantics.Ctx (W : Type u_1) (M : Type u_2) (V : Type u_3) : Type u_3

A context: a base of live discourse referents, bundled as an object of the category whose morphisms are Transition W M X Y.

• base : Set V

  The live discourse referents.

theorem DynamicSemantics.Ctx.ext_iff {W : Type u_1} {M : Type u_2} {V : Type u_3} {x y : Ctx W M V} : x = y ↔ x.base = y.base

theorem DynamicSemantics.Ctx.ext {W : Type u_1} {M : Type u_2} {V : Type u_3} {x y : Ctx W M V} (base : x.base = y.base) : x = y

structure DynamicSemantics.Ctx.Hom {W : Type u_1} {M : Type u_2} {V : Type u_3} (X Y : Ctx W M V) : Type (max (max u_1 u_2) u_3)

Morphisms of contexts: transitions between the bases.

• t : Transition W M X.base Y.base

  The underlying transition.

theorem DynamicSemantics.Ctx.Hom.ext {W : Type u_1} {M : Type u_2} {V : Type u_3} {X Y : Ctx W M V} {x y : X.Hom Y} (t : x.t = y.t) : x = y

theorem DynamicSemantics.Ctx.Hom.ext_iff {W : Type u_1} {M : Type u_2} {V : Type u_3} {X Y : Ctx W M V} {x y : X.Hom Y} : x = y ↔ x.t = y.t

@[implicit_reducible]

instance DynamicSemantics.Ctx.instCategory {W : Type u_1} {M : Type u_2} {V : Type u_3} : CategoryTheory.Category.{max (max u_1 u_2) u_3, u_3} (Ctx W M V)

Equations

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

@[simp]

theorem DynamicSemantics.Ctx.t_id {W : Type u_1} {M : Type u_2} {V : Type u_3} (X : Ctx W M V) : (CategoryTheory.CategoryStruct.id X).t = Transition.id X.base

@[simp]

theorem DynamicSemantics.Ctx.t_comp {W : Type u_1} {M : Type u_2} {V : Type u_3} {X Y Z : Ctx W M V} (u : X ⟶ Y) (v : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp u v).t = u.t.comp v.t

The possibilities presheaf and the state fibers

def DynamicSemantics.possibilities (W : Type u) (M : Type v) (V : Type w) : CategoryTheory.Functor (Set V)ᵒᵖ (Type (max u v w))

The presheaf of possibilities: over X, world–assignment pairs at granularity X; restriction precomposes with the inclusion. A model read over the category of contexts — a set-valued indexed category in [Jac99a]'s sense, whose maps are the semantic face of weakening (the functor "which adds an extra dummy" variable, in the book's own gloss).

Equations

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

def DynamicSemantics.State.presheaf (W : Type u) (M : Type v) (V : Type w) : CategoryTheory.Functor (Set V)ᵒᵖ (Type (max u v w))

The state fibers as a presheaf on the poset of bases: the powerset functor applied fiberwise to the possibilities — by definition, in this formulation. The fiber over X is Set (W × (↑X → M)); restriction is direct image along weakening.

Equations

• DynamicSemantics.State.presheaf W M V = (DynamicSemantics.possibilities W M V).comp (CategoryTheory.ofTypeFunctor Set)

Gluing and Beck–Chevalley

possibilities sends each square of the context lattice to a pullback (possibilities_glue), so quantification and weakening cohere: the existential legs (Set.image, which is State.presheaf's own action) commute with reindexing (Set.preimage) across the square (possibilities_beck_chevalley). Together with mathlib's Set.image_subset_iff (∃ ⊣ weakening), Set.preimage_kernImage (weakening ⊣ ∀), and Set.image_inter_preimage (Frobenius), the fibers form a hyperdoctrine over the context lattice ([Law69b], [Jac99a]).

@[simp]

theorem DynamicSemantics.possibilities_map_apply {W : Type u_1} {M : Type u_2} {V : Type u_3} {X Y : Set V} (h : X ⊆ Y) (p : (possibilities W M V).obj (Opposite.op Y)) : (CategoryTheory.ConcreteCategory.hom ((possibilities W M V).map (CategoryTheory.homOfLE h).op)) p = (p.1, fun (v : ↑(Opposite.unop (Opposite.op X))) => p.2 ⟨↑v, ⋯⟩)

The action of possibilities on a lattice inequality, elementwise.

theorem DynamicSemantics.possibilities_glue {W : Type u_1} {M : Type u_2} {V : Type u_3} {X Y : Set V} [(v : V) → Decidable (v ∈ X)] (a : (possibilities W M V).obj (Opposite.op X)) (b : (possibilities W M V).obj (Opposite.op Y)) (hab : (CategoryTheory.ConcreteCategory.hom ((possibilities W M V).map (CategoryTheory.homOfLE ⋯).op)) a = (CategoryTheory.ConcreteCategory.hom ((possibilities W M V).map (CategoryTheory.homOfLE ⋯).op)) b) : ∃! c : (possibilities W M V).obj (Opposite.op (X ⊔ Y)), (CategoryTheory.ConcreteCategory.hom ((possibilities W M V).map (CategoryTheory.homOfLE ⋯).op)) c = a ∧ (CategoryTheory.ConcreteCategory.hom ((possibilities W M V).map (CategoryTheory.homOfLE ⋯).op)) c = b

Possibilities glue: a pair of possibilities over X and Y whose weakenings to X ⊓ Y agree is jointly the weakening of a unique possibility over X ⊔ Y — possibilities sends the lattice square to a pullback of types. The piecewise witness is Possibility.union in the charts of Possibility.domainEquiv.

theorem DynamicSemantics.possibilities_beck_chevalley {W : Type u_1} {M : Type u_2} {V : Type u_3} {X Y : Set V} [(v : V) → Decidable (v ∈ X)] (S : Set ((possibilities W M V).obj (Opposite.op X))) : ⇑(CategoryTheory.ConcreteCategory.hom ((possibilities W M V).map (CategoryTheory.homOfLE ⋯).op)) ⁻¹' ⇑(CategoryTheory.ConcreteCategory.hom ((possibilities W M V).map (CategoryTheory.homOfLE ⋯).op)) '' S = ⇑(CategoryTheory.ConcreteCategory.hom ((possibilities W M V).map (CategoryTheory.homOfLE ⋯).op)) '' ⇑(CategoryTheory.ConcreteCategory.hom ((possibilities W M V).map (CategoryTheory.homOfLE ⋯).op)) ⁻¹' S

Beck–Chevalley for the context-lattice square: existential image along X ⊓ Y ≤ X then weakening to Y is weakening to X ⊔ Y then existential image along Y ≤ X ⊔ Y — quantifying and reindexing commute. The image legs are State.presheaf's own action on the square's arrows.

The Grothendieck total

def DynamicSemantics.elementsToPoints {W : Type u_1} {M : Type u_2} {V : Type u_3} : CategoryTheory.Functor (possibilities W M V).Elements (Possibility W V (Part M))ᵒᵖ

Classify each element of the possibilities family as a point: on objects this is Possibility.domainEquiv; arrows become descents, by Possibility.le_iff_eq_restrict.

Equations

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

instance DynamicSemantics.instFaithfulElementsOppositeSetPossibilitiesPossibilityPartElementsToPoints {W : Type u_1} {M : Type u_2} {V : Type u_3} : elementsToPoints.Faithful

instance DynamicSemantics.instFullElementsOppositeSetPossibilitiesPossibilityPartElementsToPoints {W : Type u_1} {M : Type u_2} {V : Type u_3} : elementsToPoints.Full

instance DynamicSemantics.instEssSurjElementsOppositeSetPossibilitiesPossibilityPartElementsToPoints {W : Type u_1} {M : Type u_2} {V : Type u_3} : elementsToPoints.EssSurj

instance DynamicSemantics.instIsEquivalenceElementsOppositeSetPossibilitiesPossibilityPartElementsToPoints {W : Type u_1} {M : Type u_2} {V : Type u_3} : elementsToPoints.IsEquivalence

noncomputable def DynamicSemantics.elementsEquivPoints {W : Type u_1} {M : Type u_2} {V : Type u_3} : (possibilities W M V).Elements ≌ (Possibility W V (Part M))ᵒᵖ

The Grothendieck total of the possibilities family is the point type: the category of elements is equivalent to the opposite of the descent preorder on points — every point lies over its own domain.

Equations

• DynamicSemantics.elementsEquivPoints = DynamicSemantics.elementsToPoints.asEquivalence