One of the most basic constructions in homotopy theory assigns to a map $ f:X\to Y$ another map $ \pi_f:P_f\to Y$ such that $ P_f$ is equivalent to $ X$ and (under connectedness assumption for $ Y$ ) all $ \pi_f^{-1}(y)$ are equivalent to each other. $ P_f$ is the space of all pairs $ (x,\gamma)$ where $ x\in X$ and $ \gamma$ is a path in $ Y$ with $ \gamma(0)=x$ .

I would like to view this construction from a familial perspective. Namely, I want to view $ f$ as a family $ X_y:=f^{-1}(y)$ of spaces continuously varying over $ Y$ . Then, we are constructing another family $ \check X_y$ from it, with$ $ \check X_y=\bigcup_{y’}\operatorname{paths}(y,y’)\times X_{y’}. $ $ That spaces in this family are pairwise equivalent is ensured by the fact that any path between $ y_1$ and $ y_2$ produces equivalences between $ \operatorname{paths}(y_1,y’)$ and $ \operatorname{paths}(y_2,y’)$ for all $ y’$ .

From this point of view, the equivalence of total spaces is clear from $ $ \bigcup_{y,y’}\operatorname{paths}(y,y’)\times X_{y’}=\bigcup_{y’}\left(\bigcup_y\operatorname{paths}(y,y’)\right)\times X_{y’},$ $ as the spaces in parentheses are contractible.

Now this way of formulating it suggests that there must be many other situations where a similar construction is present.

The most likely area is of course Homotopy Type Theory. I am pretty sure that something like this is used very frequently there. Could I have a specific reference – how is it called there and what does it mean conceptually from the type-theoretic/logical point of view?

It also looks like some sort of generalization for the associated bundle <-> principal bundle business. Is a generalization along these lines known?

I am especially interested in the context of moduli spaces in algebraic geometry. Some moduli spaces (like projective spaces or, more generally, Grassmanians) manifestly consist of equivalent objects but some others do not. Is there a way to modify moduli spaces in a way similar to the above, to arrive at some equivalent moduli spaces consisting of equivalent objects?

I have vague feeling that this construction might be related to switching from coarse moduli spaces to fine moduli stacks, does this make sense and can it be made rigorous?

If this is not too much, one more question.

A dual construction suggests itself,$ $ \hat X_y=\prod_{y’}X_{y’}^{\operatorname{paths}(y,y’)}. $ $ It is as easy to show that all $ \hat X_y$ are equivalent to each other. However this time I think total space is not equivalent to the total space of the original family. Instead, the spaces of all global sections are equivalent.

Does this dual thing occur anywhere? This time I don’t even know whether it is used in homotopy theory itself.