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

• starting page on inductive covers

Anonymous

• not sure if this concept already exists on the nLab under another article, if it does it might be better to redirect this over to that other article

Anonymous

• At locally contractible space David Roberts had written a conjecture relating local contractibility to local triviality of constant n-stacks. I have added to that a converse proposition.

Anonymous

• I added the “overtness” assumption to the statement of the theorem in section 5 (see C5.3.2 of the Elephant).

Francesco Ciraulo

• Added that map is sometimes used as a synonym.

• starting separate table for the list of different categories/functors/internal logics/theories/hyperdoctrines/etc

Anonymous

• added to the definiton-section at geometric category a pointer to the alternative terms “logical category” and “pre-logos”.

• starting article on geometric hyperdoctrines with an example on how the canonical functor from the category of overt locales to its frame of opens is a geometric hyperdoctrine

Anonymous

• Created page, mainly to record/redirect the alternate name “elementary existential doctrine” and some references.

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

Anonymous

• At overt space there was a remark that since the definition quantifies over “spaces”, the overtness of a single space might depend on the general meaning chosen for “space”, but that no example was known to the author. I added an example involving synthetic topology, which may not be quite what the author of that remark was thinking of, but which I think is interesting.

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

Anonymous

• the minimum definition and some plain cross-links (we didn’t have this elsewhere, or do we?)

• starting article on A1-cohesive homotopy type theory, where an affine line $\mathbb{A}^1$ is used instead of $\mathbb{R}$ in real-cohesive homotopy type theory, and where the shape modality is $\mathbb{A}^1$-localization rather than $\mathbb{R}$-localization.

Anonymous

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

Anonymous

• I have added to continuum a paragraph titled In cohesive homotopy type theory.

This is a simple observation and idea that I have been carrying around for a while. Several people are currently thinking about ways to axiomatize the reals in (homotopy) type theory.

With cohesive homotopy type theory there is what looks like an interesting option for an approach different to the other ones: one can ask more generally about line objects $\mathbb{A}^1$ that look like continua.

One simple way to axiomatize this would be to say:

1. $\mathbb{A}$ is a ring object;

2. it is geometrically contractible, $\mathbf{\Pi} \mathbb{A} \simeq *$.

The last condition reflects the “continuumness”. For instance in the standard model Smooth∞Grpd for smooth homotopy cohesion, this distibuishes $\mathbb{A} = \mathbb{Z}, \mathbb{Q}$ from $\mathbb{A} = \mathbb{R}, \mathbb{C}$.

So while this axiomatization clearly captures one aspect of “continuum” very elegantly, I don’t know yet how far one can carry this in order to actually derive statements that one would want to make, say, about the real numbers.

• I added a bunch of things to connected space: stuff on the path components functor, an example of a countable connected Hausdorff space, and the observation that the quasi-components functor is left adjoint to the discrete space functor $Set \to Top$ (Wikipedia reports that the connected components functor is left adjoint to the discrete space functor, but that’s wrong).

This bit about quasi-components functor had never occurred to me before, although it seems to be true. I’m having difficulty getting much information on this functor. For example, does it preserve finite products? I don’t know, but I doubt it. Does anyone reading this know?

• starting page on spatial type theory, which is modal dependent type theory with the sharp and flat modalities.

Anonymous

Anonymous

• starting article on this variant of cohesive homotopy type theory

Anonymous

• Renamed to ’integral homotopy theory’ as there are now both analogs of Quillen and Sullivan’s approaches. Added references for latter

• {#Horel22} Geoffroy Horel, Binomial rings and homotopy theory (arXiv:2211.02349)

• {#Yuan23} Allen Yuan, Integral models for spaces via the higher Frobenius. Journal of the American Mathematical Society, 36(1):107–175, 2023, (arXiv:1910.00999).

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• It was pointed out to me today that in the very special case of internal (0,1)-category objects in Set, what we are calling a “pre-category” reduces to a preordered set, while adding the “univalence/Rezk-completeness” condition to make it a “category” promotes it to a partially ordered set. I feel like surely I knew that once, but if so, I had forgotten. It provides some extra weight behind this term “precategory”, especially since some category theorists like to say merely “ordered set” to mean “partially ordered set”.

• I added to star-autonomous category a mention of “$\ast$-autonomous functors”.

• Has anyone noted what is happening at Moonshine?

• brief category:people-entry for hyperlinking references

• added type theoretic rules for the flat modality and copied references from sharp modality

Anonymous

• poset of subobjects did not yet have a remark on the frequently occurring question whether to define subobjects as morphisms or as isomorphism classes thereof, nor did it yet (seem) to have a thread. Added both. In particular, added the phrase “groupoid of subobjects”. Added two reference where the morphism-versus-class-of-morphisms issue is discussed. Refrained from making any recommendations or comparisions, only writing “alternative definition”.

Whenever I see this topic coming up, I am reminded of the “Isomorphic types are equal?!” debate.

Since I do not have much experience in this debate, I shy away from trying to connect isomorphic-types-are-equal with poset of subobjects, but it seems to me that something relevant could be said in this regard in poset of subobjects by someone more experienced.

• Rob Norris, Functional Programming with Effects, talk at Scala Days 2018 [video: YT]
• now I have finally the time to come back to this, as announced, and so I am now starting an entry:

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.

• 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

• quasigroupoids as oidificated quasigroups

Anonymous

• Brief category:people-entry for hyperlinking references

• starting discussion page

Anonymous

• starting page on membership relations in set theory

Anonymous

• Made a start on an article fixed point, which might need to be farmed out to “sub-pages” (as this is a mighty big general topic).

• starting page on categorical set theories as those set theories which attempt to directly define the category Set of sets and functions; in contrast to the soon-to-be-created article allegorical set theory which are those set theories which attempt to directly define the allegory Rel of sets and relations.

Anonymous

• Updated the linkref weak initial algebras' toweak inital’ (a.k.a. ‘weakly initial’)