## Cohomology

For people interested in doing homotopy theory in homotopy type theory, Chapter 8 of the HoTT Book is a pretty good record of a lot of what was accomplished during the IAS year. However, there are a few things it’s missing, so I thought it would be a good idea to record some of those for the benefit of those wanting to push the theory further. (Hopefully at some point, papers will be written about all of these things…)

Today I want to talk about cohomology. Chapter 8 of the book focuses mostly on calculating homotopy groups, which are an important aspect of homotopy theory, but most working algebraic topologists spend more time on homology and cohomology, which (classically) are more easily computable. It’s an open question whether they will be similarly easier in homotopy type theory, but we should still be interested in defining and studying them.

Most of what I’m going to say in this post is not original or new, and should be attributed to lots of people (e.g. many of the people mentioned in the Notes to Chapter 8). At the end I’ll remark on a recent surprise that came up on the mailing list.

I’m going to use the notation of the book, such as $\Vert-\Vert_n$ for the n-truncation, with simply $\Vert-\Vert$ for the propositional truncation in the case $n=-1$. I’ll also adopt the book’s convention that the adjective merely indicates application of the propositional truncation.

### The definition of cohomology

Classically, there are many definitions of cohomology, but the one that seems most correct and tractable in homotopy type theory is the representable one. In its most general form, for any types X and Y, we define the (nonabelian) cohomology of X with coefficients in Y to be the 0-truncation of the mapping space from X to Y:

$H(X;Y) := \Vert X\to Y\Vert_0.$

It is, of course a set. This should seem like a fairly natural thing to study, since maps between types are important, and big types with lots of homotopy are complicated, so we might hope that their 0-truncations are simpler.

More precisely, the above definition is the 0th cohomology, $H^0(X;Y)$. The nth cohomology for $n<0$ is defined by adding loop spaces:

$H^n(X;Y) := \Vert X\to \Omega^{-n} Y\Vert_0 \qquad (n\leq 0).$

Note that if $n\leq -1$, then $H^{n}(X;Y)$ is always a group (it inherits the loop composition operation from $\Omega Y$), while if $n\leq -2$ then it is an abelian group by the Eckmann-Hilton argument. For positive n, the nth cohomology is only defined if Y is a loop space, so that we can “un-loop” it. Namely, if $Y = \Omega^n Y_n$ for some $n > 0$, then we can define

$H^n(X;Y) := \Vert X\to Y_n \Vert_0 \qquad (n\geq 0).$

This notation is a bit misleading, though, because this set depends not only on the type Y but on the choice of its “delooping” $Y_n$. In general, a type may admit lots of different deloopings (and some types have none at all). Classically, algebraic topologists are most interested in cohomology with coefficients in types that have all deloopings in a specified way. Such a type is called a spectrum.

More precisely, a spectrum is a family of types $Y : \mathbb{N} \to \mathcal{U}$ such that for all n we have (a specified equivalence) $Y_n = \Omega Y_{n+1}$. For such a Y, we define the (abelian) cohomology of X with coefficients in Y to be

$H^n(X;Y) := \Vert X \to \Omega^{k-n} Y_k \Vert_0 \quad (n \in \mathbb{Z})$

where k is sufficiently large so that $k-n \geq 0$. (The assumptions $Y_n = \Omega Y_{n+1}$ mean that the definition is independent of k as long as it is sufficiently large.) Note that these are all abelian groups, which is part of what makes them easier to calculate with.

Where do spectra come from? The “standard” spectra are built out of Eilenberg-Mac Lane spaces, which are mentioned briefly in the book but not expanded on. For an abelian (set) group G and $n \in \mathbb{N}$, an Eilenberg-Mac Lane space of type $K(G,n)$ is a pointed, $(n-1)$-connected, $n$-type Y such that $\pi_n(Y) = G$ (and all other homotopy groups are trivial, by the assumptions). For instance, the higher inductive circle is an Eilenberg-Mac Lane space of type $K(\mathbb{Z},1)$.

One result that was proven last spring (by Dan Licata) is that Eilenberg-Mac Lane spaces exist for all G and n. It’s easy to see that they are unique, and that $\Omega (K(G,n+1)) = K(G,n)$. Thus, for fixed G, we have an Eilenberg-Mac Lane spectrum $H G$, defined by $(H G)_n = K(G,n)$. Cohomology with coefficients in HG is called ordinary cohomology with coefficients in G,

