There’s an interesting-looking MSRI workshop Chern-Simons and Other Topological Field Theories.

I wonder what this abstract from Sylvester Gates is referring to:

]]>In 1992 at Howard University, the first descriptions of maximally extended supersymmetric Chern-Simons Theory were formulated. This initiated a research program combining SUSY with topology that in 2021 resolved a forty year-old puzzle about eleven dimensional supergravity. The discovery arc of this journey is presented in this talk.

We are finalizing this article here, if you have any comments, please drop a note:

**Twisted Cohomotopy implies M-theory anomaly cancellation**

**Abstract.** *We show that all the expected anomaly cancellations in M-theory follow from charge-quantizing the C-field in the non-abelian cohomology theory twisted Cohomotopy. Specifically, we show that such cocycles exhibit all of the following:*

*the half-integral shifted flux quantization condition,**the cancellation of the total M5-brane anomaly,**the M2-brane tadpole cancellation,**the cancellation of the $W_7$ spacetime anomaly,**the C-field integral equation of motion,**the C-field background charge.*

*Along the way, we find that the calibrated $N =1$ exceptional geometries (${Spin}(7)$, $G_2$, ${SU}(3)$, ${SU}(2)$) are all induced from the classification of twists in Cohomotopy. Finally we show that the notable factor of $1/24$ in the anomaly polynomial reflects the order of the 3rd stable homotopy group of spheres.*

```
<div>
<p>Probably most contributors here have subscribed to the category theory mailing list. For those who have not, this is to point out that lately the nLab keeps being mentioned there again and again with positve connotation.</p>
<p>Most recently, Andre Joyal, not the least among category theorists, to put it in an understatement, wrote:</p>
<blockquote>
The n-category caffé is an extraordinary experiment in
research collaboration and dissimination of knowledge.
It maybe the way of the future.
But an old mathematicians like me find it
difficult to adapt to this new form of collaboration.
</blockquote>
<p>He mentions the blog here, but previously he had linked extensively to the lab.</p>
</div>
```

```
Error 504: Element blockquote content does not follow the DTD, expecting (h1 | h2 | h3 | h4 | h5 | h6 | ul | ol | dl | p | div | pre | blockquote | address | hr | table | form | fieldset | ins | del | script | noscript | math | svg:svg)+, got (CDATA)
Line: 5, column: 0
--------------------------------------------
```

]]>
1) Is there a formalization of SEAR anywhere, like for example as a Coq/Agda/Lean library or the like? Just being able to see a fully formalized version & proving the basic theorems would help a lot. As I understand it, full SEAR requires some kind of dependent types in order to express indexed families of sets, and "property" as expressed in the nLab needs some kind of definition?

2) If you remove replacement to get the ETCS-like fragment, can the axioms be expressed purely in first order logic? Or does it still need some form of type theory? What gets lost, other than not being able to formulate products of an arbitrary number of non-isomorphic sets?

3) (possibly trivial but not immediately obvious since I have a hazy understanding of what is allowed by the axioms) In that first order fragment, is it provable that the lattice of relations from A to B is complete, since infinite conjunctions and disjunctions are generally not allowed? ]]>

I’m wondering if there’s been a study of unification and anti-unification of HoTT types? Or even maybe depedent type theory? I’ve looked around but haven’t been able to find a good reference. I’ve found papers on anti-unification for other type systems, such as [1] [2] but not having much luck generalizing them to HoTT.

Unification seems a bit more straightforward, but anti-unification (or least general generalization) of two types has flummoxed me. The problem is in introducing a variable to take the place of two types that are not equivalent and can no longer be split up. For example, take the following two types:

$A :\equiv \Sigma_{x:X} P(x)$

$B :\equiv \Sigma_{x:X} Q(x)$

Our aim in anti-unification is to find a type $C$ that would unify with both $A$ and $B$ by means of variable substitution. If following the algorithm in [1], we’d first recognize that both $A$ and $B$ use the same constructor (of the Sigma type), so we would drill down one level and attempt to anti-unify (or generalize) the two arguments. The first argument is the same for both, so we can copy that straight to $C$. However, the second argument is now an expression which is invoking two different predicates of type $X \rightarrow U$. In a traditional anti-unification algorithm, we would define a new variable that would be substituted with either $P(x)$ or $Q(x)$ when unifying $C$ with $A$ and $B$.

Here however, there seems to be more than one option. Calling this new variable $y$, we could have $y:U$ or $y:X \rightarrow U$. There could even be more options if $P(x)$ and $Q(x)$ weren’t of the same type. Let’s assume $Q: Y \rightarrow U$. Then we could have $y: (X \rightarrow U) + (Y \rightarrow U)$.

