Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
After this discussion at string diagrams for linearly distributive categories with unit = counit, I finally got round to having a go at making star-polycategory. Still much more to do. Hopefully I didn’t make any major mistakes so far.
we were lacking an entry realizability that points to all the related entries (and in fact some entries were asking for just “realizability”).
So I started one. Put in the following Idea-paragraph:
The idea of realizability is essentially that of constructivism, intuitionistic mathematics and the propositions as types paradigm: for instance constructively a proof of an existential quantification ∃x∈Xϕ(x) consists of constructing a specific x∈X and a proof of ϕ(x), which “realizes” the truth of the statement, whence the name (e.g. Vermeeren 09, section 1).
Clean up a couple parenthetical remarks. The page ring object seems to indeed have the desired diagrams.
a stub, just to finally make the link work (which has been requested for ages at inhabited set, dominance and inhabited object)
I have made some trivial edits to the wording, hoping to make it flow more nicely.
By the way, this entry is linking (at least now that I adjusted the plural redirect) to recursive function. This is only natural, but – unfortunately – our entry recursive function is empty (and always has been)!
Much of the material needed there is at partial recursive function. We should either put redirects or (better) add a little bit of content to recursive function.
I have added (here) pointer to:
(This edit prompted by discussion in another thread of the same name: here)
I was going to start game semantics to record a couple of references to dependent type theory, but I’m getting an error message at the moment. So I’ll just leave here for now:
In logic, game semantics is used to provide a semantic interpretation of logic constructions in terms of strategies for opposing players to win a game corresponding to some proposition.
For attempts to formulate a game semantics for dependent type theory, see
Matthijs Vakar, Radha Jagadeesan, Samson Abramsky, Game Semantics for Dependent Types, (pdf)
Norihiro Yamada, _Game Semantics for Martin-Löf Type Theory, (arXiv:1610.01669)
Created complete small category, and moved the proof of Freyd’s theorem to there from adjoint functor theorem.
Edited the text in the Idea-section, such as to make the terms monoidal category, monoid objects, module objects appear.
I have added the following paragraph to calculus of constructions, I’d be grateful if experts could briefly give me a sanity check that this is an accurate characterization:
More in detail, the Calculus of (co)Inductive Constructions is
a system of natural deduction with dependent types;
with the natural-deduction rules for dependent product types specified;
and with a rule for how to introduce new such natural-deduction rules for arbitrary (co)inductive types.
and with a type of types (hierarchy).
I fixed a strange link at John Power.
Expanded the entry by more references.
I have erased two redirects which used to be (probably) in Greek but some nLab upgrade has obliterated the difference between the characters and now it was ????? or alike and the info is lost. If somebody has his Greek spelling can ressurect the redirects. I have now changed the page name to his arXiv spelling and put Ioannis Vlassopoulos as a redirect.
a stub entry, for the moment just so as to give a home to these two references:
Hiroshi Kihara, Model category of diffeological spaces, Journal of Homotopy and Related Structures, (2018), 1-40 (arXiv:1605.06794)
Tadayuki Haraguchi, Kazuhisa Shimakawa, A model structure on the category of diffeological spaces (arXiv:1311.5668)
added pointer to:
added this second-order-quote:
Chen Ning Yang writes in C. N. Yang, Selected papers, 1945-1980, with commentary, W. H. Freeman and Company, San Francisco, 1983, on p. 567:
In 1975, impressed with the fact that gauge fields are connections on fiber bundles, I drove to the house of S. S. Chern in El Cerrito, near Berkeley… I said I found it amazing that gauge theory are exactly connections on fiber bundles, which the mathematicians developed without reference to the physical world. I added: “this is both thrilling and puzzling, since you mathematicians dreamed up these concepts out of nowhere.” He immediately protested: “No, no. These concepts were not dreamed up. They were natural and real.”
added pointer to this article on the arXiv today:
A hint for a relation to tmf, vaguely in line with the lift of the Witten genus to the string orientation of tmf:
added pointer to today’s
added this pointer:
gave 2d TQFT a slightly more informative Idea-section, highlighting the difference between the classical strict case classified by Frobenius algebras and the local/extended non-compact case classified by Calabi-Yau objects.
Added a reference by Abrams as a candidate for a first rigourous proof of the classification result via Frobenius algebras, and added citations for the local case (copied over from TCFT).
added pointer to today’s
added these pointers
Discussion of quantum anomaly cancellation and 7d Horava-Witten theory is in
{#GherghettaKehagias02} Tony Gherghetta, Alex Kehagias, Anomaly Cancellation in Seven-Dimensional Supergravity with a Boundary, Phys.Rev. D68 (2003), 065019, (arXiv:hep-th/0212060)
Spyros D. Avramis, Alex Kehagias, _Gauged D=7 Supergravity on the S1/ℤ2 Orbifold (arXiv:hep-th/0407221)
T.G. Pugh, Ergin Sezgin, Kellogg Stelle, D=7 / D=6 Heterotic Supergravity with Gauged R-Symmetry (arXiv:1008.0726)
Added pointer to today’s
Guillaume Bossard, Franz Ciceri, Gianluca Inverso, Axel Kleinschmidt, Maximal D=2 supergravities from higher dimensions [arXiv:2309.07232]
Guillaume Bossard, Franz Ciceri, Gianluca Inverso, Axel Kleinschmidt, Consistent truncation of eleven-dimensional supergravity on S8×S1 [arXiv:2309.07233]
I finally realized that this ought to exist. And sure enough, it had been constructed already: the 4d supergravity Lie 2-algebra-extension of the 4d N=2 super-Poincaré super-Lie algebra. I have added a minimum of an Idea-section and pointers to the references.
Minimal stub requested by links at reproducing kernel Hilbert space and few other entries.
a stub (though I did try my hand on a brief idea-section), for the moment mostly to provide a home for
stub for iterated integral (more references as soon as the nLab wakes up again…)
quick note for 5-dimensional Chern-Simons theory, for the moment just to record some references
added pointer to André Henriques’ recent MO comment here to quantization of 3d Chern-Simons theory. Should try to find time to work that into the entry.
gave 11d Chern-Simons theory its own (brief, for the moment) entry (splitting off some material from self-dual higher gauge theory)
Added a fair bit of content to 7d Chern-Simons theory.
Of the three examples discussed there, the first two are review. The third is inspired by something I have been talking about with D. Fiorenza, C. Rogers and H. Sati.
Changed title and links to different convention, see discussion here. (Unified redirects among articles about Chern-Simons theory in a particular dimension. There are now four for every artile “D=n Chern-Simons theories”, “nd Chern-Simons theory”, “nd Chern-Simons theories”, “n-dimensional Chern-Simons theory” and “n-dimensional Chern-Simons theories”.)
started adding these kinds of references, but maybe this should eventually go in its own stand-alone entry:
A kind of 4d Chern-Simons theory intermediated between ordinary 3d Chern-Simons theory and compled 3d (hence real 6d) holomorphic Chern-Simons theory:
Kevin Costello, Edward Witten, Masahito Yamazaki, Gauge Theory and Integrability, II, ICCM Not. 6, 120-146 (2018) (arXiv:1802.01579)
Kevin Costello, Edward Witten, Masahito Yamazaki, Gauge Theory and Integrability, I, ICCM Not. 6, 46-119 (2018) (arXiv:1709.09993)
Meer Ashwinkumar, Meng-Chwan Tan, Qin Zhao, Branes and Categorifying Integrable Lattice Models (arXiv:1806.02821)
Changed title and links to different convention, see discussion here. (Unified redirects among articles about Chern-Simons theory in a particular dimension. There are now four for every artile “D=n Chern-Simons theories”, “nd Chern-Simons theory”, “nd Chern-Simons theories”, “n-dimensional Chern-Simons theory” and “n-dimensional Chern-Simons theories”)
Changed title and links to different convention, see discussion here. (Unified redirects among articles about Chern-Simons theory in a particular dimension. There are now four for every artile “D=n Chern-Simons theories”, “nd Chern-Simons theory”, “nd Chern-Simons theories”, “n-dimensional Chern-Simons theory” and “n-dimensional Chern-Simons theories”)
Added to fix a dead link.