Skip to main content
Bounty Ended with 250 reputation awarded by მამუკა ჯიბლაძე
added 3267 characters in body
Source Link
Anton Fetisov
  • 4.8k
  • 2
  • 29
  • 39

Given a type family $P: X \to Type$ we can construct its total space $Y := \sum_{x:X} P(x)$ with a canonical projection map $Y \xrightarrow{p} X$ defined by induction on $\Sigma$. Then we can consider the type family of homotopy fibers of $p$: $$x:X \vdash P^*(x) := \left( \sum_{y:Y} x = p(y) \right) : Type$$$$x:X \vdash \mathrm{fib}_p(x) := \left( \sum_{y:Y} x = p(y) \right) : Type$$

The resulting type family is equal to $P$ in the sense $\prod_{x:X} P(x) = P^*(x)$$\prod_{x:X} P(x) = \mathrm{fib}_p(x)$. By univalence we need to provide a homotopy equivalence between fibers. The map from left to right is the obvious inclusion of a strict fiber into a homotopy one. The map from right to left is constructed via induction on $\Sigma$ and paths. In the other direction, to any map $Y \xrightarrow{f} X$ we can associate its fiber type family $\mathrm{fib}_f$ and its total space $\sum_{x:X} \mathrm{fib}_f(x)$. It will be equivalent to $Y$ as objects over $X$. The relevant reference here is [4.8 The object classifier] in the HoTT book.

Essentially the big statement at work here is that from the PoV of higher category theory, the core groupoid for the overcategory $\mathbb{S}_{/X}$ is "representable" by a certain object $Type: \mathbb{S}$ (more formally, we consider a filtration of the overcategory by subcategories of bounded increasing cardinalities and require that each of these functors should be representable, thus getting an increasing sequence of objects $Type_{\kappa}$, see HTT 6[6.1.6 ". $\infty$-topoistopoi and classifying objects"objects]). In classical 1-topos theory and set theory this statement is limited to $(-1)$-truncated morphisms and type families and corresponds to the comprehension principle: any subset can be defined by a proposition which is true exactly for the elements of this subset, and vice versa. Type theory extends this principle to arbitrary constructions: any statement $P:X \to Type$ defines a type of "structures" on $X$ (the sumsigma type), and equivalently any map of types can be defined by some statement in a sense of a type family.

Regarding the moduli spaces: I don't think this construction has really anything to do with them. Not that it's entirely irrelevant, but moduli spaces carry much more structure than homotopy types and you can't get around that unless you're willing to sacrifice most information. One possibility is to consider moduli spaces as stacks of groupoids on the Zariski (or etale etcétale, flat, ...) site. Sheaves of groupoids naturally form a higher topos and should be a model of HoTT, however the information you get this way is mostly trivial: if your classified objects don't have any automorphisms, then the stack will be just a sheaf of sets, and if you have automorphisms, then you'll get the tautological description of locally isomorphic objects. Another possibility would be to enlarge your notion of equivalence, for example you could state that all fibers of the universal family are equivalent, e.g. by saying that an equivalence of $E$ and $E^\prime$ can be given as any fibration $X$ over $\mathbb{A}^1$ such that $X(0) \simeq E$ and $X(1) \simeq E^\prime$. This feels a lot like $\mathbb{A}^1$-homotopy theory, but I can't state anything more meaningful. In any case it feels like most (all?) of the algebraic information would be lost, even if one is very careful with definitions (I already see some problems in the one above).

Regarding your "associated bundle --- principal bundle" comment. Indeed, one can view this construction for connected spaces in a similar way. Assume given a point $x:X$ and $X$ connected, then fibrations $P:X \to Type$ over $X$ are roughly equivalent to homotopy representations of the ($A_\infty$-)group of loops $\Omega_x X$ in the automorphisms $Aut(P(x))$ of the fiber $P(x)$. This is certainly true in classical homotopy theory of spaces, but in HoTT there are complications. First there is a problem with the definition of homotopy groups$A_\infty$-groups and their representations, which we will ignore. The construction itself in one direction is obvious, we already know that each loop induces an automorphism of the fiber. In the other direction $y=x$ is a right torsor over $\Omega_x X$ so we can take the product over the loop group $y = x \times_{\Omega_x X} P(x)$$(y = x) \times_{\Omega_x X} P(x)$. Classically this gives us back $P$, but in HoTT this requires clarification.

