← The Framework

Component 4: The Edit Monad

Composable state transitions as a monad on the topos.

So far we have a topos of data states (Component 3) and a semantic functor that fills it with data. But data changes : people create objects, update properties, add links. We need a way to talk about these transitions that is both precise and composable, and a monad does exactly this: it wraps an endofunctor (the space of possible edits), a unit (the "do nothing" edit), and a multiplication (flattening nested edit plans into a single plan). The resulting Kleisli category is where all operational workflows live.

1. Primitive Edit Operations

Definition 1.1 : Edit Algebra

An ontology edit is an endomorphism e : ΦΦ′ in Ont. Five primitive operations generate everything:

Every structural modification of the ontology decomposes into a finite sequence of these. Write Edit for the five primitives and Edit* for the free monoid: finite sequences under concatenation, with the empty sequence as identity.

Example 1.2

Rename a person and link them to a company: UpdateProperty(o, name, "Alice") · AddLink(o, worksFor, c). The monoid structure makes the sequencing unambiguous.

2. The Monad

Definition 2.1 : The Edit Monad 𝕋

𝕋 = (T, η, μ) on Ont, where:

Endofunctor T : OntOnt sends each presheaf Φ to the coproduct of all states reachable by a finite edit sequence:

T(Φ) = ∐eEdit* e(Φ)

An element of T(Φ) is a pair (e, Φ′) : an edit sequence together with the state it produces.

Unit ηΦ : ΦT(Φ) includes via the empty edit: η(x) = (ε, x).

Multiplication μΦ : T(T(Φ)) → T(Φ) flattens a plan-within-a-plan: μ((e₂, (e₁, Φ′))) = (e₁ · e₂, e₂(e₁(Φ))).

3. Verification of Monad Laws

Theorem 3.1 : Monad Laws

(T, η, μ) satisfies:

  1. Left unit: μT(η) = idT.
  2. Right unit: μηT = idT.
  3. Associativity: μμT = μT(μ).

All three are inherited from the free monoid Edit*: the empty sequence is identity for concatenation, and concatenation is associative. The monad laws hold for exactly the same reason that string concatenation is associative with empty string as identity.

4. The Kleisli Category

The monad gives rise to a new category whose morphisms are effectful : they produce edit plans rather than just mapping states : and this is where decisions live.

Definition 4.1 : Kleisli Category

Ont𝕋 has:

Composition: for f : Φ𝕋 Ψ and g : Ψ𝕋 Γ,

g𝕋 f = μT(g) ∘ f

Execute f, apply g to the resulting state, flatten. Identity is η: do nothing.

Remark 4.2

Think of Ont𝕋 as the decision category. Every operational workflow : a single property edit, a multi-step approval pipeline, an automated rule : is a morphism here. Workflow chaining is Kleisli composition. The monad laws guarantee it is associative.

5. Action Types Formalized

Definition 5.1 : Action Type

An action type on entity type O consists of:

The action executes only when σ(p, Φ) = true.

Proposition 5.2 : Composable Workflows

Given action types A₁ and A₂, their sequential composition A₂ ∘𝕋 A₁ is itself an action type:

(A₂ ∘𝕋 A₁)(p₁, p₂, Φ) = μ(A₂(p₂, A₁(p₁, Φ)))

Any finite sequence of actions composes into a single Kleisli morphism : a workflow. Associativity and unitality are the monad laws.

6. Eilenberg-Moore Algebras: Materializations

There is a different perspective here: instead of asking "what edits can I make?" (Kleisli), ask "how does a state absorb edits?" (Eilenberg-Moore). The answer is a 𝕋-algebra, and it formalizes what the platform calls a materialization.

Definition 6.1 : 𝕋-Algebra

A 𝕋-algebra is a pair (D, α) where DOnt and α : T(D) → D satisfies:

  1. Unit: αηD = idD : doing nothing changes nothing.
  2. Associativity: αμD = αT(α) : applying a batch of edits all at once gives the same result as applying them one by one.

The map α is the conflict resolution strategy: last-write-wins, user-edit-priority, merge with timestamps, etc. Different choices of α give different materialization behaviors on the same underlying data.

Proposition 6.2 : Free-Forgetful Adjunction

F𝕋U𝕋 : OntOnt𝕋. The free algebra (T(Φ), μΦ) remembers every edit sequence without collapsing anything : the "unresolved" materialization. A concrete materialization chooses a specific α to collapse the edit history into a state.

7. The Writeback Adjunction

The final piece closes the loop: we had Sem going from data to ontology, and now we need a way back.

Definition 7.1 : Writeback Functor

WB : OntData serializes the ontology back into datasets and source systems. It is the right adjoint to Sem: SemWB.

Proposition 7.2 : Unit and Counit

The unit η : Id → WBSem says: index into the ontology, then write back, and you recover the original data (plus any absorbed edits). The counit ε : SemWB → Id says: write back, then re-index, and you recover the ontology state. Together, they guarantee the feedback loop is coherent : no information is silently lost.

Remark 7.3

The full cycle: (1) Sem pours raw data into the ontology; (2) users make decisions as Kleisli morphisms in Ont𝕋; (3) materializations absorb edits via Eilenberg-Moore algebras; (4) WB serializes the result back to source. One adjunction governs the entire round-trip.


Summary

The edit monad 𝕋 formalizes state transitions on the ontology topos: primitives generate Edit*; the Kleisli category Ont𝕋 is the decision category; action types are parametrized Kleisli morphisms with submission criteria; Eilenberg-Moore algebras are materializations; and SemWB closes the loop.

Next: Component 5: The Grothendieck Topology, security as a topological structure on the schema.