((In conclusion)

It was hard to choose which answer to accept. I decided for the one which addressed most of the various aspects of the question.

)

(Later addon)

I now decided to put a bounty on this, and want to put particular accent on one aspect of the question that puzzles me most.

As discussed in greater length below, at the first sight from the point of view of Homotopy Type Theory (HoTT) the situation seems next to trivial: if we view $f:X\to Y$ as a family $X_y:=f^{-1}(y)$ of spaces continuously varying over $Y$ then, if $Y$ is connected, HoTT squeezes water out of it and leaves the plain fact "all $y$ are equal to each other". This then implies that all $X_y$ are equal to each other.

But on the other hand, the above argument completely ignores the fact that the fibration associated to $f$ might be nontrivial, i.e. one might be unable to uniformly pick simultaneous equalities $X_y=X_{y'}$ for all pairs $y$, $y'$. So, on top of having this next to trivial description of homotopy fibers, seemingly HoTT must also possess techniques to detect nontriviality of the fibration, etc. What are they?

End(Later addon)

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.

1more comment