Not signed in (Sign In)

A discussion forum about contributions to the nLab wiki and related areas of mathematics, physics, and philosophy.

Want to take part in these discussions? Sign in if you have an account, or apply for one below

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

- Discussion Type
- discussion topicregular language
- Category Latest Changes
- Started by alexis.toumi
- Comments 5
- Last comment by Urs
- Last Active Nov 13th 2022

- Discussion Type
- discussion topicco-unitality
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 13th 2022

- Discussion Type
- discussion topicno-cloning theorem
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by Urs
- Last Active Nov 13th 2022

created a stub for

*no-cloning theorem*.For the moment what I wanted to highlight is that under the identification of linear logic as quantum logic it is this theorem which is the “linearity” of the logic.

- Discussion Type
- discussion topicaction monad
- Category Latest Changes
- Started by PaoloPerrone
- Comments 11
- Last comment by Urs
- Last Active Nov 13th 2022

- Discussion Type
- discussion topicBrouwer's fixed point theorem
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by Urs
- Last Active Nov 13th 2022

added pointer to

- B. A. Dubrovin, S. P. Novikov, A. T. Fomenko, corollary 15.3.4 of
*Modern Geometry — Methods and Applications: Part II: The Geometry and Topology of Manifolds*, Graduate Texts in Mathematics 104, Springer-Verlag New York, 1985

- B. A. Dubrovin, S. P. Novikov, A. T. Fomenko, corollary 15.3.4 of

- Discussion Type
- discussion topicaxiom of replacement
- Category Latest Changes
- Started by TobyBartels
- Comments 9
- Last comment by Urs
- Last Active Nov 13th 2022

- Discussion Type
- discussion topicproper subset
- Category Latest Changes
- Started by nLab edit announcer
- Comments 2
- Last comment by nLab edit announcer
- Last Active Nov 13th 2022

added section on definitions in structural set theories, and added links to subset and improper subset

Anonymous

- Discussion Type
- discussion topicimproper subset
- Category Latest Changes
- Started by nLab edit announcer
- Comments 1
- Last comment by nLab edit announcer
- Last Active Nov 13th 2022

- Discussion Type
- discussion topicwell-pointed topos
- Category Latest Changes
- Started by Urs
- Comments 10
- Last comment by nLab edit announcer
- Last Active Nov 13th 2022

Added an "Examples"-section to well-pointed topos and to Boolean topos mentioning Set and models for ETCS.

- Discussion Type
- discussion topicaxiom schema
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by nLab edit announcer
- Last Active Nov 12th 2022

- Discussion Type
- discussion topicaxiom of foundation
- Category Latest Changes
- Started by Mike Shulman
- Comments 4
- Last comment by nLab edit announcer
- Last Active Nov 12th 2022

Three questions at axiom of foundation.

- Discussion Type
- discussion topicquantum measurement
- Category Latest Changes
- Started by Urs
- Comments 16
- Last comment by Urs
- Last Active Nov 12th 2022

created a currently fairly empty entry

*quantum measurement*, just so as to have a place where to give a commented pointer to the article- Klaas Landsman, Robin Reuvers,
*A Flea on Schrödinger’s Cat*, Found. Phys. 43, 373-407 (2013) (arXiv:1210.2353)

- Klaas Landsman, Robin Reuvers,

- Discussion Type
- discussion topicEric Oliver Paquette
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 12th 2022

- Discussion Type
- discussion topiccomposite system
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 12th 2022

added a sentence on entanglement and this historical reference:

- Erwin Schrödinger,
*Discussion of Probability Relations between Separated Systems*, Mathematical Proceedings of the Cambridge Philosophical Society,**31**4 (1935) 555-563 [doi:10.1017/S0305004100013554]

- Erwin Schrödinger,

- Discussion Type
- discussion topicaxiom of materialization
- Category Latest Changes
- Started by Mike Shulman
- Comments 3
- Last comment by nLab edit announcer
- Last Active Nov 12th 2022

- Discussion Type
- discussion topicMostowski's collapsing lemma
- Category Latest Changes
- Started by nLab edit announcer
- Comments 2
- Last comment by nLab edit announcer
- Last Active Nov 12th 2022

- Discussion Type
- discussion topicMostowski set theory
- Category Latest Changes
- Started by nLab edit announcer
- Comments 2
- Last comment by nLab edit announcer
- Last Active Nov 12th 2022

