## January 19, 2015

### The Univalent Perspective on Classifying Spaces

#### Posted by Mike Shulman

I feel like I should apologize for not being more active at the Cafe recently. I’ve been busy, of course, and also most of my recent blog posts have been going to the HoTT blog, since I felt most of them were of interest only to the HoTT crowd (by which I mean, “people interested enough in HoTT to follow the HoTT blog” — which may of course include many Cafe readers as well). But today’s post, while also inspired by HoTT, is less technical and (I hope) of interest even to “classical” higher category theorists.

In general, a classifying space for bundles of $X$’s is a space $B$ such that maps $Y\to B$ are equivalent to bundles of $X$’s over $Y$. In classical algebraic topology, such spaces are generally constructed as the geometric realization of the nerve of a category of $X$’s, and as such they may be hard to visualize geometrically. However, it’s generally useful to think of $B$ as a space whose points are $X$’s, so that the classifying map $Y\to B$ of a bundle of $X$’s assigns to each $y\in Y$ the corresponding fiber (which is an $X$). For instance, the classifying space $B O$ of vector bundles can be thought of as a space whose points are vector spaces, where the classifying map of vector bundle assigns to each point the fiber over that point (which is a vector space).

In classical algebraic topology, this point of view can’t be taken quite literally, although we can make some use of it by identifying a classifying space with its representable functor. For instance, if we want to define a map $f:B O\to B O$, we’d like to say “a point $v\in B O$ is a vector space, so let’s do blah to it and get another vector space $f(v)\in B O$. We can’t do that, but we can do the next best thing: if blah is something that can be done fiberwise to a vector bundle in a natural way, then since $Hom(Y,B O)$ is naturally equivalent to the collection of vector bundles over $Y$, our blah defines a natural transformation $Hom(-,B O) \to Hom(-,B O)$, and hence a map $f:B O \to B O$ by the Yoneda lemma.

However, in higher category theory and homotopy type theory, we can really take this perspective literally. That is, if by “space” we choose to mean “$\infty$-groupoid” rather than “topological space up to homotopy”, then we can really define the classifying space to be the $\infty$-groupoid of $X$’s, whose points (objects) are $X$’s, whose morphisms are equivalences between $X$’s, and so on. Now, in defining a map such as our $f$, we can actually just give a map from $X$’s to $X$’s, as long as we check that it’s functorial on equivalences — and if we’re working in HoTT, we don’t even have to do the second part, since everything we can write down in HoTT is automatically functorial/natural.

This gives a different perspective on some classifying-space constructions that can be more illuminating than a classical one. Below the fold I’ll discuss some examples that have come to my attention recently.

All of these examples have to do with the classifying space of “types equivalent to $X$” for some fixed $X$. Such a classifying space, often denoted $B Aut(X)$, has the property that maps $Y \to B Aut(X)$ are equivalent to maps (perhaps “fibrations” or “bundles”) $Z\to Y$ all of whose fibers are equivalent (a homotopy type theorist might say “merely equivalent”) to $X$. The notation $B Aut(X)$ accords with the classical notation $B G$ for the delooping of a (perhaps $\infty$-) group: in fact this is a delooping of the group of automorphisms of $X$.

Categorically (and homotopy-type-theoretically), we simply define $B Aut(X)$ to be the full sub-$\infty$-groupoid of $\infty Gpd$ (the $\infty$-groupoid of $\infty$-groupoids) whose objects are those equivalent to $X$. You might have thought I was going to say the full sub-$\infty$-groupoid on the single object $X$, and that would indeed give us an equivalent result, but the examples I’m about to discuss really do rely on having all the other equivalent objects in there. In particular, note that an arbitrary object of $B Aut(X)$ is an $\infty$-groupoid that admits some equivalence to $X$, but no such equivalence has been specified.

### Example 1: $B Aut(2)$

As the first example, let $X = 2 = \{0,1\}$, the standard discrete space with two points. Then $Aut(2) = C_2$, the cyclic group on 2 elements, and so $B Aut(2) = B C_2 = K(C_2,1)$. Since $C_2$ is an abelian group, $B C_2$ again has a (2-)group structure, i.e. we should have a multiplication operation $B C_2 \times B C_2 \to B C_2$, an identity, inversion, etc.

