Heyting valued set theory and fibre bundles (Q1108267)

\textit{G. Takeuti} and \textit{S. Titani} [Ann. Pure Appl. Logic 31, 307-339 (1986; Zbl 0615.03048)] 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 their paper, and then to establish various internal-external interconnections. For example, we show that the external notion of integration over a 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.