starting article on Mostowski set theory, which Mike Shulman proved in

- Michael Shulman (2018). Comparing material and structural set theories. arXiv:1808.05204.

to be equivalent in strength to ETCS

Anonymous

- Discussion Type
- discussion topicqudit
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 12th 2022

- Discussion Type
- discussion topicqbit
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Urs
- Last Active Nov 12th 2022

added the original reference for the term

*q-bit*:- Benjamin Schumacher,
*Quantum coding*, Phys. Rev. A**51**(1995) 2738 $[$doi:10.1103/PhysRevA.51.2738$]$

- Benjamin Schumacher,

- Discussion Type
- discussion topicQWIRE
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by Urs
- Last Active Nov 12th 2022

one more in the list of quantum programming languages

- Discussion Type
- discussion topicCoq
- Category Latest Changes
- Started by Urs
- Comments 15
- Last comment by Urs
- Last Active Nov 12th 2022

I have been trying to collect some information at Coq.

- Discussion Type
- discussion topicCoqQ
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 12th 2022

a stub enty, for the moment just to give a home to:

- Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying,
*CoqQ: Foundational Verification of Quantum Programs*[arXiv:2207.11350]

- Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying,

- Discussion Type
- discussion topicdomain specific embedded programming language
- Category Latest Changes
- Started by Urs
- Comments 9
- Last comment by Urs
- Last Active Nov 12th 2022

Roux Cody kindly alerted me of the fact that analog of synthetic mathematics under “computational trinitarianism” in programming theory is that of

*domain specific embedded programming languages*. To record this neat insight I have now created a minimum entry on the latter and cross-linked a bit.

- Discussion Type
- discussion topicMingsheng Ying
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 12th 2022

- Discussion Type
- discussion topiccertified programming
- Category Latest Changes
- Started by Urs
- Comments 28
- Last comment by Urs
- Last Active Nov 12th 2022

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 $n$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.

- Discussion Type
- discussion topicexcluded middle
- Category Latest Changes
- Started by Mike Shulman
- Comments 11
- Last comment by Urs
- Last Active Nov 12th 2022

I added to excluded middle a discussion of the constructive proof of double-negated LEM and how it is a sort of “continuation-passing” transform.

- Discussion Type
- discussion topicsharp modality
- Category Latest Changes
- Started by nLab edit announcer
- Comments 3
- Last comment by Urs
- Last Active Nov 12th 2022

- Discussion Type
- discussion topicJ-B Vienney
- Category Latest Changes
- Started by J-B Vienney
- Comments 3
- Last comment by J-B Vienney
- Last Active Nov 11th 2022

- Discussion Type
- discussion topic!-modality
- Category Latest Changes
- Started by Urs
- Comments 27
- Last comment by J-B Vienney
- Last Active Nov 11th 2022

collected some references on the interpretation of the !-modality as the Fock space construction at

*!-modality*.Cross-linked briefly with he stub entries_Fock space_ and

*second quantization*.

- Discussion Type
- discussion topicKruna S. Ratkovic
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 11th 2022

- Discussion Type
- discussion topicsuspension spectrum
- Category Latest Changes
- Started by Urs
- Comments 7
- Last comment by Urs
- Last Active Nov 11th 2022

stub for suspension spectrum

- Discussion Type
- discussion topicstabilization
- Category Latest Changes
- Started by Urs
- Comments 13
- Last comment by Urs
- Last Active Nov 11th 2022

started entry on stabilization (in the sense of sending an (oo,1)-category to its free stable (infinity,1)-category)

I want to eventually state more properties of the effect of stabilization on objects here.

- Discussion Type
- discussion topicAleks Kissinger
- Category Latest Changes
- Started by nLab edit announcer
- Comments 3
- Last comment by Urs
- Last Active Nov 11th 2022

adding reference

- Krzysztof Bar, Aleks Kissinger, Jamie Vicary.
*Globular: an online proof assistant for higher-dimensional rewriting*, Logical Methods in Computer Science, January 22, 2018, Volume 14, Issue 1 - (doi:10.23638/LMCS-14(1:8)2018, arXiv:1612.01093)

Anonymous

- Krzysztof Bar, Aleks Kissinger, Jamie Vicary.

