ora-0180

16.1 Environment morphisms and knowledge packages

An environment must expose more than a task label. Write

\[ E=(\mathcal I_E,\mathcal A_E,\mathcal C_E,\mathcal Q_E, \Omega _E,\mathcal S_E) \]

for its information, action, and consequence categories, query doctrine, observer, and safety subobject. An environment morphism \(f:E\to E'\) contains functors between these components together with comparison cells for the decision declaration. It may forget information, refine actions, change the clock, or transport consequences; each variance must be stated.

Definition 16.1 Structural knowledge package

A structural knowledge package over \(E\) is a tuple

\[ K_E=(D_E,U_E,W_E,R_E,Q_E), \]

where \(D_E\) is a learned diagram or categorical presentation, \(U_E\) is a universal construction on it, \(W_E\) is its universal witness, \(R_E\) is a family of repair types and certificates, and \(Q_E\) is the observational quotient on which the package is claimed to be valid.

Definition 16.2 Admissible structural transport

For \(f:E\to E'\), an admissible transport \(\tau _f:K_E\rightsquigarrow K_{E'}\) consists of:

  1. a transport of the learned diagram and its settled subdiagram;

  2. an invertible Beck–Chevalley mate comparing the two orders of transport and extension;

  3. a coherent image of the universal witness and registered repair types;

  4. an observer comparison preserving the quotient \(Q_E\); and

  5. a safety comparison landing in \(\mathcal S_{E'}\).

For tangent knowledge, it additionally includes an invertible comparison \(T\tau _f\Rightarrow \tau _fT\) on the admitted tangent structure.

Structural transport compares learning before transfer with transfer before reuse. Commutation up to the declared coherent equivalence is the central transport certificate.
Figure 16.1 Structural transport compares learning before transfer with transfer before reuse. Commutation up to the declared coherent equivalence is the central transport certificate.