$H^n(X;G) := H^n(X;H G).$

### The Eilenberg-Steenrod axioms

Now as I mentioned, in classical algebraic topology, cohomology has lots of equivalent definitions. Some of them, like cellular and simplicial cohomology, seem difficult or impossible to mimic in homotopy type theory. But another very useful classical characterization of cohomology is via what are called the Eilenberg-Steenrod axioms. One writes down a list of properties satisfied by the family of functors $H^n(-;G)$, and then it is a theorem that any family of functors satisfying these axioms is equal to $H^n(-;G)$ for some abelian group G. In many cases, cohomology groups can be calculated using only the axioms, without needing to invoke any particular definition. So it’s natural to want to show at least that our definition in homotopy type theory satisfies the axioms.

Actually, the axioms don’t quite apply to the cohomology functors we’ve defined above, but rather to the reduced cohomology functors $\tilde{H}^n(X;G)$, defined whenever X is a pointed space (i.e. equipped with an element $x_0:X$) by replacing the type of maps by the type of pointed maps (those which send the basepoint to the basepoint). If X is unpointed, then $X_+ := X+1$ is pointed and we have $\tilde{H}^n(X_+;G) = H^n(X;G)$, so these groups are actually more general. (An equivalent list of axioms can also be formulated for relative cohomology, in which the input is a map of unpointed types.)

Here are the axioms, which apply to a collection of contravariant functors $\tilde{Y}^n:\underline{\mathsf{Type}_*} \to \underline{\mathsf{AbGrp}}$ from pointed types to abelian groups.

1. Exactness: For any map $f:A\to B$ with cofiber $C_f$, the sequence $\tilde{Y}^n(C_f) \to \tilde{Y}^n(B) \to \tilde{Y}^n(A)$ is exact.

2. Suspension: We have natural isomorphisms $\tilde{Y}^n(X) \cong \tilde{Y}^{n+1}(\Sigma X)$, where $\Sigma X$ is the suspension of X.

3. Additivity: For a set-indexed family of pointed spaces $X:I \to \mathsf{Type}_*$, with $\bigvee_i X_i$ their wedge (joint pushout over the basepoints), the induced map $\tilde{Y}^n(\bigvee_i X_i) \to \prod_{(i:I)} \tilde{Y}^n(X_i)$ is an isomorphism.

A collection of such functors is called a cohomology theory, and it is said to be ordinary if $\tilde{Y}^n(S^0) = 0$ for $n\neq 0$ (note that the reduced cohomology of $S^0$ is the unreduced cohomology of a point). Ordinary cohomology theories correspond to the Eilenberg-Mac Lane spectra H G, where G is the 0th unreduced cohomology of a point. In this case, the above axioms are enough to compute the cohomology of any CW complex, and this is how the uniqueness theorem can be proven in classical algebraic topology. Namely, a CW complex X can be stratified into subspaces $X_n$, where $X_n$ is obtained from $X_{n-1}$ by attaching n-discs. Then the cofiber of the inclusion $X_{n-1} \to X_n$ is a wedge of n-spheres, so that its cohomology is determined by the suspension and additivity axioms; hence by induction we can calculate the cohomology of each $X_n$. Unraveling all this yields the usual definition of cellular cohomology.

Now recall that in homotopy type theory, for any spectrum Y, our definition of reduced cohomology is

$\tilde{Y}^n(X) := \tilde{H}^n(X;Y) := \Vert \mathrm{Map}_*(X,\Omega^{k-n} Y_k) \Vert_0,$

where $\mathrm{Map}_*(-,-)$ denotes the type of pointed maps. Unlike in classical homotopy theory, not every type is equivalent to a CW complex, so we shouldn’t expect a uniqueness theorem, but if we could show the axioms, then we could hope to at least calculate cohomology of all types that are CW complexes. So let’s try to prove the axioms.

For exactness, the universal property of the cofiber $C_f$ says essentially that for any Z, we have a fiber sequence

$\mathrm{Map}_*(C_f,Z) \to \mathrm{Map}_*(B,Z) \to \mathrm{Map}_*(A,Z)$

Passing to 0-truncation from this yields the desired exact sequence. For the suspension axiom, the adjointness between suspension and loop spaces yields