Using the equivalence $B C_2 \simeq B Aut(2)$, we can describe all of these operations directly. A point $Z \in B Aut(2)$ is a space that’s equivalent to $2$, but without a specified equivalence. Thus, $Z$ is a set with two elements, but we haven’t chosen either of those elements to call “$0$” or “$1$”. As long as we perform constructions on $Z$ without making such an unnatural choice, we’ll get maps that act on $B Aut(2)$ and hence $B C_2$ as well.

The identity element of $B Aut(2)$ it’s fairly obvious: there’s only one canonical element of $B Aut(2)$, namely $2$ itself. The multiplication is not as obvious, and there may be more than one way to do it, but after messing around with it a bit you may come to the same conclusion I did: the product of $Z,W\in B Aut(2)$ should be $Iso(Z,W)$, the set of isomorphisms between $Z$ and $W$. Note that when $Z$ and $W$ are 2-element sets, so is $Iso(Z,W)$, but in general there’s no way to distinguish either of those isomorphisms from the other one, nor is $Iso(Z,W)$ naturally isomorphic to $Z$ or $W$. It is, however, obviously commutative: $Iso(Z,W) \cong Iso(W,Z)$.

Moreover, if $Z=2$ is the identity element, then $Iso(2,W)$ is naturally isomorphic to $W$: we can define $Iso(2,W) \to W$ by evaluating at $0\in 2$. Similarly, $Iso(Z,2)\cong Z$, so our “identity element” has the desired property.

Furthermore, if $Z=W$, then $Iso(Z,Z)$ does have a distinguished element, namely the identity. Thus, it naturally equivalent to $2$ by sending the identity to $0\in 2$. So every element of $B Aut(2)$ is its own inverse. The trickiest part is proving that this operation is associative. I’ll leave that to the reader (or you can try to decipher my Coq code).

(We did have to make some choices about whether to use $0\in 2$ or $1\in 2$. I expect that as long as we make those choices consistently, making them differently will result in equivalent 2-groups.)

### Example 2: An incoherent idempotent

In 1-category theory, an idempotent is a map $f:A\to A$ such that $f \circ f = f$. In higher category theory, the equality $f \circ f = f$ must be weakened to an isomorphism or equivalence, and then treated as extra data on which we ought to ask for additional axioms, such as that the two induced equivalences $f \circ f \circ f \simeq f$ coincide (up to an equivalence, of course, which then satisfies its own higher laws, etc.).

A natural question is if we have only an equivalence $f \circ f \simeq f$, whether it can be “improved” to a “fully coherent” idempotent in this sense. Jacob Lurie gave the following counterexample in Warning 1.2.4.8 of Higher Algebra:

let $G$ denote the group of homeomorphisms of the unit interval $[0,1]$ which fix the endpoints (which we regard as a discrete group), and let $\lambda : G \to G$ denote the group homomorphism given by the formula

$\lambda(g)(t) = \begin{cases} \frac{1}{2} g(2t) & \quad if\; 0\le t \le \frac{1}{2}\\ t & \quad if\; \frac{1}{2}\le t \le 1. \end{cases}$

Choose an element $h\in G$ such that $h(t)=2t$ for $0\le t\le \frac{1}{4}$. Then $\lambda(g)\circ h = h\circ \lambda(\lambda(g))$ for each $g\in G$, so that the group homomorphisms $\lambda,\lambda^2 : G\to G$ are conjugate to one another. It follows that the induced map of classifying spaces $e:B G \to B G$ is homotopic to $e^2$, and therefore idempotent in the homotopy category of spaces. However… $e$ cannot be lifted to a [coherent] idempotent in the $\infty$-category of spaces.

Let’s describe this map $e$ in the more direct way I suggested above. Actually, let’s do something easier and just as good: let’s replace $[0,1]$ by Cantor space $2^{\mathbb{N}}$. It’s reasonable to guess that this should work, since the essential property of $[0,1]$ being used in the above construction is that it can be decomposed into two pieces (namely $[0,\frac{1}{2}]$ and $[\frac{1}{2},1]$) which are both equivalent to itself, and $2^{\mathbb{N}}$ has this property as well:

$2^{\mathbb{N}} \cong 2^{\mathbb{N}+1} \cong 2^{\mathbb{N}} \times 2^1 \cong 2^{\mathbb{N}} + 2^{\mathbb{N}}.$

Moreover, $2^{\mathbb{N}}$ has the advantage that this decomposition is disjoint, i.e. a coproduct. Thus, we can also get rid of the assumption that our automorphisms preserve endpoints, which was just there in order to allow us to glue two different automorphisms on the two copies in the decomposition.

Therefore, our goal is now to construct an endomap of $B Aut(2^{\mathbb{N}})$ which is incoherently, but not coherently, idempotent. As discussed above, the elements of $B Aut(2^{\mathbb{N}})$ are spaces that are equivalent to $2^{\mathbb{N}}$, but without any such specified equivalence. Looking at the definition of Lurie’s $\lambda$, we can see that intuitively, what it does is shrink the interval to half of itself, acting functorially, and add a new copy of the interval at the end. Thus, it’s reasonable to define $e:B Aut(2^{\mathbb{N}}) \to B Aut(2^{\mathbb{N}})$ by

$e(Z) = Z + 2^{\mathbb{N}}.$

Here $Z$ is some space equivalent to $2^{\mathbb{N}}$, and in order for this map to be well-defined, we need to show is that if $Z$ is equivalent to $2^{\mathbb{N}}$, then so is $Z + 2^{\mathbb{N}}$. However, the decomposition $2^{\mathbb{N}} \cong 2^{\mathbb{N}} + 2^{\mathbb{N}}$ ensures this. Moreover, since our definition didn’t involve making any unnatural choices, it’s “obviously” (and in HoTT, automatically) functorial.

Now, is $e$ incoherently-idempotent, i.e. do we have $e(e(Z))\cong e(Z)$? Well, that is just asking whether

$(Z + 2^{\mathbb{N}}) + 2^{\mathbb{N}} \quad\text{is equivalent to}\quad Z + 2^{\mathbb{N}}$

but this again follows from $2^{\mathbb{N}} \cong 2^{\mathbb{N}} + 2^{\mathbb{N}}$! Showing that $e$ is not coherent is a bit harder, but still fairly straightforward using our description; I’ll leave it as an exercise, or you can try to decipher the Coq code.

### Example 3: Natural pointed sets

Let’s end by considering the following question: in what cases does the natural map $B S_{n-1} \to B S_{n}$ have a retraction, where $S_n$ is the symmetric group on $n$ elements? Looking at homotopy groups, this would imply that $S_{n-1} \hookrightarrow S_n$ has a retraction, which is true for $n\lt 5$ but not otherwise. But let’s look instead at the map on classifying spaces.

The obvious way to think about this map is to identify $B S_n$ with $B Aut(\mathbf{n})$, where $\mathbf{n}$ is the discrete set with $n$ elements, and similarly $B S_{n-1}$ with $B Aut(\mathbf{n-1})$. Then an element of $B Aut(\mathbf{n-1})$ is a set $Z$ with $n-1$ elements, and the map $B S_{n-1} \to B S_{n}$ takes it to $Z+1$ which has $n$ elements.

However, another possibility is to identify $B S_{n-1}$ instead with the classifying space of pointed sets with $n$ elements. Since an isomorphism of pointed sets must respect the basepoint, this gives an equivalent groupoid, and now the map $B S_{n-1} \to B S_{n}$ is just forgetting the basepoint. With this identification, a putative retraction $B S_{n} \to B S_{n-1}$ would assign, to any set $Z$ with $n$ elements, a pointed set $(r(Z),r_0)$ with $n$ elements. Note that the underlying set $r(Z)$ need not be $Z$ itself; they will of course be isomorphic (since both have $n$ elements), but there is no specified or natural isomorphism. However, to say that $r$ is a retraction of our given map says that if $Z$ started out pointed, then $(r(Z),r_0)$ is isomorphic to $(Z,z_0)$ as pointed sets.

Let’s do some small examples. When $n=1$, our map $r$ has to take a set with 1 element and assign to it a pointed set with 1 element. There’s obviously a unique way to do that, and just as obviously if we started out with a pointed set we get the same set back again.