Even if making one of these choices, the formulation of $C$ eludes me. Do we write $C :\equiv \Sigma_{x:X} \Sigma_{f: X \rightarrow U} f(x)$, or $C :\equiv \Pi_{f: X \rightarrow U} \Sigma_{x:X} f(x)$, or something else? Any help or direction would be much appreciated!

]]>I see there’s a conference coming up Generalized Cohomology and Physics. EDIT: Link corrected as per #3 (and #5).

]]>I hope that this is the right place to ask a question.

I am trying to understand the hammock localization of a (plain) category with respect to a subcategory. I’ve looked at the original paper by Dwyer and Kan. Given any pair of objects, they define the Hom-set as a simplicial set in which the $k$-simplices are hammocks of width $k$. This defines a simplicial category.

It appears to me that one can always cut a width $k$ hammock into $k$ width $1$ hammocks. In other words a $k$-simplex is a concatenation of $1$-simplices. I think that means that this simplicial space is just the nerve of a category, consisting of the width $0$ and $1$ hammocks.

This implies that the hammock localization doesn’t need to be treated as a simplicial category. It is just a 2-category in disguise.

Is this correct? Is there some reason for preferring the simplicial category description?

Eli

]]>Am not sure if this page exists on the nlab, but I think a nice presentation of this proof technique, would be useful in the development of **“new ways of doing mathematics”**. I would also like to know of other proof techniques in category theory that are useful but happen to be unpopular, maybe a page can be created to handle such? I would appreciate an example that illustrates transformation of a proof in theory A to a proof in theory B(a concept we may have taken for granted? I don’t know). You can view Olivia Caramello’s general idea

We are finalizing an article:

$\,$

$\,$

**Abstract.** *We extend the Chern character on K-theory, in its generalization to the Chern-Dold character on generalized cohomology theories, further to twisted non-abelian cohomology theories, where its target is a non-abelian de Rham cohomology of twisted L-∞ algebra valued differential forms. The construction amounts to leveraging the fundamental theorem of dg-algebraic rational homotopy theory, which we review in streamlined form, to a twisted non-abelian generalization of the de Rham theorem. We show that this non-abelian character reproduces the Chern-Weil homomorphism on non-abelian cohomology in degree 1, represented by principal bundles; and thus generalizes it to higher non-abelian cohomology, represented by higher bundles/higher gerbes. As a fundamental example we discuss the character map on twistorial Cohomotopy theory over 8-manifolds, which is a twisted non-abelian enhancement of the Chern-Dold character on topological modular forms (tmf) in degree 4. This turns out to exhibit a list of subtle topological relations that in high energy physics are thought to govern the charge quantization of fluxes in M-theory.*

$\,$

Comments are welcome. Please grab the latest version of the file from behind the above link.

]]>I think I’m missing something here.

Say we have an equivalence

$A \simeq B$

and a polymorphic predicate:

$P : \Pi_{A:U} A \rightarrow U$

Then should we not expect the following equivalence?

$\Sigma_{a:A} {P (A, a)} \simeq \Sigma_{b:B} {P (B, b)}$

It seems to me like this should be supported through substitute of like for like, but I can’t figure out how to prove this through the language of HoTT, even when using Univalence. Is my thinking correct here or am I missing something?

]]>At last it has happened - Huawei Research collaboration is starting to publish their groundbreaking work on the formalization and theory of deep neural networks and deep learning. https://arxiv.org/abs/2106.14587v1 is the first published preprint (more than 100 pages already) and it references to-be-published preprints and also whole book of papers.

I can handle the theory as a beginner, but this preprint is full of musings and is not formatted in the form of theorems, lemmas and proofs. etc.

So - can we have some discussions about it? Some elaboration? Reformulation?

I have asked the first question in Stackexchange https://math.stackexchange.com/questions/4189699/topos-and-stacks-of-neural-networks-how-to-understand-sentence-values-in-t

But there will be more and more such questions. I hope that preprint will have next versions and I hope to read especailly forthcoming reference: [BBG20] Jean-Claude Belfiore, Daniel Bennequin, and Xavier Giraud. Logical informa-tion cells. Internal technical report, Huawei, 2020.

But DNN theory (especially used for guidance in the selection of DNN architecture and discovery of deep learning algroithms) is so hot topic, that it is impossible to wait.

