# Start a new discussion

## Not signed in

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

## Site Tag Cloud

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

Also hyperlinked various keywords as well as some author names in the list of references.

• Reorganized and added to the list of types of numbers.

• Stub.

• A stub with the definition and the wikipedia link.

• Started a list of ’selected papers’.

• Created a new page on right-connected double categories, with a basic definition and reference. I intend to fill in with more details and examples soon.

• added definitions of cosine function

Anonymous

• added the series definition of a sine function

Anonymous

• added a section on defining the exponential function in real algebras.

Anonymous

• Added a reference to the 2023 Bourke paper An orthogonal approach to algebraic weak factorisation systems.

• brief category:people-entry for hyperlinking references

• added (here) the full excerpt form p. 6 of Bishop’s 1967 book, an eloquent account, critique and praise of Brouwer’s Brouwerianism

• Redirect: rationals

• noticed that the entry was missing, so I created a stub for integer

• Page created, but author did not leave any comments.

Anonymous

• Created.

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• I notice that there seemed to be no-where a really explicit semantics explanation of the claim that “univalence implies the existence of quotient types”. I checked with Peter Lumsdaine, and he kindly provided some text which, up to some minor reformatting, I have put into quotient type – Properties – from univalence.

RichardMau5

• I looked at real number and thought I could maybe try to improve the way the Idea section flows. Now it reads as follows:

A real number is something that may be approximated by rational numbers. Equipped with the operations of addition and multiplication induced from the rational numbers, real numbers form a number field, denoted $\mathbb{R}$. The underlying set is the completion of the ordered field $\mathbb{Q}$ of rational numbers: the result of adjoining to $\mathbb{Q}$ suprema for every bounded subset with respect to the natural ordering of rational numbers.

The set of real numbers also carries naturally the structure of a topological space and as such $\mathbb{R}$ is called the real line also known as the continuum. Equipped with both the topology and the field structure, $\mathbb{R}$ is a topological field and as such is the uniform completion of $\mathbb{Q}$ equipped with the absolute value metric.

Together with its cartesian products – the Cartesian spaces $\mathbb{R}^n$ for natural numbers $n \in \mathbb{N}$ – the real line $\mathbb{R}$ is a standard formalization of the idea of continuous space. The more general concept of (smooth) manifold is modeled on these Cartesian spaces. These, in turnm are standard models for the notion of space in particular in physics (see spacetime), or at least in classical physics. See at geometry of physics for more on this.

• Wrote a section on the associated monad at operad, in terms of the framework introduced under the section titled Preparation.

• I’m making a correction about enriched vs internal categories.

An algebroid is a category enriched in Vect, according to the nLab page on algebroids. Meanwhile, a category internal to Vect is what Baez and Crans call a “2-vector space”.

• Generalized the definition at group of units, and added another example (analyzing the group of units of the $p$-adic integers).

• brief category:people-entry for hyperlinking references

• touched the formatting in congruence, fixed a typo on the cartesian square, added a basic example

• the topic-cluster “algebra” is stiil a little orphaned on the Lab, I find. I added a bit to

but these entries are still a bit pitiful. Maybe somebody feels challenged to turn them into good entries. Especially the latter.

Should we have pages algebra over a Lawvere theory, algebra over a PROP, etc? Some entries look like they want such links (for instance algebra itself).

• I created separator, while having the nagging feeling that we already have this entry. Of course after creating it I remembered the page generator.

So we should merge the stuff. Might this be an occasion to merge away from generator? A set of “generating objects” also means other things than “separating objects” (notably colimit generation). So I’d be inclined to move all material to separator. That would also allow to drop the warning at the beginning of generator.

• Began a page to fulfil a link.

• A stub to note some references.

• starting something (prodded by the comment here), but just a bare minimum for the moment

• Added the general formula for the inclusion-exclusion principle.

• brief category:people-entry for hyperlinking references

• 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.

• brief category:people-entry for hyperlinking references

• the entry braid group said what a braid is, but forgot to say what the braid group is; I added in a sentence, right at the beginning (and fixed some other minor things).

• Created page.

• Added alternative terminology “local right adjoint” and “strongly cartesian monad” from Berger-Mellies-Weber. They claim the former “has become the more accepted terminology” than “parametric right adjoint”; does anyone know other references to support this? (I think it’s certainly more logical, in that it fits with the general principle of “local” meaning “on slice categories” — not to be confused with the different general principle of “local” meaning “in hom-objects”.)

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• I have added pointer to

Their Prop. 7.2.2 is verbatim the characterization that BCMMS made the definition of “bundle gerbe module” a month and a half later (except that LU focus on open covers instead of more general surjective submersions, but that’s not an actual restriction and in any case not the core of the definition).

• brief category:reference-item