- Discussion Type
- discussion topicGlobular
- Category Latest Changes
- Started by Urs
- Comments 90
- Last comment by Urs
- Last Active Nov 11th 2022

Jamie Vicary is kindly adding information to the $n$Lab on the higher-category-theory-proof-assistant that he and collaborators are developing, at:

I have added a few more hyperlinks to related nLab entries.

And I have changed the page name from lower case “globular” to upper case “Globular” to fit our conventions on entry titles.

Currently, lower case “globular” still redirects to the entry. But if anyone has links to the lower case version from elsewhere, please consider changing them, for eventually the lower case “globular” really ought to go to a page that disambiguates all sorts of globular-related entries on the nLab, such as

*globe*and*globular set*, etc.

- Discussion Type
- discussion topicJamie Vicary
- Category Latest Changes
- Started by nLab edit announcer
- Comments 2
- Last comment by Urs
- Last Active Nov 11th 2022

adding reference

- Krzysztof Bar, Aleks Kissinger, Jamie Vicary.
*Globular: an online proof assistant for higher-dimensional rewriting*, Logical Methods in Computer Science, January 22, 2018, Volume 14, Issue 1 - (doi:10.23638/LMCS-14(1:8)2018, arXiv:1612.01093)

Anonymous

- Krzysztof Bar, Aleks Kissinger, Jamie Vicary.

- Discussion Type
- discussion topicZFC
- Category Latest Changes
- Started by TobyBartels
- Comments 15
- Last comment by nLab edit announcer
- Last Active Nov 11th 2022

- Discussion Type
- discussion topicMartin-Löf dependent type theory
- Category Latest Changes
- Started by Zhen Lin
- Comments 31
- Last comment by nLab edit announcer
- Last Active Nov 11th 2022

I started an article about Martin-Löf dependent type theory. I hope there aren't any major mistakes!

One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?

- Discussion Type
- discussion topicKrzysztof Bar
- Category Latest Changes
- Started by nLab edit announcer
- Comments 1
- Last comment by nLab edit announcer
- Last Active Nov 11th 2022

starting page for category:people reference and to put the source

- Krzysztof Bar, Aleks Kissinger, Jamie Vicary.
*Globular: an online proof assistant for higher-dimensional rewriting*, Logical Methods in Computer Science, January 22, 2018, Volume 14, Issue 1 - (doi:10.23638/LMCS-14(1:8)2018, arXiv:1612.01093)

Anonymous

- Krzysztof Bar, Aleks Kissinger, Jamie Vicary.

- Discussion Type
- discussion topicZorn's lemma
- Category Latest Changes
- Started by Urs
- Comments 5
- Last comment by zskoda
- Last Active Nov 10th 2022

I found the organization at

*Zorn’s lemma*a bit rough, so I have tried to smoothen it out a bitFor instance

at one point it had suddenly said “proof of the converse” without a clear statement of the other direction having appeared before. I have created two Theorem-environments and tried to make the statements clearer.

the Idea-section had started out saying that “Zorn’s lemma is a trick”. I think that’s misleading or at least misses the important nature of the thing, so I rewrote that and expanded a bit.

But the foundationalists among you please check!

- Discussion Type
- discussion topicpotentiality and actuality
- Category Latest Changes
- Started by Urs
- Comments 30
- Last comment by David_Corfield
- Last Active Nov 10th 2022

starting something, to go alongside

*necessity and possibility*(will adjust page name in a second)

not much here yet, though, under construction

- Discussion Type
- discussion topicGavin Bierman
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 10th 2022

- Discussion Type
- discussion topicmusic theory
- Category Latest Changes
- Started by nLab edit announcer
- Comments 2
- Last comment by John Baez
- Last Active Nov 10th 2022

- Discussion Type
- discussion topicstring theory results applied elsewhere
- Category Latest Changes
- Started by Urs
- Comments 13
- Last comment by David_Corfield
- Last Active Nov 10th 2022

Reading the blog entry

- Matthew Strassler,
*From string theory to the large hadron collider*(blog post)

and the reactions to it made me realize that apparently there is no comprehensive list either in print or online of all the insights into QFT in general and observed standard model physics in particular, that have been obtained via results in string theory.

So I have entertained myself with starting to collect notes for such a list:

In the process I have created a bunch of new entries, most of them stubs, linked to from there.

- Matthew Strassler,