Actually - this is the moment that Gates and Allen experienced some 40 years ago - trillion$ business opportunity. And huge step for civilization as well, not just in Science.

]]>There are 2 interesting articles this year: https://arxiv.org/abs/2104.03902 - about autodidactive universe that maps old-school gauge theories to old-school neural networks https://arxiv.org/abs/2106.14587 - about utmost generalization of deep neural networks (and their learning and the emergence of semantics in them) in the terms of category theory

Since the time of their appearance I have had the silent dream to make a generalization of “autodidactic universe” to the level of M-theory and topos-stacks preprint may be the right tool to do this. Is this the prospective research theme? Anyone has similar ideas?

This is just shy reminder that this forum still hosts interesting (and still open and ongoing, although without too heavy traffic) discussion about topos and stacks DNN article https://nforum.ncatlab.org/discussion/13133/understanding-preprint-topos-and-stacks-of-deep-neural-networks and that this discussion should be resolved before trying to apply topos-and-stacks-DNN to the M-theory for autodidactic (multi)uni-verse. Of course, more earthly applications are also possible.

]]>Does anyone of any connections that have been made between the notions of cybernetics, autopoeitic systems, or even George Spencer Browns Laws of Form, and homotopy theory or category theory?

I suppose right now such connections might be somewhat tenuous, as the latter is pretty philosophical, and the former is pretty formal, but it seems that there are perhaps connections to be made. Especially, with the notion of the distinctions in space that Spencer-Brown talks about, ideas of homology and homotopy occur to me. Also, possible connections with David Spivak’s ontology logs and various ideas about categorical database type things. I’m also wondering if there are any connections between the aforementioned more philosophical topics and internal logic of topoi, or even topological semantics.

Any references or ideas on this would be really appreciated, it’s just kind of a shot in the dark. Perhaps the question is not well formed.

Best, Jon Beardsley

]]>What are examples of rig categories which

- are not just rigs or ordered rigs, and
- are not distributive monoidal categories (so the sum is not the coproduct)?

I cannot seem to come up with an example myself except very artificial ones (such as taking a distributive monoidal category and removing some arrows). I’m sure there’s quite some though, can anyone help?

]]>I’ve just been re-reading Cassirer’s 1944 paper The concept of group and the theory of perception where he’s bringing together Klein’s Erlanger Program with the findings of the Gestalt school of psychology.

If perception is to be compared to an apparatus at all, the latter must be such as to be capable of “grasping intrinsic necessities.” Such intrinsic necessities are encountered everywhere. It is only with reference to such “intrinsic necessity” that the “transformation” to which we subject a given form is well defined, inasmuch as the transformation is not arbitrary and executed at random but proceeds in accordance with some rule that can be formulated in general terms. (p. 26) (“grasping intrinsic necessities” is due to Max Wertheimer)

He thinks that in mathematics this procedure is taken further right up to group-theoretic invariance, but that its seeds are there in perception.

Interesting that the word ’necessities’ appears, in view of our discussion on necessity as dependent product and base change over $W \to \ast$. Could one say something similar over $B G \to \ast$? I think maybe I’d like to get clearer on the dependent product - homotopy invariants relation.

Or to start with perception, how do we ’know’ that we’re dealing with the same shape in A of this image? We seem to be able to relate 2D projections of a 3D figure subjected to the actions of $E(3)$.

There’s also one’s own motion to consider. True to his neo-Kantian roots Cassirer quotes Bühler

The concept of factors of constancy in the face of variation of both external and internal conditions of perception is the realization, in modern form, of that which in principle…was known to Kant, the analyst, and which he stated in terms of mediating schemata.

Perceptual images of objects are products of the imagination. Productive imagination is necessary for objective determination.

I wonder what of all this can be given the HoTT treatment.

]]>Is there a bug in the handling of theorem numbering? The last paragraph of this page refers to "Theorem 3" but it should really be "Theorem 6."

]]>Elsewhere we proven that all fundamental weight systems are quantum states. Now we want to find the decomposition of these quantum states as mixtures of pure states and compute the resulting probability distribution.

Specifically, I suppose the pure states in the mixture are labelled by Young diagrams, and so we should get a god-given probability distribution on the set of Young diagrams (of $n$ boxes for the fundamental $\mathfrak{gl}(n)$-weight system). It’s bound to be something classical (probably the normalized numbers of some sort of Young tableaux) but it will still be interesting to know that this classical notion is in fact the probability distribution secretly encoded by fundamental weight systems.

I had started to sketch out how to approach this over here in the thread on the Cayley distance kernel. Now I’d like to flesh this out.