We define a $(\infty, 1)$-category $C$ as a type of objects $Ob_C: Type$ and a family of morphism types $a,b:C \vdash C(a,b): Type$, together with units and composition which we can't provesuppress in the required equivalencefollowing discussion. One can prove thatAs usual, a groupoid is a category in which all morphisms are invertible, and for any category $C$ we have its core groupoid $C^\sim$ which is the largest subgroupoid in $C$. For any $X: Type$ its path groupoid $\Pi X: Cat$ has $Ob_{\Pi X} = X$ and $a, b:X \vdash \Pi X(a, b) := (a = b) : Type$. A category is called univalent if insteadthe natural functor $\Pi Ob_C \to C^\sim$ is an equivalence. Our definition of representationsa category follows the Segal space approach, and univalent categories are precisely complete Segal spaces. The category of types $Type$ has $Ob_{Type} = Type$ and $X,Y : Type \vdash Type(X, Y) := (X \to Y)$. The classical axiom of univalence is precisely the loop group we would considerstatement that $Type$ is an univalent category. We also define the representations ofgeometric realization functor $|C|$ as the fundamentalleft adjoint to the path groupoid functor, then there would indeed be an equivalencei.e. $Type(|C|, X) = Cat(C, \Pi X)$. For any ($A_\infty$-)group or monoid $G$ we define the delooping category $\mathbb B G$ as $Ob_{\mathbb B G} = 1$, $\mathbb B G(\ast, \ast) = G$. Presheaves of type familiestypes on $\mathbb B G$ are the same as representations of $G$. However

Now, the equivalencecorrespondence between type families and group representations stated above would implyin these terms says that for any connected $X: Type$ with $x: X$ the categories $\mathbb{B} \Omega_x X$$\mathbb B \Omega_x X$ and $\Pi X$ are Morita equivalent, whichi.e. their categories of type presheaves are equivalent. We have an obvious inclusion $\mathbb B \Omega_x X \to \Pi X$, however this is constructively impossible: suchnot an equivalence of categories, since an equivalence on object types would choose a path in $x = y$ for each $y:X$ (the equality between $1_{\Pi X}$ and $f \circ g$ forrestrict to the statement $f$ a natural inclusion from loops into paths),$\forall y: X, x = y$ which is only possible for contractiblemeans that $X$ is contractible. Note that for classical groupoids this statementThis is true essentially byin stark contrast with the axiom of1-categorical situation where any groupoid is equivalent to its full subgroupoid on one object. The classical statement relies on a choice: all sets principle to choose an equivalence for each nonempty $x=y$ are non-empty$C(x, y)$, sobut constructively we can't have such strong choice. One can choose an element in each oneargue that this failure is due to non-univalence of $\mathbb B \Omega_x X$ and then defineit's true in a sense, but I have two objections. The first is that the truth of this equivalence. For for univalent subcategories is itself a more explicit examplenontrivial theorem, consider some generic sheafessentially it is May's delooping theorem together with its version for path groupoids. Using such strong statements for a basic notion of spaces $X$ on some siteequivalence doesn't seem like a good idea. Let $x:X$The second is that the delooping category is an extremely natural object, and being unable to naturally talk about it would be a global element, then in general $\Omega_x X$ can "see" onlyproblem. I also find it troubling that the global structuresimple construction of $X$delooping category for a monoid would suddenly blow up into a much more complex path category if the monoid is a group. Similarly, but it canis natural to select subcategories on a set of objects, or consider action groupoids for groups, and none of them would be potentially arbitrarily complicated locallycategories under the univalence requirement (e.g. add skyscraper sheavesthe action groupoid on a torsor would have "too few" morphisms to be univalent and to be equivalent to its geometric realization, which is a point). This shows thatEven the expected equivalence $\mathbb B \Omega_x X \simeq \Pi X$ is impossiblebasic 1-categorical definition of a category wouldn't be a category if we require all categories to be univalent. Sure, at least naivelywe could do the Rezk completion, but that extra step would be unnecessary in half of situations and very nontrivial in the other half.

Non-univalent categories will break the homotopy hypothesis, but I wonder if one could stateview it as a lesser evil in some "locally true" mannerthis case. Groupoids should be at least as complicated as homotopy types, ebut there is no reason why they couldn't contain more information.g