$\mathrm{Map}_*(X,\Omega^{k-n} Y_k) = \mathrm{Map}_*(\Sigma X, \Omega^{k-n-1} Y_k)$

so that passing to 0-truncation yields the desired isomorphism. Finally, since wedges are coproducts of pointed types, given $X:I \to \mathsf{Type}_*$ we have

$\mathrm{Map}_*(\bigvee_i X_i, Z) = \prod_i \mathrm{Map}_*(X_i,Z)$

for any Z. Now we can pass to 0-truncation and conclude the additivity axiom… if $\prod_i$ commutes with 0-truncation! This is true if the indexing set I is finite, but in general, it is a sort of axiom of choice, and can fail even if I is an otherwise well-behaved type like the natural numbers.

The finite additivity axiom, along with the other axioms, is enough to show (by the above sort of arguments) that the ordinary cohomology of any finite CW complex (such as a sphere or a torus) agrees with its value in classical algebraic topology. This is nice; but what about the infinite case?

### The cohomology of sets

In fact, it seems that there are models where infinite additivity fails, and where the cohomology of infinite complexes can look very different from its classical value. On the mailing list a few days ago, I sketched an argument that the cohomology

$H^1(\mathbb{N};\mathbb{Z})$

can be nontrivial. Here $\mathbb{N}$ denotes the usual (infinite) set of natural numbers, which is in particular a set, having no higher homotopy above dimension 0. It even has decidable equality. Nevertheless, the claim is that in some models, it can have nontrivial higher cohomology!

This may seem extremely bizarre at first, but it seems less strange if you know something about the models in question. On the one hand, we already knew that in some toposes there are sets with nontrivial cohomology. For instance, there are "cohesive" toposes which contain all classical smooth manifolds as objects, and in which their internally defined cohomology agrees with their usual cohomology (and hence is nontrivial). Note that although such manifolds are of course not “discrete sets” in the usual sense, they are still “sets” in the sense of the model, i.e. 0-truncated objects. (There is another, unrelated, internal notion of “discreteness” in such models.) However, these models don’t explain how a set like $\mathbb{N}$, which is discrete in all possible senses, could have nontrivial cohomology.

On the other hand, there are toposes of sheaves on topological spaces, in which we might naturally expect the (external) cohomology of the space on which we are considering sheaves to be visible in some way. The relationship isn’t completely straightforward, though, because as I mentioned above, internally, weird things can only happen in the cohomology of infinite spaces (like $\mathbb{N}$).

To see how this can happen, note first that since $K(\mathbb{Z},1)=S^1$, calculating $H^1(\mathbb{N};\mathbb{Z})$ is about looking for maps $\mathbb{N} \to S^1$, i.e. sequences of points on the circle. The basic idea of the argument is that there can be nonstandard points on the circle, i.e. points $x:S^1$ which are not provably equal to the basepoint. (Of course, like all points on the circle, they are merely equal to the basepoint, i.e. $\Vert x=\mathsf{base}\Vert$ is inhabited, though $x=\mathsf{base}$ may not be.)

To produce a nonstandard point of the circle, suppose we have mere propositions P, Q, R, S such that $\Vert P+Q\Vert$ (the “mere disjunction” of P and Q) holds, and such that $P\times Q = R+S$. Now it is a fact that the mere disjunction is equivalent to the join $P*Q$, i.e. the pushout of P and Q under $P\times Q$. This can be proven by a fairly tedious calculation; Nicolai Kraus and Christian Sattler have recently given a slicker argument that also doesn’t require having $P*Q$ in hand to begin with.

Thus, since $\Vert P+Q\Vert$ holds by assumption, we may define a point of $S^1$ by induction on $P*Q$, which is to say we have to give functions $P\to S^1$ and $Q\to S^1$ and a proof that they agree on $P\times Q$. We take both functions to be constant at the basepoint (what else could we do?). But on $P\times Q$, which is equal to $R+S$, we divide into cases: if R, we take the proof of equality $\mathsf{base}=\mathsf{base}$ to be reflexivity, while if S we take it to be some nontrivial loop (such as the generating loop of the circle).

This yields a point of the circle, but it is not obvious how to prove that this point is equal to the basepoint. And indeed, in some models it is not equal to it. For instance, in the topos of sheaves on the topological circle, with P and Q the complements of two antipodal points, these “nonstandard” points form the external degree-1 cohomology of the topological circle with coefficients in $\mathbb{Z}$, which is certainly nontrivial. A less topological example is the topos of presheaves on the poset $\{a,b,c,d\}$ with $a\leq c$ and $a\leq d$ and $b\leq c$ and $b\leq d$, where P and Q are the representables at c and d. (Note that the geometric realization of this poset is the topological circle.)