The case $n=2$ is a bit more interesting: our map $r$ has to take a set $Z$ with 2 elements and assign to it a pointed set with 2 elements. One option, of course, is to define $r(Z)=2$ for all $Z$. Since every pointed 2-element set is uniquely isomorphic to every other, this satisfies the requirement. Another option motivated by example 1, which is perhaps a little more satisfying, would be to define $r(Z) = Iso(Z,Z)$, which is pointed by the identity.

The case $n=3$ is more interesting still, since now it is not true that any two pointed 3-element sets are naturally isomorphic. Given a 3-element set $Z$, how do we assign to it functorially a pointed 3-element set? The best way I’ve thought of is to let $r(Z)$ be the set of automorphisms $f\in Iso(Z,Z)$ such that $f^3 = id$. This has 3 elements, the identity and two 3-cycles, and we can take the identity as a basepoint. And if $Z$ came with a point $z_0$, then we can define an isomorphism $Z \cong r(Z)$ by sending $z\in Z$ to the unique $f\in r(Z)$ having the property that $f(z_0)= z$.

The case $n=4$ is somewhat similar: given a 4-element set $Z$, define $r(Z)$ to be the set of automorphisms $f\in Iso(Z,Z)$ such that $f^2 = id$ and whose set of fixed points is either empty or all of $Z$. This has 4 elements and is pointed by the identity; in fact, it is the permutation representation of the Klein four-group. And once again, if $Z$ came with a point $z_0$, we can define $Z \cong r(Z)$ by sending $z\in Z$ to the unique $f\in r(Z)$ such that $f(z_0)= z$.

I will end with a question that I don’t know the answer to: is there any way to see from this perspective on classifying spaces that such a retraction doesn’t exist in the case $n=5$?

Posted at January 19, 2015 6:25 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2800

### Re: The Univalent Perspective on Classifying Spaces

(typography: the later $C_n$s … did we mean $S_n$ or $𝔖_n$, perhaps? Of course we want to avoid Σ in the present context)

Posted by: Jesse C. McKeown on January 20, 2015 3:48 AM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

Duhh, yes. Thanks, fixed.

Posted by: Mike Shulman on January 20, 2015 11:23 PM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

I don’t think $\text{Iso}(Z, W)$ is morally correct, among other things because it’s naturally a contravariant functor in the first variable. Consider, for example, the case of invertible modules over a commutative ring $R$; the $2$-group structure here comes not from the hom (which fails even to be commutative) but instead the tensor product, which gives us $B \mathbb{Z}_2$ when $R = \mathbb{F}_3$. This operation is covariant in both variables, clearly commutative, and clearly associative, even coherently.

Let’s take a closer look at the tensor product of $1$-dimensional vector spaces over $\mathbb{F}_3$ to see what this construction is actually doing. Such a vector space can be identified with the two nonzero elements in it, which are swapped with each other under multiplication by $2 = -1 \in \mathbb{F}_3$. If $\{ 0, v_1, v_2 \}$ and $\{ 0, w_1, w_2 \}$ are two such vector spaces, with $v_2 = 2 v_1 = - v_1, w_2 = 2 w_1 = -w_1$, then their tensor product is $\{ 0, v_1 \otimes w_1, v_2 \otimes w_1 \}$ where $v_1 \otimes w_1 = v_2 \otimes w_2$ and $v_2 \otimes w_1 = v_1 \otimes w_2$.

So, as an operation on $2$-element sets, the tensor product of $1$-dimensional vector spaces over $\mathbb{F}_3$ corresponds to the following construction: take the cartesian product, which is a $4$-element set, then take orbits under the diagonal action of $\mathbb{Z}_2$, which is a $2$-element set. In other words, we are thinking of $2$-element sets as $\mathbb{Z}_2$-torsors and the $2$-group structure on $B \mathbb{Z}_2$ comes from taking the tensor product of $\mathbb{Z}_2$-torsors. This description generalizes to the case that $\mathbb{Z}_2$ is replaced by any abelian group and should work internally to many contexts.

Posted by: Qiaochu Yuan on January 20, 2015 7:31 AM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