That said, univalence of $Type$ is a very natural requirement. In particular, I don't know how to prove the Morita equivalence above without the univalence axiom, or even if you consider sheavesit's true. With univalence it is easy to prove that for any groupoid its category of spaces over some nontrivial homotopypresheaves is equivalent to the category of type, then families over its geometric realization:

$$\begin {eqnarray} C & \to & Type & \simeq\\ C & \to & Type^\sim & \simeq \\ C & \to & \Pi Type & \simeq \\ |C| & \to & Type & \simeq \\ \Pi |C| & \to & Type \end{eqnarray} $$

Together with the loop representationdelooping theorem --- fibrations$|\mathbb B \Omega_x X| = X$, $|\Pi X| = X$ this proves the Morita equivalence will not be true globallyabove. The part about path groupoids is easy to prove, but locally all such sheaves are just like spaces overI'm not sure that the point and admit this isomorphismpart about $\mathbb B$ can be proved without univalence.

I should review this text with a fresh headIn summary, and it's alreadyassuming univalence, type families over connected inhabited types can be uniquely reconstructed from their fiber over some point together with an action of the top longloop group on it. Tell me if anything needs further clarification or ifAt the moment there is no type-theoretic reference for the constructions that I missed some questionperformed above, but something like that should be in books on higher categories and topology.

Given a type family $P: X \to Type$ we can construct its total space $Y := \sum_{x:X} P(x)$ with a canonical projection map $Y \xrightarrow{p} X$ defined by induction on $\Sigma$. Then we can consider the type family of homotopy fibers of $p$: $$x:X \vdash P^*(x) := \left( \sum_{y:Y} x = p(y) \right) : Type$$

The resulting type family is equal to $P$ in the sense $\prod_{x:X} P(x) = P^*(x)$. By univalence we need to provide a homotopy equivalence between fibers. The map from left to right is the obvious inclusion of a strict fiber into a homotopy one. The map from right to left is constructed via induction on $\Sigma$ and paths. In the other direction, to any map $Y \xrightarrow{f} X$ we can associate its fiber type family $\mathrm{fib}_f$ and its total space $\sum_{x:X} \mathrm{fib}_f(x)$. It will be equivalent to $Y$ as objects over $X$. The relevant reference here is [4.8 The object classifier] in the HoTT book.

Essentially the big statement at work here is that from the PoV of higher category theory, the core groupoid for the overcategory $\mathbb{S}_{/X}$ is "representable" by a certain object $Type: \mathbb{S}$ (more formally, we consider a filtration of the overcategory by subcategories of bounded increasing cardinalities and require that each of these functors should be representable, thus getting an increasing sequence of objects $Type_{\kappa}$, see HTT 6.1.6 "$\infty$-topois and classifying objects"). In classical 1-topos theory and set theory this statement is limited to $(-1)$-truncated morphisms and type families and corresponds to the comprehension principle: any subset can be defined by a proposition which is true exactly for the elements of this subset, and vice versa. Type theory extends this principle to arbitrary constructions: any statement $P:X \to Type$ defines a type of "structures" on $X$ (the sum type), and equivalently any map of types can be defined by some statement in a sense of a type family.

Regarding the moduli spaces: I don't think this construction has really anything to do with them. Not that it's entirely irrelevant, but moduli spaces carry much more structure than homotopy types and you can't get around that unless you're willing to sacrifice most information. One possibility is to consider moduli spaces as stacks of groupoids on the Zariski (or etale etc) site. Sheaves of groupoids naturally form a higher topos and should be a model of HoTT, however the information you get this way is mostly trivial: if your classified objects don't have any automorphisms, then the stack will be just a sheaf of sets, and if you have automorphisms, then you'll get the tautological description of locally isomorphic objects. Another possibility would be to enlarge your notion of equivalence, for example you could state that all fibers of the universal family are equivalent, e.g. by saying that an equivalence of $E$ and $E^\prime$ can be given as any fibration $X$ over $\mathbb{A}^1$ such that $X(0) \simeq E$ and $X(1) \simeq E^\prime$. This feels a lot like $\mathbb{A}^1$-homotopy theory, but I can't state anything more meaningful. In any case it feels like most (all?) of the algebraic information would be lost, even if one is very careful with definitions (I already see some problems in the one above).