However, the internal cohomology $H^1(1;\mathbb{Z})$ is still trivial: these nonstandard points are all still merely equal to the basepoint, hence become equal upon 0-truncation. But we can obtain nontrivial internal cohomology by invoking the failure of the axiom of choice. Roughly, if we define $f:\mathbb{N} \to S^1$ such that each $f(n)$ is a nonstandard point defined using a different collection of P, Q, R, S, then we have $\prod_{(n:\mathbb{N})} \Vert f(n) = \mathsf{base}\Vert$, but that won’t necessarily imply $\Vert \prod_{(n:\mathbb{N})} (f(n) = \mathsf{base})\Vert$, so that f may represent a nontrivial element of $H^1(\mathbb{N};\mathbb{Z})$. The best concrete example I’ve thought of so far is the topos of sheaves on the topological Hawaiian earring, where we have countably many circles that we can use to define countably many nonstandard points, but only finitely many of these points can be trivialized over any open cover.

So what are we to make of a theory where $H^1(\mathbb{N};\mathbb{Z})$ can be nontrivial? On the one hand, we might find it a bit depressing for the prospect of doing homotopy theory in homotopy type theory: we can’t even determine the ordinary cohomology of such a simple space as the natural numbers. On the other hand, it’s also kind of exciting. We have an entirely new thing to study, which is apparently only visible in constructive homotopy type theory: the cohomology of sets!

What does the cohomology of a set mean? This example suggests that as long as the “ambient logic” has sufficiently nontrivial cohomology (i.e. there are enough nonstandard points of the circle, or more generally nonstandard points of Eilenberg-Mac Lane spaces), then the cohomology of a set X “measures” the failure of the axiom of choice for certain X-indexed families. This shouldn’t be surprising, since geometrically, cohomology can be said to measure the existence of “nontrivial coverings” of a space. But it suggests that we could use cohomological methods in logic. For instance, the exactness and finite additivity axioms are still true for the cohomology of sets, hence give us ways to calculate that cohomology when a complicated set is constructed out of simpler ones. The same would apply to other calculational tools, like spectral sequences, once we establish them in homotopy type theory.

This entry was posted in Homotopy Theory, Models. Bookmark the permalink.

### 18 Responses to Cohomology

1. Zhen Lin says:

In a paper of Andreas Blass (_Cohomology detects failures of the axiom of choice_), he shows that, if all sets have trivial H^1, then the axiom of choice holds. More precisely, if a particular set X has trivial H^1 for all coefficient groups (not necessarily abelian), then every surjection onto X splits.

• Mike Shulman says:

Ah, excellent! I see he also shows that if $H^1(X;G)$ vanishes for all sets X and all abelian groups G, then the axiom of choice holds, although he doesn’t manage to “localize” the abelian case to projectivity of individual sets.

Here is a theorem about projective sets that follows from Blass’ result. Suppose we have a function $f:A\to B$ such that $A$ and $B/A$ are projective. Then for any coefficient group G, in the exact sequence of pointed sets

$H^1(B/A;G) \to H^1(B;G) \to H^1(A;G)$

the first and third terms are trivial, hence so is the middle one. Thus, $B$ is also projective. I don’t immediately see how to prove that without cohomology, but there’s probably a way; anyone see it?

The “Serre spectral sequence” for nonabelian cohomology of sets is just a short exact sequence: given a map $p:E\to B$ with fibers $F_b$, we have an SES of pointed sets

$0 \to H^1(B;H^0(F;G)) \to H^1(E;G) \to H^0(B;H^1(F;G))$

where $H^*(F;G)$ is actually the family $b\mapsto H^*(F_b;G)$ of sets (or groups) indexed by $b:B$, so that the first and third terms are actually cohomology with local coefficients. (In the case of a product projection $E = F\times B$, the local coefficients go away.) This implies that if $B$ and each $F_b$ are projective, then so is $E$. That’s certainly easy to prove directly, using the universal property for maps out of $E = \sum_{(b:B)} F b$, but it’s cute that we can see it as a consequence of homological algebra!

