Heyting Valued Set Theory and Fibre Bundles

Abstract

Takeuti and Titani [15] have demonstrated that, given a manifold $B$ with topology $\Omega =\mathcal{O}(B)$, the internal notion of an apartness vector space in $V^{(\Omega )}$ and the external notion of a vector bundle over $B$ are no more than two representations of the same entity. The principal objective of this paper is, first of all, to internalize fibre bundles on the lines of Takeuti and Titani [15], and then to establish various internal-external interconnections around this. For example, we show that the external notion of integration over the fibre corresponds to the usual integration on internalized manifolds within $V^{(\Omega )}$. The paper attains its climax as we discuss the internal and external aspects of an internalized version of celebrated Stokes theorem.