Well, I don’t really find the fact that groupoids are self-dual to be morally wrong. (-: In fact, it’s a big part of the reason why homotopy type theory is easier than directed type theory. I also believe the definition as $Iso(Z,W)$ should work for torsors over any abelian group, and it has the advantage of not requiring any colimits — so, for instance, we can define it in HoTT without HITs (other than propositional truncation to define $B Aut$).

But your alternative description is also nice to have; thanks!. It’s not hard to see that it’s isomorphic to the definition I gave: a pair $z\otimes w \in Z\otimes W$ corresponds to the unique isomorphism $Z\cong W$ that sends $z$ to $w$. This isomorphism is natural on the groupoids of 2-element sets or 1-dimensional $\mathbb{F}_3$-modules, and unless I’m mistaken is moreover dinatural on the category of the latter — and this should also generalize to torsors over any abelian group.

Posted by: Mike Shulman on January 20, 2015 11:50 PM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

This is a minor point, but… it doesn’t seem to me that Iso(Z, W) is naturally a contravariant functor in the first variable. An arbitrary map from Z’ to Z doesn’t give us a map from Iso(Z, W) to Iso(Z’, W). Rather, it seems to me Iso(Z, W) is naturally an “isovariant” functor in both variables, and I would not normally think of “isovariance” as having separate co- and contra-variant flavors; my own morals are to view the situation with respect for its complete symmetry.

(This isn’t to quibble with anything else; I do often think of the group structure on 2-element sets in terms of tensor products of $\mathbb{Z}_2$-torsors)

Posted by: Sridhar Ramesh on January 23, 2015 10:31 PM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

I mean it’s a contravariant functor on the groupoid, of course. I think identifying left and right actions of groups or groupoids without explicitly saying that you’re doing so is bad categorical hygiene in the same way that identifying the tangent and cotangent bundles of a Riemannian manifold without explicitly saying that you’re doing so is bad categorical hygiene.

Posted by: Qiaochu Yuan on February 2, 2015 9:36 PM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

This is actually a really interesting point. What you say about categorical hygiene is very natural from the perspective of a category theorist, who thinks of groupoids as special categories. But from the perspective of a homotopy theorist, who thinks of groupoids as special homotopy types (1-types), there is no sense in asking whether a map between them is “contravariant or covariant”; all maps are just “isovariant” in the same way.

Posted by: Mike Shulman on February 2, 2015 11:50 PM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

Hm… I often would not identify tangent and cotangent bundles because I often am not in a context where there is a canonical isomorphism between them (e.g., in ordinary space in the physical universe, we do not have a “dimensionless” dot product, but rather, a dot product valued in squared distances, which have no distinguished unit, and thus there is no canonical isomorphism between vectors and covectors). It is good hygiene to not introduce a non-canonical identification, thus reminding oneself of the symmetries of the situation (between the various different non-canonical identifications possible).

But in a situation where there is a canonical isomorphism (e.g., between a groupoid and its dual), it seems to me much less “unhygienic” to construe such an isomorphism as an identification. In fact, in this case, it would be the drawing of distinctions between a supposedly contravariant first argument and covariant second argument in Iso(V, W) which would be obscuring the symmetries of the situation!

[But, again, I agree that the group structure on 2-element sets is more naturally understood in terms of tensor products than the Iso functor, making associativity, etc., obvious. This irrelevant quibbling is just as to the side issue of how to think hygienically about the Iso functor.]

Posted by: Sridhar Ramesh on February 12, 2015 11:17 PM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

Okay, I’m confused by a lot of things now:

1. Why should $\mathbf{B}\mathrm{Aut}(X)$ have terms given by types merely isomorphic to $X$? I would have thought that $\mathbf{B}G$ would have terms given by $G$-torsors, since $\mathbf{B}G$ classifies $G$-principal bundles and a fiber of a $G$-principal bundle is a $G$-torsor. If that’s right, then I’m confused because typically an $\mathrm{Aut}(X)$-torsor is a very different thing from a type merely isomorphic to $X$: for example, a 3-element set doesn’t carry a natural action of $S_3$, and 3-element sets don’t even have the same number of elements as $S_3$-torsors. If there’s an equivalence of types here, then it’s “non-concrete” and I don’t see it. In the case $X=2$, I suppose these descriptions are the same because a 2-element set is naturally an $S_2$-torsor.

2. Qiaochu, how does your construction generalize to arbitrary abelian groups? I must be misunderstanding something because it seems to me that it only generalizes to groups which are the multiplicative group of a field.

3. Mike, are you claiming that your definition of multiplication generalizes to other groups? I haven’t looked at your code, but the associativity proof I came up with $\mathrm{Iso}(\mathrm{Iso}(A,B),C) \to \mathrm{Iso}(A,\mathrm{Iso}(B,C))$ was $g \mapsto \lambda a.\lambda b. g(h_{a,b})$ where $h_{a,b}$ is the unique isomorphism mapping $a$ to $b$. This doesn’t look like it will readily generalize, regardless of how $\mathbf{B}G$ is defined.

Posted by: Tim Campion on January 23, 2015 1:28 AM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

The torsor construction works very nicely for groups we already know as groups, and even better for discrete groups with solvable word problem; but that doesn’t mean other constructions are wrong! The example of $\mathbf{B} Aut(X) \simeq \{ Y \& \| Y \simeq X \|_0 \}$ is a case of on the other hand, starting from something $X$ from which a canonical group $Aut (X)$ can be constructed. The equivalence is essentially just the content of the univalence axiom specialized to types isomorphic to $X$. If you like, that’s why you can’t see it: it’s an independent axiom.

Posted by: Jesse C. McKeown on January 23, 2015 4:06 AM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

Right, there can be lots of different-looking ways to define $B G$. An $Aut(X)$-torsor doesn’t look the same as a set merely isomorphic to $X$, but the groupoid of $Aut(X)$-torsors is equivalent to the groupoid of sets merely isomorphic to $X$. One way to define such an equivalence is that if $Z$ is merely isomorphic to $X$, then $Iso(Z,X)$ is an $Aut(X)$-torsor.

It’s easy to get confused when the group is $C_2 = S_2 = Aut(2)$, since $C_2$ itself has two elements and hence is merely isomorphic to $2$, and moreover any set merely isomorphic to $2$ comes itself with a canonical $C_2$-action. Neither of those is true for the group $G = Aut(X)$ for other values of $X$.

Another way to define $B G$, which works for any group $G$, is the obvious one: it has one object with $G$ as its automorphisms. (That doesn’t work in HoTT in exactly the same way, but there is a similar definition using a HIT.)

Qiaochu’s construction generalizes to arbitrary groups by using torsors rather than vector spaces, as Jesse said. (I’m not actually sure why he brought vector spaces into it at all.)

The definition of multiplication that I gave above does not generalize directly to other groups, and it had better not, because $Aut(X)$ is not generally abelian, so that $B Aut(X)$ doesn’t generally have a group structure! What I meant to say is that if we instead use torsors for an arbitrary abelian group $G$, then we can define the multiplication using the hom just as well as with the tensor.

Posted by: Mike Shulman on January 23, 2015 7:01 AM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

I brought in vector spaces in part because I thought they would be more familiar than torsors and in part because looking for a construction that makes sense on the category of vector spaces rather than on the groupoid of $1$-dimensional vector spaces makes it easier to notice the tensor product as a good candidate.

Posted by: Qiaochu Yuan on February 2, 2015 9:40 PM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

The link to the Coq code given in Example 1 doesn’t work, but this link seems to do the right thing:

https://github.com/HoTT/HoTT/blob/master/theories/Spaces/BAut/Bool.v

Posted by: Dan Christensen on January 30, 2015 12:06 AM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

Thanks, fixed. Sorry about that; the pull request to the main library got merged, but I hadn’t managed to update the link yet.

Posted by: Mike Shulman on January 30, 2015 5:54 AM | Permalink | Reply to this

### Re: The Univalent Perspective on Classifying Spaces

I hope someday someone writes an introductory text on homotopy theory which takes the HoTT perspective throughout. If it were written well it might be easier than the usual approach.

Posted by: John Baez on February 4, 2015 1:22 AM | Permalink | Reply to this

Post a New Comment