sec-temporal-trust-contracts
13.6 Temporal behavior types as trust contracts
The information category says which decisions can depend on which evidence, but a safety theory also needs a language for what a system may do over an interval. Schultz and Spivak’s temporal type theory supplies such a language [ Schultz and Spivak , 2017 ] . A behavior type is modeled as a sheaf: to each time window \(U\) it assigns a set \(B(U)\) of possible behaviors, and an inclusion \(V\hookrightarrow U\) induces a restriction
Their semantics lives in a topos of sheaves on a translation-invariant quotient of the interval domain. This setting supports discrete, continuous, and hybrid behavior, as well as an internal temporal logic in which familiar linear and metric temporal logics can be represented.
For agentic UODL, a behavioral safety contract is a monomorphism
in the behavior topos. A realized trajectory \(b\in B(U)\) is verified over \(U\) when it has a lift \(\widetilde b\in S(U)\) with \(j_U(\widetilde b)=b\). Thus trust is not identified with a scalar confidence score. It is witnessed inhabitation of a declared temporal subtype.
Let \(j:S\hookrightarrow B\) be a behavioral contract in a sheaf topos, let \(\{ U_i\to U\} \) be a covering family, and let \(b\in B(U)\). If every restriction \(b|_{U_i}\) lifts to a section \(s_i\in S(U_i)\), then \(b\) lifts uniquely to a section \(s\in S(U)\).
Because each \(j_{U_i}(s_i)\) is the restriction of the same section \(b\), the local witnesses agree after restriction to every overlap: monicity of \(j\) reflects their equality there. The sheaf condition for \(S\) therefore glues them to a unique \(s\in S(U)\). The sections \(j_U(s)\) and \(b\) have equal restrictions on the cover, so separatedness of \(B\) gives \(j_U(s)=b\). Uniqueness follows again from monicity.
This proposition turns compositional trust into descent. Verification on local windows yields a global certificate only when the local certificates agree on overlaps and the contract is genuinely sheaf-like for the chosen temporal coverage. A collection of independent monitor outputs without overlap compatibility is not such a certificate. Nor does the proposition guarantee that the monitors see every relevant execution: that remains the faithfulness and coverage obligation of Proposition 13.5.
The connection to online UDL is immediate. At time \(t\), the observed execution is a restricted section \(b|_{U_t}\). Persistence requires the verification witnesses to restrict coherently as \(U_t\) grows. The information category controls which agents may construct or inspect those sections; the temporal behavior topos controls which histories satisfy the contract; and the audit observer exposes evidence that a verifier can check. When an unexpected channel changes the information shape, the contract must be reindexed to the realized shape and subjected to the Kan-transport test of Theorem 13.3.
There is also a useful warning in the Schultz–Spivak construction. Some properties that look local on short ordinary intervals are not preserved by naive concatenation. Their interval-domain semantics was designed in part to represent such non-composable behaviors correctly. Agentic safety contracts therefore require a declared temporal coverage and gluing law; “safe on every short run we tested” is not automatically a theorem about a long-lived team.
An emerging industrial direction.
The translation of these ideas into agent engineering is beginning to appear outside the academic literature. A 2026 Daice Labs research synthesis presents category theory as a language for composable and trustworthy AI and emphasizes polynomial-functor interfaces that type what an agent can observe and which actions it can produce [ Daice Labs , 2026 ] . On that view, containment should be expressed as an interface constraint and compatibility should be checked before agents are composed.
This direction is closely aligned with UODL but does not subsume it. Typed interfaces constrain the boundary of an individual component; UODL must also track how the realized information category changes online, whether temporal contracts survive that change, and whether the audit observer faithfully sees the resulting execution. Conversely, polynomial functors offer a promising concrete presentation of the abstract capability categories used in this chapter. We cite the Daice essay as evidence of an emerging industrial research direction, not as a formal safety guarantee or a report of a certified deployed system.