Regarding your "associated bundle --- principal bundle" comment. Indeed, one can view this construction for connected spaces in a similar way. Assume given a point $x:X$ and $X$ connected, then fibrations $P:X \to Type$ over $X$ are roughly equivalent to homotopy representations of the ($A_\infty$-)group of loops $\Omega_x X$ in the automorphisms of the fiber $P(x)$. This is certainly true in classical homotopy theory of spaces, but in HoTT there are complications. First there is a problem with the definition of homotopy groups and their representations, which we will ignore. The construction itself in one direction is obvious, we already know that each loop induces an automorphism of the fiber. In the other direction $y=x$ is a right torsor over $\Omega_x X$ so we can take the product over the loop group $y = x \times_{\Omega_x X} P(x)$. Classically this gives us back $P$, but in HoTT we can't prove the required equivalence. One can prove that if instead of representations of the loop group we would consider the representations of the fundamental groupoid, then there would indeed be an equivalence of type families. However the equivalence stated above would imply that the categories $\mathbb{B} \Omega_x X$ and $\Pi X$ are equivalent, which is constructively impossible: such an equivalence would choose a path in $x = y$ for each $y:X$ (the equality between $1_{\Pi X}$ and $f \circ g$ for $f$ a natural inclusion from loops into paths), which is only possible for contractible $X$. Note that for classical groupoids this statement is true essentially by the axiom of choice: all sets $x=y$ are non-empty, so we can choose an element in each one and then define the equivalence. For a more explicit example, consider some generic sheaf of spaces $X$ on some site. Let $x:X$ be a global element, then in general $\Omega_x X$ can "see" only the global structure of $X$, but it can be potentially arbitrarily complicated locally (e.g. add skyscraper sheaves). This shows that the expected equivalence $\mathbb B \Omega_x X \simeq \Pi X$ is impossible, at least naively. I wonder if one could state it in some "locally true" manner, e.g. if you consider sheaves of spaces over some nontrivial homotopy type, then the loop representation --- fibrations equivalence will not be true globally, but locally all such sheaves are just like spaces over the point and admit this isomorphism.

I should review this text with a fresh head, and it's already over the top long. Tell me if anything needs further clarification or if I missed some question.

Given a type family $P: X \to Type$ we can construct its total space $Y := \sum_{x:X} P(x)$ with a canonical projection map $Y \xrightarrow{p} X$ defined by induction on $\Sigma$. Then we can consider the type family of homotopy fibers of $p$: $$x:X \vdash \mathrm{fib}_p(x) := \left( \sum_{y:Y} x = p(y) \right) : Type$$

The resulting type family is equal to $P$ in the sense $\prod_{x:X} P(x) = \mathrm{fib}_p(x)$. By univalence we need to provide a homotopy equivalence between fibers. The map from left to right is the obvious inclusion of a strict fiber into a homotopy one. The map from right to left is constructed via induction on $\Sigma$ and paths. In the other direction, to any map $Y \xrightarrow{f} X$ we can associate its fiber type family $\mathrm{fib}_f$ and its total space $\sum_{x:X} \mathrm{fib}_f(x)$. It will be equivalent to $Y$ as objects over $X$. The relevant reference here is [4.8 The object classifier] in the HoTT book.

Essentially the big statement at work here is that from the PoV of higher category theory, the core groupoid for the overcategory $\mathbb{S}_{/X}$ is "representable" by a certain object $Type: \mathbb{S}$ (more formally, we consider a filtration of the overcategory by subcategories of bounded increasing cardinalities and require that each of these functors should be representable, thus getting an increasing sequence of objects $Type_{\kappa}$, see HTT [6.1.6. $\infty$-topoi and classifying objects]). In classical 1-topos theory and set theory this statement is limited to $(-1)$-truncated morphisms and type families and corresponds to the comprehension principle: any subset can be defined by a proposition which is true exactly for the elements of this subset, and vice versa. Type theory extends this principle to arbitrary constructions: any statement $P:X \to Type$ defines a type of "structures" on $X$ (the sigma type), and equivalently any map of types can be defined by some statement in a sense of a type family.

