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.
stub for quantum computation
I created a stub certified programming.
That’s motivated from me having expanded the Idea-section at type theory. I enjoyed writing the words “is used in industry”. There are not many Lab pages where I can write these words.
I am saying this only half-jokingly. Somehow there is something deep going on.
Anyway, in (the maybe unlikely) case that somebody reading this here has lots of information about the use and relevance of certified programming in industry, I’d enjoy seeing more information added to that entry.
Since it came up in another thread, I’ve made reverse mathematics slightly less stubby. I included some notes on constructive reverse mathematics, but perhaps it should have its own page.
brief entry nilpotence theorem
(in chromatic homotopy theory, maybe needs disambiguation later…)
now I have finally the time to come back to this, as announced, and so I am now starting an entry:
relation between type theory and category theory .
So far there is just some literature collected. I now plan to extract the essence of Seely’s artice into the entry in some technical detail.
added pointer to:
am giving unimath.github.io/SymmetryBook/book.pdf a category:reference
-entry
brief note: Sierpinski topos
copied over the homotopy-theoretic references from modal type theory to here.
Added disambiguation link to poly-morphism.
I have created an entry type of types. Wanted to collect some literature there, but ended up not finding too much…
I have worked a bit on contractible type. Apart from beautifying it a bit (or so I hope I did) I have added in the section Categorical semantics a fair bit of pedestrian detail on how to see that a term of is indeed a contraction right homotopy, and vice versa.
The term “discrete mathematics”, as it is actually used in the literature, appears to be synonymous with combinatorics.
Its use appears to be limited mostly to introductory textbooks on combinatorics.
I suggest that this article reflects the actual use of this term, and, in particular, does not claim that (∞,1)-toposes are part of discrete mathematics, as it currently does.
Do we really need a separate article here, or should this be merged into combinatorics, with a section on terminology there?
added pointer to today’s
added statement of existence of linear extensions (here)
Will give this its own entry at linear extension of a partial order, for ease of referencing
created homotopy level
However, the instiki-table does not come out correctly yet. It did before I added the third column. These tables are the most delicate things. I never know why sometimes they display correctly and sometimes not.
brief category: people
-entry, for the moment just to attribute the naming at Betti number
added missing publication data to some references, and added this new reference:
This is the list from proof assistant – Examples, and was (incompleteky) copied by hand into related entries, but we should make it (as done hereby) a standalone to be !include
ed under “Related concepts” in relevant entries
All I did in editing was to group the proof assistants into “based on type/set theory” and “applicable to homotopy type theory”. Experts please hit “edit” and improve on it
the entry that used to be titled quantum mechanics in terms of dagger-compact categories I have renamed into finite quantum mechanics in terms of dagger-compact categories (with a “finite” up front) and I have added to the first sentence the qualifier “finite” and “finite-dimensional” a bunch of times.
I am currently at “Quantum Physics and Logic 2012” in Brussels, and every second speaker advertizes the formalism of what they call “categorical quantum theory”. It’s all fine for the majority of the audience which is all into quantum information theory, where one is only interested in shuffling a finite bunch of qbits around, but it is rather misleading from an ordinary perspective on quantum physics. Already the particle on the line is not a finite quantum system.
I have split-off Feynman diagram from perturbation theory, gave it a brief Idea-section and added a pointer to an insightful reference.
created spectral triple, but so far a bit bizarre:
I give an unorthodox category-theoretic VAGUE definition, which I have reason to think is the right one
and then I record an unusual reference on vonNeumann spectral triple (just because at MO somebody asked for this and I don't like to dig out a link just to throw it away after one reference use like a paper napkin )
commented list of some background references for today’s
Edit to: GUT by Urs Schreiber at 2018-04-01 01:21:13 UTC.
Author comments:
added pointer to textbook account
I have touched a bunch of the entries related to the Erlangen program, trying to polish a bit, adding more cross links and more references.
(This includes the entries stabilizer group, coset, Klein geometry, Cartan geometry and maybe more.)
Added to Klein geometry a section History with quotations for where exactly Klein actually speaks about .
(This key passages is a bit hidden in Klein’s text, appearing at a somewhat unexpected point somewhere in the middle of a 35 page document.)