(Hopefully in my next post I’ll explain how to get the Serre SS in homotopy type theory.)

• Mike Shulman says:

In the application to cofibers, the function $f:A\to B$ has to be injective, otherwise the cofiber may no longer be a set. This conclusion is also easy to prove if we assume LEM, since any family of merely inhabited sets over B can then be divided into one over A and one over $B/A = (B\setminus A) + 1$, extended trivially over the basepoint in the latter case. Without LEM, it seems to me like the natural thing to do is consider the family over $B/A$ defined by dependent product along the quotient map, but I don’t see how to show that all the fibers of the quotient map are projective: the assumption that A is projective handles the fiber over the basepoint, and the fiber over a point that isn’t the basepoint is the unit type, but still, without LEM I don’t know what to do in general.

• Mike Shulman says:

This also means I was wrong in saying that the cohomology of sets is only visible to HoTT. Blass defines $H^1(X;G)$ following Giraud, as the set of isomorphism classes of G-torsors over X. (Interestingly, at least the naive form of this definition goes up a universe level, an issue which as far as I can see Blass doesn’t address.) This agrees with the HoTT definition, because the type of G-sets that are merely isomorphic to G (which classifies G-torsors almost by definition) can be shown to be a $K(G,1)$. In particular, this implies that the ordinary axiom of choice, which the book calls $\mathsf{AC}_{0,-1}$, is the one whose failure is detected by $H^1$.

So, what about the other forms of AC, and what about $H^n$ for $n>1$? If there were a relationship between them, then that might go some ways towards answering the question of which other forms of AC are interesting.

• Zhen Lin says:

I think the universe level problem goes away in ZF because we can use Scott’s trick. I’m glad you found the paper interesting! I had wanted to study the connection between logic and geometric invariants for a while now but never got around to it.

• Mike Shulman says:

Yes, there is usually that, but I’m a bit surprised he didn’t even mention it.

Unfortunately, I just noticed that his proof (both of them) does use excluded middle. )-: I wonder if one can do without that.

• It wouldn’t go up a universe level with if WISC held.

• Mike Shulman says:

Of course, in HoTT we don’t need to worry, because we can show that $G$-torsors are classified by maps into the HIT $K(G,1)$, which lives in the same universe.

In ZF, you may be right that WISC is what we need. Let’s see, I guess we would take the fiberwise free $G$-set on each of a weakly initial set of covers, then consider the set of all fiberwise $G$-set quotients of those that are torsors?

And on second thought, I’m not sure that Scott’s trick would be enough. It would give us a (set of) representatives for each isomorphism class of torsors, but how do we know that there are only set-many such isomorphism classes?

2. Bas Spitters says:
• Mike Shulman says:

Indeed! And I remember reading that question and its answers, so I have no excuse for not knowing about Blass’s paper. (-:

3. Mike Shulman says:

By the way, it’s easy to produce nontrivial higher cohomology too. For instance, suppose we have hprops $P_0, Q_0, P_1, Q_1, P_2, Q_2$ such that $P_0 \vee Q_0$ and $P_0\wedge Q_0 = P_1 \vee Q_1$ and $P_1 \wedge Q_1 = P_2 + Q_2$. Then we can similarly define a nonstandard point of $S^2$, hence also of $K(\mathbb{Z},2)$, which has to do with the external $H^2(S^2;\mathbb{Z})$. By then passing to sheaves on a space that I’m tempted to call the “Hawaiian Matryoshka ball”, we ought to obtain a nontrivial $H^2(\mathbb{N};\mathbb{Z})$.

According to Blass’s theorem, a nontrivial $H^1(\mathbb{N};\mathbb{Z})$ implies that countable choice fails. Does nontrivial $H^2(\mathbb{N};\mathbb{Z})$ imply that countable choice fails “worse”?

4. Mike Shulman says:

Here is a hotter version of one of Blass’s proofs. Suppose X is a set with vanishing $H^1$ with all coefficients, and let $p:Y\to X$ be a surjection where Y is also a set. Consider the homotopy pushout (i.e. not the set-pushout):

If Y and X have decidable equality, then C is a 1-type. It is an open question whether this is always true. (It’s a slightly more general version of the question raised by Guillaume of whether the suspension of a set is always a 1-type.) It seems to be true in all known models, but no one has managed to prove it yet.

But anyway, even if C isn’t a 1-type, we can consider its 1-truncation, $\Vert C \Vert_1$, which is. Since p is surjective, i.e. 0-connected, so is $c: \mathbf{1}\to C$, and hence so is $|c|_1: \mathbf{1}\to \Vert C\Vert_1$. Thus, $\Vert C \Vert_1$ is a pointed connected 1-type, hence equivalent to $K(G,1)$ for some group G (namely $G :\equiv (|c|_1 =_{\Vert C \Vert_1} |c|_1) = \Vert c =_C c \Vert_0$).

Therefore, the map $|f|:X\to \Vert C\Vert_1$ represents a class in $H^1(X;G)$, which by assumption is trivial. Hence, $|f|$ is merely equal to the constant map at c, and thus there merely exists a homotopy $H: \prod_{(x:X)} \Vert f(x) = c \Vert_0$.

Now, by a van-Kampeny sort of argument, $\Vert f(x) = c \Vert_0$ is a quotient of the set of finite sequences

$y_0 z_1^{-1} y_1 z_2^{-1} y_2 \cdots z_n^{-1} y_n$

where each $y_i, z_i \in Y$, with $p(y_0) = x$, and $p(z_i) = p(y_i)$ for all $i\ge 1$. The quotient allows us to cancel $y^{-1} y$ and $y y^{-1}$ wherever they appear. Just as with free groups, if Y and X have decidable equality, then any such sequence is equivalent to a unique reduced one in which all adjacent elements are distinct. In particular, the “first element” of a reduced word is well-defined, and thus we have a section of p sending each x to the first element of the reduction of $H(x)$.

Constructively, however, it’s not clear where to go from here.

5. jessemckeown says:

Allow me to register my doubt on the theoremness of set suspensions always being 1-types. It’d be nice, of course (and I wouldn’t mind being wrong) but your multifarious uses of “hawaiian” today have rather shaken my confidence in being able to separate earings from suspensions of $\omega$, while it’s easy to choose a metric on an earing space such that its loop spaces ought to be a Cantor set, and then nonstandard anything seems conceivable.

• Mike Shulman says:

Well, the “suspension” we’re talking about is purely $\infty$-groupoidal, not topological at all, so I don’t think there’s any danger of anything hawaiian entering in.

6. Urs Schreiber says:

Apart from the interpretation in logical terms (failure of axiom of choice) there is also be an interpretation of this phenomenon in geometric terms, which maybe sounds less mysterious:

First of all, as mentioned in the above post but to amplify again: it is clear that there are h-sets with nontrivial cohomology. The interesting step is rather that there are h-sets (like the natural number object ) that “look discrete” and still have non-trivial cohomology. One way to understand this geometrically is to notice that these may “look discrete” but are not actually *discrete objects* in the technical sense.

To make this precise, use the notion of “discrete object” as defined here: http://ncatlab.org/nlab/show/discrete object . An infinity-topos has discrete objects if the left adjoint to the global sections functor is fully faithful, hence if it respects hom-spaces. An object in the image of this left adjoint generally tends to “look discrete”, but if the left adjoint is not full and faithful, then it is in fact not. And since hom-spaces precisely compute cohomology, one way to say find it is not full and faithful is that it sends trivial cohomology to non-trivial cohomology.This is the phenomenon discussed above.

One could use this to refine the notion of “dsicrete object”: even if the left adjoint to global sections is not fully faithfull, a restriction of it may be. The objects in the image of this restriction would be those objects that not only look discrete, but in fact are discrete, as measured by their cohomology.

7. Alexander Shamov says:

Here is a very naive observation.
If we define, say, $H^1(X, \mathbb{Z})$, as homotopy classes of maps into $S^1$, the usual topological circle, then LEM alone implies that $H^1(X, \mathbb{Z})$ is trivial for any set $X$. Indeed, assuming LEM the obvious injection $[0,1) \to \mathbb{R} / \mathbb{Z} \simeq S^1$ becomes invertible (and we don’t care about continuity here due to discreteness of $X$). Using this, we can factor any map into $S^1$ through $[0,1)$, and then contract it there.
I don’t see any obvious way to avoid LEM. Do you?
And is it possible to translate this argument into the hott framework?

• Mike Shulman says:

I don’t think that any such argument can work in HoTT, because the relevant circle is not topological.

8. Steven Meyerson says:

Notify me of new posts via email.