Transport Discipline: Univalence as a systems principle

A16Prose proofThe discipline of transporting proofs across equivalent representations.

The discovery that the rising sun is not new every morning, but always the same, was one of the most fertile astronomical discoveries.
— Gottlob Frege, 'On Sense and Reference' (1892)

This chapter formalizes substitution discipline as transport along witnessed equivalences, defining Anchor A16 (Transport Discipline): replacing A with B in a context requires not only a witnessed equivalence but a transport certificate for each property in the context's footprint, subject to identity, composition, and coherence laws. The univalence axiom from homotopy type theory is presented as the theoretical ideal, with the certificate regime serving as its engineering surrogate. T2 (Reference) and T7 (Contextual Equivalence) are resolved as scope-bounded transport problems. A16 completes Part III by threading through the context structure (A12), sheaf condition (A13), fibrations (A14), and logic selection (A15); the formal development here corresponds to the narrative treatment of evidentiary substitution in Vol I, Chapter 6 ("Evidence without Custody").

The Substitution Problem

A data pipeline migrates product IDs from the old SKU format to UUIDs. The mapping is bijective at the level of product identity: every product has exactly one old ID and one new ID. The equivalence is mathematically clean. The migration runs. Downstream, a pricing rule breaks.

The pricing rule checked whether the SKU started with "CL-" to identify clearance items. Under UUIDs, that check is meaningless. The rule was written against the representation of the ID, not the product identity. The equivalence preserved products but not the predicate.

This is not a bug in the migration. The migration did exactly what it was told: map old IDs to new IDs. The failure occurred because substitution was treated as a syntactic operation when it required semantic validation. The equivalence said "these are the same product." It did not say "you can replace one with the other in this context and preserve meaning."

The same pattern appears in other domains:

User account merge: Two accounts are merged based on email match. The equivalence is valid. But notification preferences were stored per-account; merging lost the user's settings because no one asked whether preferences transport along the equivalence.

Schema migration: A column is renamed from user_id to account_id. The data is identical. But a foreign key constraint referenced the old column name. The constraint broke because it was defined syntactically, not relationally.

Address normalization: Two address formats are equivalent (US vs international). Validation rules were defined on the US format. After conversion, the validation fails because the rules assumed the old field structure.

The common failure mode is substitution without transport. The equivalence exists—the properties do not follow.

Transport as the Key Operation

Transport is the operation that carries properties along an equivalence(Program 2013, ch. 2).

Given a property P defined on objects of type A, and an equivalence e : A ≃ B, transport produces a corresponding property on objects of type B. If P_A assigns values to elements of A, transport produces P_B that assigns "corresponding" values to elements of B.

What "corresponding" means depends on the witness class:

Witness Class	Correspondence
Equality (=)	P_B(map_e(a)) = P_A(a)
Isomorphism (≅)	P_B(map_e(a)) ≅ P_A(a)
Equivalence (≃)	P_B(map_e(a)) ≃ P_A(a) (up to coherence)
Approximation (≲)	P_B(map_e(a)) ≲ P_A(a) (monotone/lossy)

The key insight: transport is not free. Not every property can be moved along every equivalence. The "clearance" predicate could not transport along the SKU→UUID equivalence because it was defined in terms of the SKU representation, not the product identity.

Transport requires a certificate: an artifact that attests the property can be moved along this equivalence, within this scope, up to this witness class.

A16: Transport Discipline

A16

Transport Discipline (A16)

Require:

Witnessed equivalence e : A ≃ B with witness class K(e)
For each property class P with evaluators P_A : A → V and P_B : B → V, a transport certificate asserting:

P_B(\text{map}_e(a)) \approx_{K(e)} P_A(a)

Substitution discipline:

Replacing A with B in context C[A] is valid iff:

Witness e exists with valid(ctx, e) = Valid
Transport certificate exists for each P ∈ Footprint(C)
K(e) permits the operations in C[_] (non-escalation)
If any P involves negation or absence-sensitive claims, Adapter(L,P) certificate required

Transport laws:

Identity: Transport along id_A is identity on property values
Composition: Transport along e₂ ∘ e₁ equals transport along e₂ then e₁
Coherence: Round-trip transport preserves meaning up to K(e)

Theorem: Scoped Transport Safety

The following theorem establishes that transport along witnessed equivalences preserves truth within scope and fails explicitly outside it.