Regarding the moduli spaces: I don't think this construction has really anything to do with them. Not that it's entirely irrelevant, but moduli spaces carry much more structure than homotopy types and you can't get around that unless you're willing to sacrifice most information. One possibility is to consider moduli spaces as stacks of groupoids on the Zariski (étale, flat, ...) site. Sheaves of groupoids naturally form a higher topos and should be a model of HoTT, however the information you get this way is mostly trivial: if your classified objects don't have any automorphisms, then the stack will be just a sheaf of sets, and if you have automorphisms, then you'll get the tautological description of locally isomorphic objects. Another possibility would be to enlarge your notion of equivalence, for example you could state that all fibers of the universal family are equivalent, e.g. by saying that an equivalence of $E$ and $E^\prime$ can be given as any fibration $X$ over $\mathbb{A}^1$ such that $X(0) \simeq E$ and $X(1) \simeq E^\prime$. This feels a lot like $\mathbb{A}^1$-homotopy theory, but I can't state anything more meaningful. In any case it feels like most (all?) of the algebraic information would be lost, even if one is very careful with definitions (I already see some problems in the one above).

Regarding your "associated bundle --- principal bundle" comment. Indeed, one can view this construction for connected spaces in a similar way. Assume given a point $x:X$ and $X$ connected, then fibrations $P:X \to Type$ over $X$ are equivalent to homotopy representations of the ($A_\infty$-)group of loops $\Omega_x X$ in the automorphisms $Aut(P(x))$ of the fiber $P(x)$. This is certainly true in classical homotopy theory of spaces, but in HoTT there are complications. First there is a problem with the definition of $A_\infty$-groups and their representations, which we will ignore. The construction itself in one direction is obvious, we already know that each loop induces an automorphism of the fiber. In the other direction $y=x$ is a right torsor over $\Omega_x X$ so we can take the product over the loop group $(y = x) \times_{\Omega_x X} P(x)$. Classically this gives us back $P$, but in HoTT this requires clarification.

We define a $(\infty, 1)$-category $C$ as a type of objects $Ob_C: Type$ and a family of morphism types $a,b:C \vdash C(a,b): Type$, together with units and composition which we suppress in the following discussion. As usual, a groupoid is a category in which all morphisms are invertible, and for any category $C$ we have its core groupoid $C^\sim$ which is the largest subgroupoid in $C$. For any $X: Type$ its path groupoid $\Pi X: Cat$ has $Ob_{\Pi X} = X$ and $a, b:X \vdash \Pi X(a, b) := (a = b) : Type$. A category is called univalent if the natural functor $\Pi Ob_C \to C^\sim$ is an equivalence. Our definition of a category follows the Segal space approach, and univalent categories are precisely complete Segal spaces. The category of types $Type$ has $Ob_{Type} = Type$ and $X,Y : Type \vdash Type(X, Y) := (X \to Y)$. The classical axiom of univalence is precisely the statement that $Type$ is an univalent category. We also define the geometric realization functor $|C|$ as the left adjoint to the path groupoid functor, i.e. $Type(|C|, X) = Cat(C, \Pi X)$. For any ($A_\infty$-)group or monoid $G$ we define the delooping category $\mathbb B G$ as $Ob_{\mathbb B G} = 1$, $\mathbb B G(\ast, \ast) = G$. Presheaves of types on $\mathbb B G$ are the same as representations of $G$.

Now, the correspondence between type families and group representations stated above in these terms says that for any connected $X: Type$ with $x: X$ the categories $\mathbb B \Omega_x X$ and $\Pi X$ are Morita equivalent, i.e. their categories of type presheaves are equivalent. We have an obvious inclusion $\mathbb B \Omega_x X \to \Pi X$, however this is not an equivalence of categories, since an equivalence on object types would restrict to the statement $\forall y: X, x = y$ which means that $X$ is contractible. This is in stark contrast with the 1-categorical situation where any groupoid is equivalent to its full subgroupoid on one object. The classical statement relies on a choice principle to choose an equivalence for each nonempty $C(x, y)$, but constructively we can't have such strong choice. One can argue that this failure is due to non-univalence of $\mathbb B \Omega_x X$ and it's true in a sense, but I have two objections. The first is that the truth of this equivalence for univalent subcategories is itself a nontrivial theorem, essentially it is May's delooping theorem together with its version for path groupoids. Using such strong statements for a basic notion of equivalence doesn't seem like a good idea. The second is that the delooping category is an extremely natural object, and being unable to naturally talk about it would be a problem. I also find it troubling that the simple construction of delooping category for a monoid would suddenly blow up into a much more complex path category if the monoid is a group. Similarly, it is natural to select subcategories on a set of objects, or consider action groupoids for groups, and none of them would be categories under the univalence requirement (e.g. the action groupoid on a torsor would have "too few" morphisms to be univalent and to be equivalent to its geometric realization, which is a point). Even the basic 1-categorical definition of a category wouldn't be a category if we require all categories to be univalent. Sure, we could do the Rezk completion, but that extra step would be unnecessary in half of situations and very nontrivial in the other half.

