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.
I noticed that we had no entry density, so I very briefly created one. While cross-linking it, I noticed that at volume form there is related discussion re “pseudo-volume forms”. Maybe somebody here would enjoy to add a bit more glue? (I won’t at the moment.)
I added a couple of references for the claim
There is a Curry–Howard correspondence between linear-time temporal logic (LTL) and functional reactive programming (FRP).
How about for CLT and CLT* (in the computation tree logic section)?
Were we looking to integrate this section with the one above on temporal type theory as an adjoint logic, could there be a way via some branching representation of our type as a tree?
I see Joachim Kock has an interesting way of presenting trees.
started formal dg-algebra
Deleted. Former content:
Basic Research in Computer Science is an international research and PhD school within the areas of computer and information sciences, hosted by the Universities of Aarhus and Aalborg in Denmark, and funded partially by the Danish Agency for Science, Technology, and Innovation.
stub at locally compact locale
A bare minimum, for the moment just to connect the statement (which had long been made at Fredholm operator but without any comment on where it comes from) to some references.
I have edited a bit at Fredholm operator. Also started a stubby Fredholm module in the process. But it remains very much unfinished. Have to interrupt now for a bit.
added pointer to generalization to linearly distributive categories by Cockett and Seely
Created poset-stratified space. I wasn’t sure what to call this, since the references generally just call it a “stratified space”, but our page stratified space is about all notions of stratified space rather than just one of them. Suggestions are welcome.
(Am now listening to John Francis talk about these things at the Mid-Atlantic Topology Conference.)
some minimum, for the moment mostly to record this item:
I was involved in some discussion about where the word “intensional” as in “intensional equality” comes from and how it really differs from “intenTional” and what the point is of having such a trap of terms.
Somebody dug out Martin-Löf’s lecture notes “Intuitionistic type theory” from 1980 to check. Having it in front of me and so before I forget, I have now briefly made a note on some aspects at equality in the section Different kinds of equalits (below the first paragraph which was there before I arrived.)
Anyway, on p. 31 Martin-Löf has
intensional (sameness of meaning)
I have to say that the difference between “sameness of meaning” and “sameness of intenTion”, if that really is the difference one wants to make, is at best subtle.
at principle of equivalence I have restructured the Examples-section: added new subsections in “In physics” on gauge transformations and on general covariance (just pointers so far, no text), and then I moved the section that used to be called “In quantum mechanics” to “Examples-In category theory” and renamed it to “In the definition of -categories” (for that is really what these paragraphs discuss, not any notion of equivalence in quantum mechanics, the application of -categories in that context notwithstanding)
Added an examples section with examples of propositional resizing, propositional impredicativity, impredicative polymorphism, and the type theoretic axiom of replacement
Karl Schoenbaum
moving plenty of material from material set theory that I felt deserved its own page on the difference between material and structural set theory.
Anonymous
Starting page for one of the authors of the publication
Anonymous
Moved talk by McLarty to the History section of the refernces from functorial geometry
Migrated some content from the duplicate article G. Winskel.
Duplicate of Glynn Winskel. Content migrated there. Deleted.
I gave regular cardinal its own page.
Because I am envisioning readers who know the basic concept of a cardinal, but might forget what “regular” means when they learn, say, about locally representable category. Formerly the Lab would just have pointed them to a long entry cardinal on cardinals in general, where the one-line definition they would be looking for was hidden somewhere. Now instead the link goes to a page where the definition is the first sentence.
Looks better to me, but let me know what you think.
double power set redirected to BoolAlg but has importance in mathematics independent of its use in constructing BoolAlg
Added more material to Boolean algebra, particularly the principle of duality and the connection to Boolean rings, and a wee bit of material on Stone duality.
Stone duality deserves greater expansion, bringing out the dualities via ambimorphic (ahem, schizophrenic) structures on the 2-element set, and mentioning the connection to Chu spaces. Another day, another dollar.
splitting off the material about characteristic of a rig from characteristic to its own topic, since the characteristic of a rig is represented by two numbers, not one.
This old entry (dating from 2011, by Andrew Stacey) used to be titled “equivariant tubular neighbourhoods” (plural!). Since 2021 this has been clashing with the entry “equivariant tubular neighbourhood” without anyone (me) noticing.
But since this old entry here is not in fact generally about equivariant tubular neighbourhoods, but specialized to when the ambient space is a mapping space, I am just renaming it hereby to, as you can see, “equivariant tubular neighbourhood in a mapping space”
Have added to HowTo a description for how to label equations
In the course of this I restructured the section “How to make links to subsections of a page” by giving it a few descriptively-titled subsections.
[deleted]
I created Bishop’s constructive mathematics by moving some material from Errett Bishop and adding some more discussion of what it is and isn’t. Comments and suggestions are very welcome; I’m still trying to figure out the best way to describe the relationship of this theory to other things like topos logic.
Added as examples: , and with . Proved that they are exactly the boolean rigs of cardinal less or equal than .
I don’t know if boolean rigs in the sense of this entry are always commutative. In The variety of Boolean semirings, they show that they are commutative assuming that . If some noncommutative boolean rig exists, it must be of cardinal , not be a ring (because boolean rings are commutative) and not verify this equation.
I made “constructive logic” redirect to here (“constructive mathematics”) instead of to “intuitionistic mathematics”, as it used to
I gave continuous map a little bit of substance by giving it an actual Idea-paragraph and by writing out the epsilontic definition for the case of metric spaces, together with its equivalence to the “abstract” definition in terms of opens.
started something at Church-Turing thesis, please see the comments that go with this in the thread on ’computable physics’.
This is clearly just a first step, to be expanded. For the moment my main goal was to record the results about physical processes which are not type-I computable but are type-II computable.
I am splitting off band from rectangular band, and will be adding material.