tried to edit Ext a bit. But this needs to be expanded, eventually.

]]>starting something, but am being interrupted now. Am saving anyway to make the link work

]]>started atomic geometric morphism

]]>I tried to structure the entry Heyting algebra a bit more. Check if you like it.

I also added a little bit to the Examples-section.

In the section on toposes it says that a “Grothendieck (0,1)-topos” is a locale. Is that correct? Shouldn’t it say: a Grothendieck (0,1)-topos is a category of open subsets of a topological space?

]]>I have added to *principal bundle*

a remark on their

*definition*As quotients;statements about (classes of) (counter-)examples of quotients

Thanks for pointers to the literature from this MO thread!

]]>a disambiguation page, for

]]>I am beginning to split off from *fiber sequence* an entry *long exact sequence in homology* (also splitting off all the related redirects, such as long exact sequence in cohomology etc).

A disambiguation page.

]]>I added a note about what “projectively flat” means in the context of parabolic Cartan geometry. I would assume that this should mean the same thing as “a connection which is flat up to central term” as described in the first sentence?

]]>Started something at homotopical algebraic geometry, have to run now.

]]>That doesn’t look right at Via left homotopy of spectra. $\ell$ is supposed to be the forgetful functor from spectra to prespectra.

But what kind of spectra are we looking at? It seems to be coordinate-free spectrum. So then we need a definition of prespectrum.

]]>Earlier today I was checking where on the $n$Lab we had recorded basics on finite homotopy (co)limits of spectra. But it seems we haven’t at all, except for the discussion at *Introduction to Stable homotopy theory*.

So then I started to add something at *Spectra*, only to notice that this needs harmonizing/merging with the parallel entry *stable (infinity,1)-category of spectra*.

To cut this Gordian knot, I am now creating hereby an entry with a bare section on finite homotopy (co)limits of spectra, to be `!include`

ed into these entries (and into *stable homotopy category* and maybe elsewhere, too).

So far I have just some bare minimum here. Deserves to be expanded.

]]>added rough description and original citation to *Adams e-invariant*

for ease of reference, and to go along with *SO(2), Spin(2), Pin(2), Spin(3), Spin(4)*

I am in the process of preparing a piece on [[Hochschild cohomology]]

while the Lab is down, I'll abuse the forum here for posting my source. Probably not well suited for reading it, but just so the effort is not wasted should my notebook get run over by a bus. That could happen, as the buses here in Sheffield go on the wrong side of the road.

See followup comment...

]]>am giving this its own little entry (in line with Spin(2), Spin(3), Spin(4), Spin(5)). For the moment just as to record a nice reference for the exceptional iso $Spin(6) \simeq SU(4)$

]]>A bare reference item. For the moment just as an experiment, to go with the discussion here.

]]>pure morphism (much more to be said, and more references, but no time now)

]]>Just for completeness, to go with *e-invariant* and *f-invariant*.

renamed [[model structure on marked simplicial oversets]] to [[model structure for Cartesian fibrations]]

merged the material that was at [[marked simplicial set]] (now [[marked simplicial set > history]]) into this entry

expanded the entry a bit, but still working on it...

I strongly disagree with the statement in Grothendieck category that the Grothendieck category is small. The main examples like ${}_R Mod$ are not! What did the writer of that line have in mind ?

]]>Since I gathered them for my recent talk, I may as well provide a list here of work in this area. I need to add names, etc.

]]>Added a subsection

]]>## As a homotopy type

As a homotopy type the torus is the product of two copies of the circle.

In homotopy type theory the torus can be formalized as the higher inductive type generated by a point

`base`

, two paths, $p$ and $q$, from`base`

to itself, and an element $t$ of $p\cdot q = q \cdot p$. It has been formally shown (Sojakova15) that this type is equivalent to the product of two circles. For a treatment in cubical type theory, see (Licata-Brunierie).

brief `category:people`

-entry for hyperlinking references at *Nielsen-Schreier theorem*