Non-univalent categories will break the homotopy hypothesis, but I view it as a lesser evil in this case. Groupoids should be at least as complicated as homotopy types, but there is no reason why they couldn't contain more information.

That said, univalence of $Type$ is a very natural requirement. In particular, I don't know how to prove the Morita equivalence above without the univalence axiom, or even if it's true. With univalence it is easy to prove that for any groupoid its category of presheaves is equivalent to the category of type families over its geometric realization:

$$\begin {eqnarray} C & \to & Type & \simeq\\ C & \to & Type^\sim & \simeq \\ C & \to & \Pi Type & \simeq \\ |C| & \to & Type & \simeq \\ \Pi |C| & \to & Type \end{eqnarray} $$

Together with the delooping theorem $|\mathbb B \Omega_x X| = X$, $|\Pi X| = X$ this proves the Morita equivalence above. The part about path groupoids is easy to prove, but I'm not sure that the part about $\mathbb B$ can be proved without univalence.

In summary, assuming univalence, type families over connected inhabited types can be uniquely reconstructed from their fiber over some point together with an action of the loop group on it. At the moment there is no type-theoretic reference for the constructions that I performed above, but something like that should be in books on higher categories and topology.

Source Link
Anton Fetisov
  • 4.8k
  • 2
  • 29
  • 39

Yes, there is a certain sense in which your statements are true. As Mike Shulman and Qiaochu Yuan said, the strict fiber of a map cannot be defined in HoTT and doesn't make sense, but you can work from the other direction: instead of trying to associate a family of types to a map start with an arbitrary type family $P: X \to Type$. This includes any classical Serre fibrations: you associate to a point a fiber over it and to higher dimensional simplices some choice of their lifting, which is possible to do coherently by the path lifting property of fibrations. In the simplest case of a flat bundle you can make an explicit choice of lifts, which defines an equivalence between flat bundles and representations of the fundamental group of $X$. Homotopy-theoretically "every bundle is flat" in a sense that any two maps between fibers induced by a pair of equivalent paths are themselves (noncanonically) equivalent. The magic of HoTT and its models allows us to assume that all fibrations are given as representations of the path groupoid: path induction allows us to prove that any map of types is functorial in the sense that paths map to paths, composition to composition etc for all higher relations. This shows that a type family $P: X \to Type$ associates to any point $x: X$ a type $P(x): Type$, to any path $s: x=y$ a homotopy equivalence $ P(x) = P(y)$ etc (a map from paths in $Type$ to equivalences is automatic by path induction). In certain cases we can turn a coherent system of equivalences between fibers into a type family over $X$. The simplest case is when $X$ is defined as a higher inductive type, since higher inductive types are defined as representing objects of certain systems of equivalences between types. See chapter 6, in particular [6.12 The flattening lemma] in the HoTT book.

Given a type family $P: X \to Type$ we can construct its total space $Y := \sum_{x:X} P(x)$ with a canonical projection map $Y \xrightarrow{p} X$ defined by induction on $\Sigma$. Then we can consider the type family of homotopy fibers of $p$: $$x:X \vdash P^*(x) := \left( \sum_{y:Y} x = p(y) \right) : Type$$

The resulting type family is equal to $P$ in the sense $\prod_{x:X} P(x) = P^*(x)$. By univalence we need to provide a homotopy equivalence between fibers. The map from left to right is the obvious inclusion of a strict fiber into a homotopy one. The map from right to left is constructed via induction on $\Sigma$ and paths. In the other direction, to any map $Y \xrightarrow{f} X$ we can associate its fiber type family $\mathrm{fib}_f$ and its total space $\sum_{x:X} \mathrm{fib}_f(x)$. It will be equivalent to $Y$ as objects over $X$. The relevant reference here is [4.8 The object classifier] in the HoTT book.

