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

• What is a weakly separated space ?

Anonymous

• This is my first hook to the n-lab, I am pretty sure that isomorphism is an overly strong condition, and that any is a too weak restriction.

Please see the wikipedia article on the principle of bivalence. https://en.wikipedia.org/wiki/Principle_of_bivalence

I am unsure as how to proceeed.

vukovinski

• Changed requiring that all j-morphisms are invertible to demand being equivalences as in infinity-groupoid entry.

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

vukovinski

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

Anonymous

• 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 $Time$ as a tree?

I see Joachim Kock has an interesting way of presenting trees.

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

• starting something, but I am running out of steam now

• table for inclusion as floating TOCs

• am starting some minimum here. Have been trying to read up on this topic. This will likely become huge towards beginning of next year

• Added a definition of meager sets.

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

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

• in order to have a good place to record the diagram:

$\array{ ( q_1, q_2 ) &\mapsto& (x \mapsto q_1 \cdot x \cdot \overline{q}_2) \\ Sp(1) \times Sp(1) &\overset{\simeq}{\longrightarrow}& Spin(4) \\ \big\downarrow && \big\downarrow \\ Sp(1)\cdot Sp(1) &\overset{\simeq}{\longrightarrow}& SO(4) }$
• corrected the reference to point to the right publication

• updated current situation

DamienC

• Described the free suplattice on a poset.

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

• Should we replace "to all the elements in the set" with "to all the elements in the subset" at meet's definition?

> In a preordered set or partially ordered set then the meet or infimum of a subset of elements is, if it exists, the largest element which is smaller or equal to all the elements in the set. If this element is member of the original subset, then it is also called the minimum of that subset.

https://ncatlab.org/nlab/show/meet

Thank you!
• Fair enough: I changed the wording.