((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.

  • 3
    $\begingroup$ This construction has no model-independent meaning: it is an example of fibrant replacement in model category theory. The dual construction is cofibrant replacement, which in spaces loosely replaces any map with a homotopy equivalent inclusion; explicitly it is given by the mapping cylinder. $\endgroup$ Nov 17, 2017 at 18:20
  • 2
    $\begingroup$ What does have model-independent meaning is taking the homotopy fiber; this generalizes to homotopy pullbacks in a model category or higher category. For example, for affine schemes this is the derived tensor product. $\endgroup$ Nov 17, 2017 at 18:22
  • $\begingroup$ @QiaochuYuan Thank you for this. Although I do not see any ground to disagree, still - is not there some model-independent version of the whole thing too? For example, the homotopy pullback of $X\to Y$ along the identity of $Y$? $\endgroup$ Nov 17, 2017 at 18:44
  • 4
    $\begingroup$ That gives, model-independently, the same map again. $\endgroup$ Nov 18, 2017 at 1:07
  • $\begingroup$ @QiaochuYuan Yes of course, sorry. Still I am puzzled - the above construction does resemble something well known and canonical, does not it? And in any case it should be canonical in, say, HoTT, no? $\endgroup$ Nov 18, 2017 at 7:09

3 Answers 3


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 \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 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 (é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).

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 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.

  • 1
    $\begingroup$ I don't think I agree with your penultimate paragraph. There is certainly the problem that in current HoTT we don't know how to define a coherent $A_\infty$-group or $A_\infty$-action. Maybe that's what you're referring to by "a problem with the definition of homotopy groups and their representations"? But beyond that I don't think there is any problem. I don't quite understand what you're doing, but it is true in HoTT that if $X$ is a connected type then $\mathbf{B} \Omega_x X \to X$ is an equivalence (for any possible meaning of that). $\endgroup$ Dec 9, 2017 at 23:41
  • 2
    $\begingroup$ This is why I don't like the terminology "univalent category"; it suggests that the things you have before you Rezk-complete are the objects of study of "category theory", and the univalent ones are a well-behaved subclass analogous to complete metric spaces etc. In my opinion, that's just false. The univalent categories are the proper objects of study of category theory in HoTT; the others are a weird thing that you get by leaving out one of the axioms, but which you have to pass through in order to define certain constructions, which is why the HoTT Book calls them "precategories". $\endgroup$ Dec 11, 2017 at 14:50
  • 2
    $\begingroup$ Describing the situation in your comment as if there were something true classically that's false in HoTT is like saying that "univalence proves the law of excluded middle is false". It's true that there is a naive way to translate the law of excluded middle which yields a false statement under univalence, but the practical upshot of that is that that's the wrong way to translate the law of excluded middle into HoTT; there's a better one which is consistent with univalence. $\endgroup$ Dec 11, 2017 at 14:51
  • 3
    $\begingroup$ Similarly, it's not that classically true statements about groupoids become false in HoTT; the fact that they would be false about precategories is part of what motivates us to conclude that category theory should be translated into HoTT solely in the world of (univalent) categories. $\endgroup$ Dec 11, 2017 at 14:52
  • 2
    $\begingroup$ Put differently, weird behavior of non-complete Segal spaces should not be regarded as any sort of commentary on what "$(\infty,1)$-category theory" looks like when done with complete Segal spaces, since it is the latter that are the model of $(\infty,1)$-category theory. $\endgroup$ Dec 11, 2017 at 16:53

I am answering your "later addon" only, although it seems actually to be a very different question than your original one.

This is perhaps one of the most misunderstood aspects of HoTT and particularly Univalence.

There is no squeezing of water.

Upon hearing that univalence "makes equivalent spaces equal to each other", it's natural to think that somehow this is losing information about the particular equivalence. But this is not so. The point is that rather than "squeezing" the notion of equivalence down to coincide with the classically "flat" notion of equality, instead univalence expands the notion of "equality", making it as rich as the classical notion of equivalence.

The difference between a trivial and a nontrivial fibration, and similarly between a connected space and a contractible space, is represented in HoTT by the difference between a "truncated" equality and an untruncated one. Suppose you try to write naively a statement in HoTT that (based on "equalities mean paths") you might think means "$Y$ is connected", like "for all $y_1,y_2:Y$ we have $y_1=y_2$". In formal type theoretic syntax this would be $\prod_{y_1,y_2:Y} (y_1=y_2)$. But it turns out that this statement actually means "$Y$ is contractible (or empty)", because everything in HoTT is "continuous/functorial/natural" unless you force it not to be. In particular, if "for all $y_1,y_2:Y$ we have $y_1=y_2$" in this sense, then the operation assigning the path from $y_1$ to $y_2$ must depend continuously on $y_1$ and $y_2$, which means that as soon as $Y$ has a point it can be continuously retracted back to that point.

If you want to say instead that $Y$ is connected, then you need some way to break this "continuity". For this purpose there is an operation called propositional truncation. If $A$ is a space, then its propositional truncation $\Vert A \Vert$ is a space that is empty if $A$ is empty, and contractible if $A$ is nonempty. In other words, it encodes the information of whether $A$ is nonempty without any information about what points there are in $A$ or how they are homotopically connected. Now the modified statement $\prod_{y_1,y_2:Y} \Vert y_1=y_2\Vert $ does mean only that $Y$ is connected (or empty), because it doesn't force the path from $y_1$ to $y_2$ to be specified as a continuous function of $Y$; instead only "the fact that there exists such a path" is specified as a continuous function of $Y$. Sometimes we pronounce $\Vert y_1=y_2\Vert$ as "$y_1$ is merely equal to $y_2$".

This distinction then carries over to any fibration over $Y$. If $Y$ is contractible, so that all of its points are equal, then all fibers are also equal, and the fibration is trivial. But if $Y$ is only connected, so that all of its points are merely equal, then all fibres are merely equal. In the latter case, we cannot "uniformly pick simultaneous equalities" as you said.


Here is an answer to your original question in the context of HoTT. An arbitrary map $f:X\to Y$ that isn't a fibration can't be viewed literally as a family of spaces varying continuously over $Y$, because the strict fibers don't vary continuously over $Y$; a path from $y_1$ to $y_2$ doesn't induce any sort of map from the fiber over $y_1$ to the fiber over $y_2$. In (ordinary) HoTT, however, we can't talk about such strict fibers at all; the naive definition of "fiber" $\mathrm{fib}_f(y) = \sum_{x:X} (f(x)=y)$ actually produces the homotopy fiber, and this is exactly the fibrant replacement construction you describe. It is a family varying over $Y$ (i.e. a type dependent on $Y$), and its total space $\sum_{y:Y} \mathrm{fib}_f(y)$ is indeed equivalent to $X$.

Fibers are defined in the HoTT Book in Definition 4.2.4, and the fact that the total space of the fibers is the original domain is Lemma 4.8.2.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.