If $\pi : F \to N$ is a fiber bundle, and $\phi : M \to N$ (here, $M$ and $N$ are manifolds), then the standard way to define the pullback bundle of $F$ by $\phi$ is $$\phi^* F := \{(m,f) \in M \times F \mid \phi(m) = \pi(f)\},$$ written as a submanifold of $M \times F$.
If additionally, $\psi : L \to M$ (where $L$ is also a manifold), then $\psi^* \phi^* F$ is a submanifold of $L \times \phi^* F$ which is a submanifold of $L \times M \times F$, and $\psi^* \phi^* F$ is naturally isomorphic to $(\phi \circ \psi)^* F$, which is a submanifold of $L \times F$. One can show that the notion of pullback is a contravariant functor (with a minor caveat).
In being super-careful about the types of domain/codomain in various bundle computations in some of my research, I'm finding that, while it is a natural way to construct a pullback bundle, this "tacking on" of the new basespace and identifying pullback bundles using the above isomorphism tends to get in the way of really rigorously typed computations (i.e. ensuring that domain/codomain are always exactly matched, and making no implicit identifications of spaces).
QUESTION: Is there an alternate construction for pullback bundles which doesn't require the identification of spaces (in the manner described above) in order for pullback to be a contravariant functor?