Theorem(Scoped Transport Safety)

Let $e : A \simeq_S B$ be a witnessed equivalence with scope $S$ . Let $P : \mathbf{Entity} \to \mathbf{Prop}$ be a transportable property. Let $U \in S$ be a context in the equivalence's scope.

If $P(A)$ holds in context $U$ , and transport is well-defined for $P$ along $e$ , then $\mathrm{transport}_e(P)(B)$ holds in context $U$ .

Conversely, if $U \notin S$ (context outside scope), transport is undefined and the operation fails with a ScopeViolation.

Proof

Within scope: By definition of witnessed equivalence, $e$ provides a certificate that $A$ and $B$ are interchangeable for all transportable properties in contexts within $S$ . The transport map $\mathrm{transport}_e : P(A) \to P(B)$ is part of the equivalence structure. If $P(A)$ holds (has a proof/witness), then $\mathrm{transport}_e$ carries that witness to a witness of $P(B)$ .
Preservation of truth: The transport is functorial: it preserves the structure of the proof. If $P(A)$ was witnessed by $\pi$ , then $P(B)$ is witnessed by $\mathrm{transport}_e(\pi)$ . The transport laws (identity, composition, coherence) ensure this preservation is well-behaved.
Outside scope: The equivalence certificate is only valid in $S$ . If $U \notin S$ , the system has no warrant that $A$ and $B$ are interchangeable in $U$ . The transport operation checks $U \in S$ as a precondition. Failure produces a ScopeViolation artifact naming the witness, the context, and the scope boundary.

Failure mode: Attempting to use an equivalence outside its scope is a type error. The equivalence $\texttt{NYC} \simeq_{\text{postal}} \texttt{New York City}$ does not justify substitution in a real estate context, even if both terms denote entities. Every successful transport produces a TransportReceipt binding the original claim, the transported claim, and the certificate. The receipt is auditable.

∎

Operationally, $\approx_{K(e)}$ is: equality (for =), structure-preserving equality (for ≅), equivalence up to declared invariants (for ≃), and monotone upper/lower bounds (for ≲).

The definition introduces Footprint(C): the declared set of property classes that context C reads or writes. This makes "for each property accessed" auditable. A system must declare its property footprint (statically or via dynamic trace) before substitution can be validated.

Transport Certificates

A transport certificate is a first-class object:

TransportCertificate {
  witness: WitnessID,              // e : A ≃ B
  property_class: PropertyClass,    // e.g., "inventory_counts"
  direction: "forward" | "backward" | "both",
  attestation: P_B(map_e(a)) ≈_K(e) P_A(a),
  scope: Scope,                    // inherited from witness
  provenance: Provenance,          // derived | declared | proved
  valid_until: Time | null
}

Certificates are directional. A→B substitution requires a forward certificate; B→A requires a backward certificate. If both exist and compose to identity (up to K(e)), the equivalence is "round-trip safe" for that property. But round-trip safety is derived, not assumed.

How certificates are obtained:

Derivation: If e is an isomorphism and P is structure-preserving (depends only on the identity of objects, not their representation), transport is derivable.
Declaration: A system administrator declares "this property transports along this equivalence." The declaration is trusted but auditable.
Proof: A formal argument that transport preserves the property's semantics. This is the strongest form of certificate.

What happens without a certificate:

If substitution is attempted and no certificate exists for some P ∈ Footprint(C):

Block the substitution (safe, may block valid operations)
Allow with warning (dangerous, may corrupt downstream)
Create an obstruction witness recording the missing certificate

The third option is the honest one. The system records what went wrong rather than silently failing.

Worked Example: Product ID Migration

A catalog migrates from SKU format (e.g., "CL-12345") to UUIDs.

Equivalence:

e : OldID ≃ NewID
Witness class: isomorphism (bijective)
Scope: S_catalog

Properties to transport:

Property	Description	Certificate
P_inventory	Inventory counts	✓ Derivable (counts are ID-independent)
P_reviews	Customer reviews	✓ Derivable (reviews reference products)
P_pricing	Pricing rules	⚠ Partial (some rules are ID-independent; others depend on SKU structure)
P_clearance	"Is clearance item"	✗ Fails (predicate factors through SKU prefix "CL-")
P_constraints	FK constraints	✗ Fails (constraints reference old column)

Why P_clearance fails:

