Canonical Dependent Fiber Equivalence

Abstract

The canonical dependent-fiber equivalence records a readout and recovers its source.

Theorem 1.1 (Canonical dependent-fiber equivalence).

$$\forall X,B:\mathrm{Type},q:X\to B,\mathrm{let}R(b):=\mathrm{ConceptFiber}\left(q,b\right),e_q:=\mathrm{canonical}(q):X\equiv \sum _{b:B}R(b),(\forall x:X,e_q(x)=⟨q(x),⟨x,refl⟩⟩)\wedge (\forall b:B,x:X,p:q(x)=b,e_q^{-1}(⟨b,⟨x,p⟩⟩)=x).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/CanonicalDependentFiberEquivalence.whole_dependent_fiber_form (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any readout q : X -> B, the named equivalence e_q sends x to its coordinate q(x), the same object x, and the reflexive proof that x lies in that fiber.

The inverse computation is public as well: it recovers x by forgetting the coordinate and equality witness.

No quotient, surjectivity, section, linear structure, or metric is assumed. The construction uses the pinned natural fiber equivalence directly, and its axiom audit has no choice dependency.

References

• Truth anchor: D5/S3/ConceptDynamics/Fibers/CanonicalDependentFiberEquivalence.whole_dependent_fiber_form
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition