Effective-Image Naturality and Surjective Lift

Abstract

Transport factorization is natural on the effective image and globally for a surjective readout.

Theorem 1.1 (Image-local naturality extends across a surjective readout).

$$\begin{array}{c}\forall XE,XEPrime,YE,YEPrime,WE,WEPrime:\mathrm{Type},\\ C:\mathrm{Concept}(XE,YE),CPrime:\mathrm{Concept}(XEPrime,YEPrime),\\ T:\mathrm{Concept}(XE,WE),TPrime:\mathrm{Concept}(XEPrime,WEPrime),\\ f:\mathrm{Concept}(YE,WE),fPrime:\mathrm{Concept}(YEPrime,WEPrime),\\ Xmap:\mathrm{Concept}(XE,XEPrime),Bmap:\mathrm{Concept}(YE,YEPrime),Ymap:\mathrm{Concept}(WE,WEPrime),\\ 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:YE,y\in \mathrm{range}(C)\Rightarrow Ymap(f(y))=fPrime(Bmap(y)))\wedge \\ (\mathrm{Surjective}(C)\Rightarrow (\forall y:YE,Ymap(f(y))=fPrime(Bmap(y)))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Transportability/EffectiveImageNaturalitySurjectiveLift.effective_image_naturality_and_surjective_lift (✓ std3). ∎

Source. Repository-derived.

Commentary.

The transport square, readout square, and both target factorizations are public premises on their exact carriers.

The first conclusion states naturality on the range of the current readout. The second independently assumes that readout is surjective and states the equation on its full codomain.

The image-local clause is imported from the frozen family theorem; surjectivity supplies a source representative for the global clause.

References

• Truth anchor: D5/S3/ConceptDynamics/Transportability/EffectiveImageNaturalitySurjectiveLift.effective_image_naturality_and_surjective_lift
• Dependency: D5/S3/ConceptDynamics/Transport/EffectiveImageNaturality