Effective-Image Naturality

Abstract

Transport factorization is natural on the effective image.

Theorem 1.1 (Naturality on the effective image).

$$\forall X,Xprime,Y,Yprime,W,Wprime:\mathrm{Type},C:\mathrm{Concept}(X,Y),Cprime:\mathrm{Concept}(Xprime,Yprime),T:\mathrm{Concept}(X,W),Tprime:\mathrm{Concept}(Xprime,Wprime),f:\mathrm{Concept}(Y,W),fprime:\mathrm{Concept}(Yprime,Wprime),Xmap:\mathrm{Concept}(X,Xprime),Bmap:\mathrm{Concept}(Y,Yprime),Ymap:\mathrm{Concept}(W,Wprime),Tprime\circ Xmap=Ymap\circ T\wedge Cprime\circ Xmap=Bmap\circ C\wedge T=f\circ C\wedge Tprime=fprime\circ Cprime\Rightarrow \forall y:W,y\in \mathrm{range}(C)\Rightarrow Ymap(f(y))=fprime(Bmap(y)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Transport/EffectiveImageNaturality.effective_image_naturality (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source and target carriers are explicit concept readouts. The transport equation and the readout equation are both public, as are the two factorization equations for the current and transported maps.

For every value in the range of the first readout, transporting after applying its factor equals applying the transported factor after the readout transport. The proof evaluates the four public equations at a source point and uses equality congruence.

The canonical Concept carrier is imported from the existing family. Repository and pinned-library searches found no exact theorem packaging these two naturality clauses with the effective-image conclusion.

References

• Truth anchor: D5/S3/ConceptDynamics/Transport/EffectiveImageNaturality.effective_image_naturality
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition