Substitution Requires a Witness

Equivalent types can be identified.

A16 asks what a proposed substitution preserves for the operation that will receive it. A witnessed identification must be accompanied by grounds for the properties that operation uses, including its actual evaluators and versions. Univalence supplies a precise type-theoretic account of transport. The implementation question is whether the proposed replacement performs the corresponding work.

The Substitution Problem

Consider a hypothetical pipeline migrating 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.

The identifier conversion can be correct while the application migration is defective. 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 match alone does not establish that the accounts, their owners or their preferences are interchangeable. 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: In another hypothetical, a column is renamed from user_id to account_id while an external checking query still uses the old name. A database may update its own constraint metadata; that does not repair an unchanged query held elsewhere.

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.

These failures require two examinations: whether the asserted equivalence is established, and whether the operation preserves the properties actually used.

Transport as the Key Operation

Transport is the operation that carries properties along an equivalence¹.

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 relation kind:

Relation Kind	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)

A bijection e does permit transport of every property P_A as P_B = P_A ∘ e⁻¹. The clearance rule could therefore be carried over by recovering the old SKU. What failed was the unchanged prefix test on the new UUID. A mathematical transport exists; the deployed evaluator did not implement it.

Transport requires a certificate: an artifact that attests the property can be moved along this equivalence, within this scope, under this relation kind.

A16: Transport Discipline

Theorem: Scoped Transport Safety

The following result concerns a supplied proof map in a declared logical interpretation. The interface’s treatment of scope is a separate contract.

The proposed interface returns ScopeViolation when the requested use is established to lie outside the certificate’s scope. An unfinished scope check instead returns Inconclusive, and neither outcome certifies the requested transport. Another certificate or independent investigation may supply grounds this one lacks. A successful transport receipt binds the original claim, resulting claim, scope and checked map; its existence does not verify those fields.

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:

1. Derivation: If e is an isomorphism and P is structure-preserving (depends only on the identity of objects, not their representation), transport is derivable.

2. Attestation: An authorized administrator attests that the property transports. The receipt preserves that dependence on testimony; it is not a mathematical proof of the map or of the attestation's truth.

3. Proof: A formal argument that the proposed maps preserve the stated property under their hypotheses. Empirical adequacy and an authority’s permission remain different claims.

What happens without a certificate:

If a required certificate is missing, the operation cannot report successful certification of that substitution. It blocks the uncertified substitution and records the missing property, scope and evidence. This is an incomplete check, not a demonstrated false property or an exact-gluing obstruction.

The recipient can supply the missing grounds or choose a use the available evidence supports. A separately authorized precaution may also be available under its own conditions. Recording the gap does not authorize the original substitution, and a warning does not complete its missing check.

Worked Example: Product ID Migration

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

Equivalence:

• e : OldID ≃ NewID
• Relation kind: 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"	✗ Unchanged UUID-prefix evaluator fails; inverse-based transport remains available
P_constraints	External constraint-checking query	✗ Stipulated query still names the removed column

Why P_clearance fails:

The mapping is bijective on products. The old evaluator tests the prefix of an old SKU. Applying that same string test to a UUID asks a different question.

To preserve the old result, the implementation can retain the inverse mapping and evaluate the old predicate after looking up the SKU. It can instead migrate the classification into an independently maintained field, provided that migration is checked. If it supplies neither, the operation must not report the missing clearance determination as false.

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, with the missing property evidence identified

The system does not silently return "false" for clearance status. It reports that this evaluator has not been supplied, while leaving the inverse-based repair available.

Transport in a Univalent Universe

In a univalent universe, an equivalence supplies a path between types. Transport along that path moves a value or proof in a type family to the corresponding fibre; Appendix D states the axiom and its setting². This identification is not literal equality of external record bytes, field names or unchanged application code.

The proposed replacement still needs an evaluator that performs the corresponding operation. Axiomatic univalence does not by itself provide every desired judgmental reduction; constructive models and cubical approaches address that computational content³. Even when an inverse or transported evaluator is computable, obtaining its result may be expensive. The recipient must establish which implementation it will run and what resources that operation requires.

There is also work in giving the formal objects their interpretation. Calling two database identifiers equivalent supplies neither a faithful type-theoretic model nor evidence that their properties serve the receiving purpose. A16 asks for the maps, scope and checked properties that accompany the proposed substitution. The clearance rule can be transported; the unchanged UUID-prefix test simply did not perform that transport. The contract locates the work needed to preserve the operation, without treating the engineering problem as a refutation of univalence.

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. Overlap permits consideration of a restricted use; it does not extend a catalog certificate to the whole warehouse context.

Composition and gluing: A16 requires the supplied transports to satisfy their declared identity and composition laws. A13 concerns exact gluing when its separate sheaf hypotheses apply; it does not by itself establish those transport laws.

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.

The transport record identifies which operation was checked, under which relation and scope. A recipient can use that result within those conditions; the record does not grant an otherwise absent authority to act.

What the Substitution Requires

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. Stipulate a separate internal record in which "NYC" labels 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

The identifier substitution can succeed while the pricing substitution remains unsupported. That difference belongs in the result the recipient sees. If a certificate is missing, it can seek further grounds or choose an operation the existing evidence covers; recording the gap has not proved the proposed price wrong.

Parts II and III have separated the correspondence, its properties, its scope and the rules for carrying a claim. Part IV asks how a new predicate can enter this account. A name that makes a useful distinction available also gives later users something to depend on. Its admission must specify what those users may preserve and what a subsequent change would oblige them to revisit.