The mapping is bijective on products. But P_clearance is defined as "SKU starts with CL-". Under UUIDs, that predicate cannot be evaluated. The property factors through the representation of the ID, not the product identity.

To transport P_clearance, you would need to either:

Redefine the predicate in ID-independent terms (e.g., add a is_clearance boolean column)
Accept that the predicate does not transport (and remove or migrate it before the ID change)

Substitution outcomes:

Query: "What is the inventory for product X?"

Footprint: P_inventory
Certificate exists: ✓
Substitution allowed

Query: "Is product X a clearance item?"

Footprint: P_clearance
Certificate does not exist: ✗
Substitution blocked (or obstruction witness created)

The system does not silently return "false" for clearance status. It reports that the property cannot be evaluated under the new ID scheme.

The North Star: Univalence

The theoretical ideal is the univalence axiom from homotopy type theory(Program 2013, ch. 2.10)(Lumsdaine 2012):

(A \simeq B) \simeq (A = B)

This says: if two types are equivalent, they are equal. Equivalence and identity are themselves equivalent. You can substitute one for the other everywhere, and all properties transport automatically.

Why we don't assume full univalence:

Computational content: Full univalence requires that transport be computable for all properties(Huber 2014). Some properties (especially representation-dependent ones) may not have computable transport.
Runtime cost: Even when computable, transport may be expensive. The system needs to control which transports are allowed and when.
Scope constraints: Univalence is global inside a given type universe(Program 2013, ch. 1.3). Scope in systems corresponds to working in different indexed universes or fibers (per A14)(Jacobs 1999, ch. 5), where equivalences may or may not exist. Our engineering surrogate makes scope explicit.

Our engineering surrogate:

Instead of assuming all transports exist, we require explicit certificates. This is weaker than full univalence but stronger than having no substitution discipline. The certificates are the "tax" you pay for not having full univalence.

The north star matters because it tells us what perfect substitution would look like. Univalence names the ideal world in which "witnessed equivalence" automatically grants safe substitution; certificates are the price of living in the world where semantics leak through representations. Our transport discipline is a practical approximation that makes coherence tractable.

Connection to Part III Machinery

A16 completes Part III by threading through all prior chapters.

A12 (Contexts): Transport must respect context. You can only transport within the scope of the witness. A certificate valid in S_catalog is not valid in S_warehouse unless the scopes overlap.

A13 (Sheaves): Transport must be coherent. If you transport along composed equivalences e₂ ∘ e₁, the result must match transporting along e₁ then e₂. This is the composition law.

A14 (Fibrations): If a property P is fibered over context (its type varies with base), transport must commute with reindexing. You cannot transport first and reindex second if reindexing would change the property's meaning.

A15 (Logic): If the source and target views have different (L, P) pairs, transport must go through the logic adapter. A property involving negation cannot transport naively across a CWA/OWA boundary.

Transport is where all the machinery becomes operational. Without transport discipline, equivalence is descriptive. With it, equivalence becomes actionable—the receipt that lets you spend the equivalence.

Touchstones Resolved

T2 (Reference): "Morning Star" ≃ "Evening Star" is a witnessed equivalence with scope S_astronomy. To substitute in a query, you need:

The witness e
Transport certificates for properties in Footprint(query)
Scope validity: query must be within S_astronomy

If the query asks for mythological associations, the scope fails. Substitution is blocked. The system does not silently corrupt the answer.

T7 (Contextual Equivalence): "NYC" ≃ "New York City" is valid in S_geography. In S_finance, "NYC" may refer to a trading desk. The witness has scope S_geography.

Substitution in a geographic query: ✓ (scope valid) Substitution in a financial query: ✗ (scope invalid)

The system does not conflate the trading desk with the city.

Consequence

Equivalence licenses substitution, but substitution requires transport. Transport requires a certificate. The certificate is the receipt.

Substitution requires certification. "These are equivalent" is not enough to justify replacement. Equivalence without transport discipline is a promissory note with no backing.

Parts II and III have built a calculus: contexts where truth lives, coherence conditions for when local truth becomes global, dependent types that vary with view, logic selection that makes inference rules explicit, and transport certificates that make substitution auditable. The question is what this calculus can do. Can you invent new predicates, locally, under invariant constraints, and promote them to broader scopes without corrupting what was already there? If you can, you have something neither empire offers. If you cannot, the machinery is an intellectual achievement and an engineering dead end.