Why were ’comprehension categories’ given that name? And ’category with attributes’?

]]>Physics hasn’t fared any better with such indiscriminate use - theory (physics).

Great talk by the way. I think that’s the first time I heard you talking since Minneapolis in 2004. Funnily enough at that meeting I remember trying to work out a way of associating categorical levels to logical theories with John Baez. If I recall, it was based on the kind of $n$-groupoid that a theory’s models constituted: so a set of models of propositional logic, a groupoid of models of a first-order theory, and there was some thought of modal logic being at the next level with a 2-groupoid of models.

]]>Something I’ve been meaning to ask about for a while: it seems I only get email notifications of new comments on nForum threads I’m following when I’m actively logged in to the nForum site. Is this intended behaviour?

]]>MO question about citing the nLab: https://mathoverflow.net/questions/298384/is-it-possible-to-cite-a-page-in-n-lab-in-a-research-paper/298390

I added some possible BibTeX to my answer; it might helpful to include such at FAQ#Citing as well. Does anyone have any improvements to suggest?

]]>Something else to put on the to-do list: the nForum has a weird bug whereby it sometimes refuses to post a comment, saying it was unable to authenticate. Generally just clicking the “post” button again makes it work, but this is a little annoying (and may be more offputting for new users who aren’t familiar with it).

]]>By “simple type 3-theory” on slide 29 I meant the same as “simple type theory” regarded as a 3-theory (as on slide 33). I guess that slide 45 should probably have been “dependent type 3-theory”, meaning the same as “dependent type theory” regarded as a 3-theory as on slide 33. I’m not sure this is the best terminology though. Even once having the idea of what a 0-theory, 1-theory, 2-theory, 3-theory means in general, it’s hard to give good names to particular ones because historically the plain word “theory” has been used indiscriminately at several levels.

]]>Quick idea section for call-by-push-value

]]>Started linear-non-linear logic, more to come.

]]>Let’s see if I have the numbering of layers right.

So we might choose to work in the type 3-theory which is dependent type theory, then choose to work in it with a specific type 2-theory with specific type constructors, say Martin-Löf dependent type theory.

Then we may choose to specify some type and term generators and axioms they satisfy for a 1-theory in our 2-theory. Finally we can choose an interpretation of our 1-theory as a model, which may be called a 0-theory.

So if ’simple type theory’ and ’dependent type theory’ are each examples of a type 3-theory (slide 33). What kind of theory then is ’dependent type 2-theory’ (slide 45)? Or ’simple type 3-theory’ (slide 29)?

]]>I am preparing talk slides which, towards the end, mention the results about ADE-singularities that I have been alluding to in discussion with David C. in other threads. They are not completely finalized yet (references are missing, for instance) but fairly polished and should be readable. A link to the pdf (“”Structured Homotopy Theory from String Theory”) is on my web here.

]]>Re #24, so now we have a name, ’context shape’, for the dependency structure (slides 36-44 of Mike’s HOTTEST talk).

]]>Now we have type 2-theories and type 3-theories (from slide 30 of Mike’s HOTTEST talk), at some point we may want to modify doctrine and perhaps more significantly higher doctrine.

]]>I can only guess!

Whatever the intentions were, I feel the way it was implemented makes no sense (that’s why I regard it as a bug), because any restriction should be imposed earlier on, where the validation takes place in the code (I elaborate slightly more on this in the commit message), so that a reasonable message can be passed on to the user; and there is no restriction on spaces in this validation (I have not checked exactly what checks are in place, but I was able to trigger a validation failure with something like the following.

[[hello%20hello|hello.pdf]]

The error displayed in such a case is not exactly great UI, but at least it is not a splurge of a stacktrace!).

Of course one needs to escape spaces in filenames on Unix systems, so maybe the original intention was to avoid worrying about that, or some such thing. If anyone does encounter any issues with or after uploading a file whose name includes spaces, just let me know, and I’ll look into it.

]]>Thanks! Do you have any idea why there was this restriction on filenames involving spaces? Just an irrational prejudice against such filenames?

]]>Fixed a bug (predating the changes of #14) which prevented filenames involving spaces (for instance) being used, but only in such a way that an error occurred internally in Instiki, with the details of the error being splurged on the edit page for the affected page. There is still a little validation in place, but spaces are now permitted, and if validation fails, a more palatable error is presented to the user. The commit is available on github.

]]>Moved to history, will redirect to identity element instead.

]]>No, only that nobody did. I have explained in #2 what happened.

]]>Similarly, the double cover $D$ of $S^1$ *is* B-finite in the truncated internal sense of “there (merely) exists a natural number $n$ and an isomorphism $[n]\cong D$”.