The broad strategy is to first consider the group algebra $\mathbb{C}[Sym(n)]$ as the star-algebra of observables, the Cayley distance kernel in the form $\big(e, [e^{- \beta \cdot d_C}] \cdot (-) \big)$ as a state on this algebra, and then find its convex combination into pure states using representation theory.

Once this is done, the result for the actual weight systems on the algebra of horizontal chord diagram should follow immediately by pullback along $perm : \mathcal{A}^{pb}_n \longrightarrow \mathbb{C}[Sym(n)]$.

It seems straightforward to get a convex decomposition of the fundamental-weight-system quantum state into “purer states” this way. I am still not sure how to formally prove that the evident purer-states are already pure, but that will probably reveal itself in due time.

Eventually this should go to its own entry. For the moment I started making unpolished notes in the *Sandbox*.

Is there a sensible category theoretic account of this monad transformer construction? Also here.

Better start an entry in case someone has thoughts: monad transformer.

]]>I am interested in Urs Schreiber’s work like “Differential cohomology in a cohesive infinity-topos”. But to study these huge works is a long-term project, I think is a good idea to study together. I recently joined one like that for Exodromy. It’s pretty nice, I learn a lot of higher topos from this. So I think we can have more like this.

Maybe some experts can give a “road map”, and learners can give talks on Zoom each week according to those materials. One benefit of holding online is it can last for a long period(year-long) so that we can have time to work on some pre-required things. And such a working group could encourage people to insistent study on this.

]]>With David Corfield and Hisham Sati we are finalizing an article:

$\,$

$\,$

The title refers to a proof presented, that all fundamental gl(n)-weight systems on horizontal chord diagrams are states with respect to the star-involution of reversion of strands.

But the bulk of the article rephrases this theorem and its proof as a special case of a more general statement in geometric group theory: characterizing the (non/semi-)positive definite phases of the Cayley distance kernel on the symmetric group.

Finally, a last section recalls from Sati, Schreiber 2019c the original motivation and interpretation of this result: Under Hypothesis H it proves, from first principles, that a pair of coincident M5-branes (transversal on a pp-wave background, as in the BMN matrix model) indeed do form a (bound) state. This is of course generally expected, but there did not use to be a theory to derive this from first principles.

$\,$

Comments are welcome. If you do take a look, please grab the latest version of the file from behind the above link.

]]>At *computational trilogy* I made explicit the quantum version – here.

As with the classical trilogy, it’s evident once you think about it.

]]>My calculus book uses many different notations for the derivative of $y = f(x)$ with respect to $x$, such as

$\frac{dy}{dx} \quad y'\quad f'(x) \quad D f(x) \quad \frac{df}{dx}$Recently I’ve found that I kind of object to a couple of these. For instance, consider $\frac{df}{dx}$. One of the things I try to teach my students is that when we define a function $f$ by writing $f(x) = x^2$, say, the variable $x$ is a dummy variable; if we wrote $f(t) = t^2$ we would be defining the same function, namely the one which squares its input. But if “$f$” denotes a function of this (usual mathematical) sort, then how can we write $\frac{df}{dx}$ to mean its derivative, since $f$ doesn’t know that we called its input variable $x$?

Notations like $f'(x)$ and $D f (x)$ don’t have this problem, because $f'$ and $D f$ denote the derivative function of $f$, which assigns to each input value the derivative of $f$ at that value, and so $f'(x)$ and $D f (x)$ just mean evaluation of this function at that value. I suppose we could interpret $\frac{df}{dx}$ similarly if we regarded “$\frac{df}{d}$” as the derivative function of $f$, which we evaluate at something by placing it after the $d$ in the denominator, but this seems strained, and would suggest even odder notations such as writing $\frac{df}{d3}$ for $f'(3)$.

It was pointed out to me that this kind of notation is even commoner in multivariable calculus, where we write things like $\frac{\partial f}{\partial x}$ and $\frac{\partial f}{\partial y}$, and in this case there aren’t good alternatives available, since we have to indicate somehow whether it is the first or second input variable of $f$ with respect to which we take the derivative.

From a differential-geometric viewpoint, one answer is to say that $x$ denotes a standard coordinate function on the 1-dimensional manifold that is the domain of $f$, and so we are actually taking the derivative with respect to a vector field associated to that function. We can even regard $\frac{df}{dx}$ as a literal quotient of differential 1-forms, since 1-forms on a 1-manifold are a 1-dimensional vector space at each point, so the quotient of two of them is a real number. But while logically consistent, this seems to undercut the force of the lesson of dummy variables, since we are endowing $x$ with a special status not shared by $t$.

