My experience with foundations is rather scant, but I've run into some types of objects that seem to resist the sort of set-theoretic encoding schemes via Kurowski tuples that are rather common for objects like groups and manifolds. In particular, they tend to be something like functions that can accept arbitrarily large inputs. I am wondering if such objects can be given foundations in a reasonably parsimonious way, so we don't have to include all possible inputs when considering such a function. The following are three examples:
Random variables: I read from Gowers's blog post that analysts define random variables as measurable functions satisfying some conditions, but that probabilists use them in a manner inconsistent with that definition. In particular, one has the problem of respecifying the sample space when new random variables come into play. If someone came up to me on the street and asked me to formalize this, I would probably respond by encoding a random variable using a proper class of all possible extensions of sample spaces. Naturally, this seems to be a rather weighty thing to carry around if I want to say that a particular probability manipulation is well-defined. From what I read in Tao's blog post, it seems that in practice, one encloses all mention of random variables in something like a type theory where the only allowable operations and quantities are those that are invariant under extension of sample space. Unfortunately, I know next to nothing about formal type theory - would this yield a decent answer?
Presheaves and sheaves on a site: Sometimes in algebraic geometry, one considers Grothendieck topologies like the fpqc topology, where even over a point, the isomorphism types of open sets and open covers form a proper class. One then encounters problems in the literature, where people claim that fpqc sheafification is a functor, but they prove it using a forbidden colimit over all open covers. This is an honest problem: in his paper Basically bounded functors and flat sheaves (Pac. J. Math. 57 no. 2 1975), Waterhouse produces a presheaf that has no fpqc sheafification. However, he also shows that for those presheaves that are left Kan extensions of presheaves on rings with a cardinality bound, sheafification and cohomology are independent of the bound for any topology (e.g., fpqc) satisfying a small approximation property. These left Kan extensions are commonly known as small presheaves, and essentially all geometrically interesting presheaves are small. In less technical and more general terms, we don't really need to make set-theoretic assumptions about the existence of universes, or truncate our presheaves to only take rings of size below some (possibly strongly inaccessible) bound, as long as we are only doing operations that preserve a sense of smallness. It would be nice, though perhaps not of fundamental importance, to have a formalism that made the recognition of such operations straightforward.
Supergeometry: While mathematicians often view supermanifolds as manifolds with sheaves of supercommutative rings, physicists doing first variation calculations for superfields often make use of an "odd parameter" that acts like an odd free variable that (as far as I can tell) completely fails to fit into the mathematicians' rings. In his book "Supermanifolds", DeWitt attempts to resolve this problem by adjoining countably infinitely many odd variables to everything in sight, but this seems to make physicists unhappy because infinitely many of those variables are unused and therefore "physically unmeaningful". Presumably, one should have a formalism that allows you to add odd parameters to your superalgebras at will, without carrying all possible extensions around with you all the time.
I hope these examples convey the flavor of what I'm seeking: some method for considering flexible or extendable objects that doesn't require the consideration of all possible extensions all the time.