The double-cover of $S^1$ is definitely a covering space with finite fibres, but I don’t see which $n$ to take to get a surjection $n\to A$.

The cover of $S^1$ by two overlapping intervals has the property that over it the double cover of $S^1$ is locally (indeed globally) constant at $2$, which is what the characterization is asking for. I’m not sure what $n$ you are talking about.

The Möbius strip is not a free module in the external sense of there being a global section as basis element, but might it be different internally, that at the level of stalks it is free?

I think it depends on whether we formulate “$V$ is free” with a truncated $\exists$ or with an untruncated $\Sigma$. If “$V$ is free” means “there exists a set $S$ and a function $f:S\to V$ such that every $v\in V$ can be expressed uniquely as $v = r_1 f(s_1) + \cdots + r_n f(s_n)$” and “there exists” is truncated, then it allows passing to a cover, and the Mobius strip is free over the cover of $S^1$ by two overlapping intervals. But if it’s not truncated then we have to give a global $S$ and $f:S\to V$, and I don’t think that’s possible.

]]>Added an abstract PBW theorem due to Dotsenko and Tamaroff.

]]>The Möbius strip is not a free module in the external sense of there being a global section as basis element, but might it be different internally, that at the level of stalks it is free? I seem to remember a statement somewhere that Kaplansky’s theorem, that projective modules over local rings are free, carries over in some degree to some toposes like sheaves over a compact space; see this excerpt from Johnstone’s Topos Theory.

]]>The standard biased definition of vector space, in which you can add two elements and zero elements, is the correct one constructively as well. The unbiased version that this generates allows you to sum (Bishop-)finite families of elements.

That’s nice. Taking the strictest possible notion of “sets you are allowed to sum over” gives you the most general possible definition of vector space. I suppose this means that the construction of the free vector space on the set $A$ is given by the formal sums of B-finite subsets of $A$.

Actually that only works if the subset is decidable, otherwise you can’t define a function by cases to be “as given inside and 0 outside”. And a decidable subset of a finite set is still finite, so this doesn’t give you anything extra.

Ah yes, that makes sense. I worried a bit about that before I wrote it, but I managed to convince myself that it’s possible to define the complement (just pullback along the “false” map $1\to 2$ rather than the “true” one). But the problem isn’t that you can’t define the complement; it’s that you can’t prove every element is either in the original set or the complement.

I don’t offhand see a reason that every finitely-generated projective vector space would be free.

Yeah, that sounds false. My understanding is that for any topological space $X$ we can recover the category of vector bundles over $X$ as the category of vector spaces over the Dedekind reals inside the topos of sheaves on $X$. And a vector bundle is dualisable iff it’s locally finite-dimensional. So consider the “Möbius-strip” 1-dimensional real vector bundle over the circle. It’s not free, but it’s dualisable.

In fact I think this gives us an example of a set that isn’t B-finite, but whose free module is dualisable. Again working in the topos of sheaves of $S^1$, let $A$ be the sheaf of sections of the nontrivial double-cover of $S^1$. Then $A$ is K-finite but not B-finite. But the free module on $A$ is dualisable, because as a bundle it’s locally 2-dimensional.

(Actually I don’t quite understand this. The nLab says at finite object that

In the category of sheaves $\mathrm{Sh}(X)$ over a topological space, the decidable K-finite objects are those that are “locally finite;” i.e. there is an open cover of $X$ such that over each open in the cover, the sheaf is a locally constant function to $N$. These are essentially the same as covering spaces of $X$ with finite fibres.

but I don’t see how this works in the case of $A$. The double-cover of $S^1$ is definitely a covering space with finite fibres, but I don’t see which $n$ to take to get a surjection $n\to A$.)

]]>Should the section “Units of measurement” at unit have a pointer to physical unit for further discussion? I would assume so, but I don’t quite understand the technical business that’s going on at physical unit, so I thought I’d check.

]]>Is there any reason not to redirect neutral element to identity element?

]]>