Using $x$ to denote the coordinate function has the other interesting consequence that it makes it okay to say “the function $x^2+1$” (since we can multiply and add functions together), instead of insisting on saying “the function $f$ defined by $f(x) = x^2+1$”. Again this feels like it undercuts the lesson of what a function is — and yet I find that it’s hard to teach a calculus class without eventually slipping into saying “the function $x^2+1$”. With $x$ as a function we can also write “$f = x^2+1$”, which again is something that I’m used to indoctrinating my students against.

I also have a problem with the notation $y'$, for a more pragmatic reason. Suppose we want to take the derivative of $y = (3x+1)^4$ using the chain rule. A nice way to do it is to make a substitution $u = 3x+1$, so that $y = u^4$, and then use differentials:

$du = 3 dx$ $dy = 4u^3 du = 4(3x+1)^3(2 dx)$ $\frac{dy}{dx}= 8(3x+1)^3$The problem here is that the notation $y'$ doesn’t indicate what variable we differentiate with respect to, and in this calculation we have two derivatives of $y$, namely $\frac{dy}{dx} = 8(3x+1)^3$ and $\frac{dy}{du}=4u^3$, which are not equal even after substituting the value of $u = 3x+1$. Here the solution seems to be straightforward: just don’t write $y'$. But if we can write $f = x^2+1$ just like $y = x^2+1$, and if we allow the notation $f'(x) = 2x$ and hence also $f' = 2x$, then we should just as well have $y' = 2x$.

Does anyone have a good solution? I feel like at least part of the problem comes from confusing $\mathbb{R}$ as the real numbers with $\mathbb{R}$ as a 1-dimensional manifold, but I haven’t exactly managed to pin down yet how to solve it from that point of view.

]]>Since it touches on several of the threads that we happen to have here, hopefully I may be excused for making this somewhat selfish post here.

For various reasons I need to finally upload my notes on “differential cohomology in a cohesive ∞-topos” to the arXiv. Soon. Maybe by next week or so.

It’s not fully finalized, clearly, I could spend ages further polishing this – but then it will probably never be fully finalized, as so many other things.

Anyway, in case anyone here might enjoy eyeballing pieces of it (again), I am keeping the latest version here

]]>Hello there, am an independent researcher interested in foundations of mathematics though without comprehensive mathematical background. Last year, it caught my attention that physics is formalized in richer kinds of homotopy theory in Science_Of_Logic. There is mention of universal algebra but they choose to work in a kind of synthetic homotopy theory but in my view continuing in universal algebra is more generic and could actually lead to a foundation of math. My math is bad but there could be some truth :

- A unity of opposites is between EM category on a monad and EM category on a comonad. It is subsumed by the ambient category via bireflection
- The bireflection has kleisli lifting as left adjoint inclusion and eilenberg-moore lifting as right adjoint inclusion(a crucial step yet am not so sure)
- The tower of adjoint modalities extends(by monadic decomposition) to any arbitrary ordinal as compared to the one on nlab which I believe is of length 12.
- A foremost assumption of mine is that any tower is equivalent to a fully faithful functor from kleisli category to eilenbergmoore category and that it is an equivalence( at least it is without overly-restrictive conditions). Also, dont forget it is still a tower of unity of opposites
- This now forms a 2-category with adjunctions as 0-cells, a square of adjunctions as 1-cell and transformations as 2-cells. The adjunctions in it are all tripple adjoints.
In my view, this should be formalized in enriched category theory so that every category turns out to be such a tower. The truth of this may be predicted using the idea that enriched categories are just free (co)completions and as such they are equivalent to eilenbergmoore categories, leading to my final step. 7.The 2-category above can be viewed as the category of all categories. The importance of this approach is that universal algebra is equivalent to inductive/recursive types and we can take advantage of this to inductively/recursively define the whole of mathematics and prove all its theorems in a big-bang kind of manner.

As a remark, I observe how bireflection seems to be equivalent to the physical notion of time, as defined in the nlab page, causal locality. This gives me the impression that math is inherently dynamic, that math actually exists objectively. Either way, what prevents a mathemetical theory from being real except causality ? I posted a related question on MathOverflow has there been any serious attempt at a circular foundation of mathematics. I at-least expect that the Hegelian pseudo-code can be formalized on such lines. I would appreciate it if some more advanced mathematician embarks on this or

**corrects me**. Thank you