- Discussion Type
- discussion topicnecessity and possibility
- Category Latest Changes
- Started by Urs
- Comments 199
- Last comment by Urs
- Last Active Nov 10th 2022

I have given

*necessity*and*possibility*(which used to redirect to*S4-modal logc*) an entry of their own.The entry presently

first recalls the usual axioms;

then complains that these are arguably necessary but not sufficient to characterize the idea of necessity/possibility;

and then points out that if one passes from propositional logic to first-order logic (hyperdoctrines) and/or to dependent type theory, then there is a way to axiomatize modalities that actually have the correct interpretation, namely by forming the reflection (co)monads of $\exists$ and $\forall$, respectively.

You may possibly complain, but not necessarily. Give it a thought. I was upset about the state of affairs of the insufficient axiomatics considered in modal logic for a long time, and this is my attempt to make my peace with it.

- Discussion Type
- discussion topicparallel computing
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 10th 2022

- Discussion Type
- discussion topicquantum parallelism
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 10th 2022

- Discussion Type
- discussion topicJean-Michel Raimond
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 10th 2022

- Discussion Type
- discussion topicSerge Haroche
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 10th 2022

- Discussion Type
- discussion topicEPR paradox
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by Urs
- Last Active Nov 10th 2022

David Corfield and I came to start something at

*EPR paradox*

- Discussion Type
- discussion topicGrover's algorithm
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by Urs
- Last Active Nov 10th 2022

stub entry, for the moment I just needed a place to record this discussion in terms of finite quantum mechanics in terms of dagger-compact categories:

- Jamie Vicary, Section 3 of:
*The Topology of Quantum Algorithms*, (LICS 2013) Proceedings of 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 93-102 (arXiv:1209.3917)

Review in:

- Ali Nabi Duman,
*The Topology of Grover Algorithm*(arXiv:1405.4425)

- Jamie Vicary, Section 3 of:

- Discussion Type
- discussion topichomotopy type theory
- Category Latest Changes
- Started by Urs
- Comments 66
- Last comment by nLab edit announcer
- Last Active Nov 9th 2022

stub for homotopy type theory

- Discussion Type
- discussion topicNullstellensatz
- Category Latest Changes
- Started by Urs
- Comments 25
- Last comment by Urs
- Last Active Nov 9th 2022

wrote something at

*Nullstellensatz*, prompted by this old MO comment by Lawvere.

- Discussion Type
- discussion topicEdward MacKinnon
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 9th 2022

- Discussion Type
- discussion topicinterpretation of quantum mechanics
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 9th 2022

added pointer to:

- Edward MacKinnon,
*Interpreting Physics – Language and the Classical/QuantumDivide*, Springer (2012) [doi:10.1007/978-94-007-2369-6]

(I was looking for references which one might point to concerning the term “quantum/classical divide”. For instance, who actually introduced that specific term? People use it to refer to Bohr’s writings, but Bohr never wrote down the specific words “quantum/classical divide”, did he?)

- Edward MacKinnon,

- Discussion Type
- discussion topicbook HoTT
- Category Latest Changes
- Started by nLab edit announcer
- Comments 1
- Last comment by nLab edit announcer
- Last Active Nov 9th 2022

- Discussion Type
- discussion topicpropositional equality
- Category Latest Changes
- Started by nLab edit announcer
- Comments 5
- Last comment by nLab edit announcer
- Last Active Nov 9th 2022

starting page on propositional equality, to contrast with judgmental equality and typal equality (the latter which redirects to identity type)

Anonymous

- Discussion Type
- discussion topictyped predicate logic
- Category Latest Changes
- Started by nLab edit announcer
- Comments 1
- Last comment by nLab edit announcer
- Last Active Nov 9th 2022

- Discussion Type
- discussion topiclayered type theory
- Category Latest Changes
- Started by nLab edit announcer
- Comments 1
- Last comment by nLab edit announcer
- Last Active Nov 9th 2022

starting article based off a suggestion from Urs to disambiguate between two-level type theory and other theories with two layers in the nForum page for propositional equality.

Anonymous

- Discussion Type
- discussion topicRoy L. Crole
- Category Latest Changes
- Started by nLab edit announcer
- Comments 2
- Last comment by varkor
- Last Active Nov 9th 2022

- Discussion Type
- discussion topicCooper pair
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Nov 9th 2022