Essentially the big statement at work here is that from the PoV of higher category theory, the core groupoid for the overcategory $\mathbb{S}_{/X}$ is "representable" by a certain object $Type: \mathbb{S}$ (more formally, we consider a filtration of the overcategory by subcategories of bounded increasing cardinalities and require that each of these functors should be representable, thus getting an increasing sequence of objects $Type_{\kappa}$, see HTT 6.1.6 "$\infty$-topois and classifying objects"). In classical 1-topos theory and set theory this statement is limited to $(-1)$-truncated morphisms and type families and corresponds to the comprehension principle: any subset can be defined by a proposition which is true exactly for the elements of this subset, and vice versa. Type theory extends this principle to arbitrary constructions: any statement $P:X \to Type$ defines a type of "structures" on $X$ (the sum type), and equivalently any map of types can be defined by some statement in a sense of a type family.

Regarding your "dual" construction: your type is defined as $\prod_{y^\prime} \prod_{y = y^\prime} X_{y^\prime}$. By path induction this type is equivalent to $X_y$, so your type family is equivalent to $X$.

Regarding the moduli spaces: I don't think this construction has really anything to do with them. Not that it's entirely irrelevant, but moduli spaces carry much more structure than homotopy types and you can't get around that unless you're willing to sacrifice most information. One possibility is to consider moduli spaces as stacks of groupoids on the Zariski (or etale etc) site. Sheaves of groupoids naturally form a higher topos and should be a model of HoTT, however the information you get this way is mostly trivial: if your classified objects don't have any automorphisms, then the stack will be just a sheaf of sets, and if you have automorphisms, then you'll get the tautological description of locally isomorphic objects. Another possibility would be to enlarge your notion of equivalence, for example you could state that all fibers of the universal family are equivalent, e.g. by saying that an equivalence of $E$ and $E^\prime$ can be given as any fibration $X$ over $\mathbb{A}^1$ such that $X(0) \simeq E$ and $X(1) \simeq E^\prime$. This feels a lot like $\mathbb{A}^1$-homotopy theory, but I can't state anything more meaningful. In any case it feels like most (all?) of the algebraic information would be lost, even if one is very careful with definitions (I already see some problems in the one above).

Abstractly, the story of the moduli spaces is the story about classifying ringed topoi, while HoTT speak only about objects of a single higher topos (or topoi that arise as their overcategories). Sort of orthogonal beasts.

Regarding your "associated bundle --- principal bundle" comment. Indeed, one can view this construction for connected spaces in a similar way. Assume given a point $x:X$ and $X$ connected, then fibrations $P:X \to Type$ over $X$ are roughly equivalent to homotopy representations of the ($A_\infty$-)group of loops $\Omega_x X$ in the automorphisms of the fiber $P(x)$. This is certainly true in classical homotopy theory of spaces, but in HoTT there are complications. First there is a problem with the definition of homotopy groups and their representations, which we will ignore. The construction itself in one direction is obvious, we already know that each loop induces an automorphism of the fiber. In the other direction $y=x$ is a right torsor over $\Omega_x X$ so we can take the product over the loop group $y = x \times_{\Omega_x X} P(x)$. Classically this gives us back $P$, but in HoTT we can't prove the required equivalence. One can prove that if instead of representations of the loop group we would consider the representations of the fundamental groupoid, then there would indeed be an equivalence of type families. However the equivalence stated above would imply that the categories $\mathbb{B} \Omega_x X$ and $\Pi X$ are equivalent, which is constructively impossible: such an equivalence would choose a path in $x = y$ for each $y:X$ (the equality between $1_{\Pi X}$ and $f \circ g$ for $f$ a natural inclusion from loops into paths), which is only possible for contractible $X$. Note that for classical groupoids this statement is true essentially by the axiom of choice: all sets $x=y$ are non-empty, so we can choose an element in each one and then define the equivalence. For a more explicit example, consider some generic sheaf of spaces $X$ on some site. Let $x:X$ be a global element, then in general $\Omega_x X$ can "see" only the global structure of $X$, but it can be potentially arbitrarily complicated locally (e.g. add skyscraper sheaves). This shows that the expected equivalence $\mathbb B \Omega_x X \simeq \Pi X$ is impossible, at least naively. I wonder if one could state it in some "locally true" manner, e.g. if you consider sheaves of spaces over some nontrivial homotopy type, then the loop representation --- fibrations equivalence will not be true globally, but locally all such sheaves are just like spaces over the point and admit this isomorphism.

I should review this text with a fresh head, and it's already over the top long. Tell me if anything needs further clarification or if I missed some question.