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.
The content of this article appears to be included in differential graded coalgebra#cdgc. Should this article be deleted?
Added an examples section with examples of propositional resizing, propositional impredicativity, impredicative polymorphism, and the type theoretic axiom of replacement
Karl Schoenbaum
I am working on an entry cohesive homotopy type theory.
This started out as material split off from cohesive (infinity,1)-topos, but is expanding now.
added pointer to the landing page (www.wolfram.com/mathematica) and cross-link with Stephen Wolfram
I gave the stub-entry Hopf algebroid a paragraph in the Idea-section that points out that already in commutative geometry there are two different kinds of Hopf algebroids associated with a groupoid (just as there are two versions of Hopf algebras associated with a group):
The commutative but non-co-commutative structure obtained by forming ordinary function algebras on objects and morphisms;
The non-commutative but co-commutative structure obtained by forming the groupoid convolution algebra.
For the moment I left the rest of the entry (which vaguely mentions commutative and non-commutative versions without putting them in relation) untouched, but I labelled the whole entry “under constructions”, since I think this issue needs to be discussed more for the entry not to be misleading.
I may find time to get back to this later…
I just have met Jamie Vicary in Brussels, at QPL 2012. In his nice talk he pointed to an Lab page which I didn’t know existed:
It’s about a computer algebra software that can handle KV-2-vector spaces. I have just now added some cross links.
added English translation of this bit
PN§260 Der Raum ist in sich selbst der Widerspruch des gleichgültigen Auseinanderseins und der unterschiedlosen Kontinuität, die reine Negativität seiner selbst und das Übergehen zunächst in die Zeit. Ebenso ist die Zeit, da deren in Eins zusammengehaltene entgegengesetzte Momente sich unmittelbar aufheben, das unmittelbare Zusammenfallen in die Indifferenz, in das ununterschiedene Außereinander oder den Raum.
Space is in itself the contradiction of the indifferent being-apart and of the difference-less continuity, the pure negativity of itself and the transformation, first of all, to time. In the same manner time – since its opposite moments, held together in unity, immeditely sublate themselves – is the undifferentiated being-apart or: space.
And polished a little around and following this bit.
An AnonymousCoward started NBG last month.
added to Mizar a quote:
One of the biggest problems that worry the developers of automated deduction systems is that their systems are not sufficiently recognized and exploited by working mathematicians. Unlike the computer algebra systems, the use of which has indeed become ubiquitous in the work of mathematicians these days, deduction systems are still seldom used. They are mostly used to formalize proofs of well-established and widely known classical theorems, the Fundamental Theorem of Algebra formalized in the systems Coq and Mizar may serve as a perfect example here. Such work, however, is not always considered to be really challenging from the viewpoint of mathematicians who are concerned with obtaining their own new results. Therefore it has been recognized as a big challenge for the deduction systems community to prove that some of the state-of-the-art systems are developed enough to cope with formalizing recent mathematics.
added references to Lean
For completeness, so that we now have this list:
I have created a page list of mathematics software with links to all the nLab pages I could find about software packages, and put all of those pages in category: software.
added pointer to:
Jeffery Zucker, Formalization of Classical Mathematics in Automath, Colloques Internationaux du Centre National de la Recherche Scientifique 249 (1975) 135-145 [web, pdf]
also in: Studies in Logic and the Foundations of Mathematics 133 (1994) 127-139 [doi:10.1016/S0049-237X(08)70202-7]
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
Is there any point to having both type of propositions and Prop? The analogous page-name Type is a redirect to type of types.
Three questions at axiom of foundation.
Starting page for one of the authors of the publication
Anonymous
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.
I was just made aware of writing in the nLab by Todd Trimble on the category theory Zulip. I think this article should be updated to the current state of the nLab in 2025 (e.g. remark 1.1 should be removed because it isn’t true anymore). It should also be linked from the first section of the HomePage so that users have an idea what to do and what not to do on the nLab. I believe if it was accessible from the HomePage all these years, then we wouldn’t have had so many anonymous editors posting their original research on the nLab in the past few years.
apartness relation says
The negation of an apartness relation is an equivalence relation. (The converse of this is equivalent to excluded middle.)
But it seems to me that the converse (“the negation of an equivalence relation is an apartness relation”) only requires de Morgan’s law. If is an equivalence relation, then certainly and , so the only thing to worry about is comparison. If , then contraposing transitivity gives , which by de Morgan gives .
I am splitting off band from rectangular band, and will be adding material.
creating page for reference
creating page for reference
added to the list of References at categorical logic a pointer to
copied over, from overcategory, statement and proof of computing limits in undercategories
Entry to fill in some of the ideas from a poset viewpoint. Note the use of the term ’residual’ for the left adjoint. It seems that this use is really traditional coming from the sense that a ’residue’ is the bit left ove. The link with ‘internal homs’ is then a categorication of that, which puts a different light on internal homs!
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.
creating page for the reference
creating page for the reference
created page for the reference
Is this article a duplicate of cumulative hierarchy?
created page for the reference