# 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 a sidebar contents for set theory, could add a lot more to this list

Anonymous

GrothenDitQue:

• Inspired by a discussion with Martin Escardo, I created taboo.

• adding some skeleton to this previously empty entry, no real content yet

• Unstub the page with a basic but original blurb. Compare and contrast my article list of complexity classes on esowiki, which has a very different audience.

• In looking for texts that would address the question “What is computation?” and arrive at an answer vaguely akin to path lifting/transport, I found (and have now added pointer to) this text:

which gets pretty close, in particular in and around their Figure 1.

• a stub entry, for the moment just in order to make the link work

• I have made some trivial edits to the wording, hoping to make it flow more nicely.

By the way, this entry is linking (at least now that I adjusted the plural redirect) to recursive function. This is only natural, but – unfortunately – our entry recursive function is empty (and always has been)!

Much of the material needed there is at partial recursive function. We should either put redirects or (better) add a little bit of content to recursive function.

• starting page on endomorphism monoid objects, to generalize endomorphism monoids and endomorphism rings

Anonymous

• New category: people entry

• fix minor typo ’Bair space’ -> ’Baire space’

Jack Crawford

• New category: people entry

• while bringing some more structure into the section-outline at comma category I noticed the following old discussion there, which hereby I am moving from there to here:

[begin forwarded discussion]

+–{.query} It's a very natural notation, as it generalises the notation $(x,y)$ (or $[x,y]$ as is now more common) for a hom-set. But personally, I like $(f \rightarrow g)$ (or $(f \searrow g)$ if you want to differentiate from a cocomma category, but that seems an unlikely confusion), as it is a category of arrows from $f$ to $g$. —Toby Bartels

Mike: Perhaps. I never write $(x,y)$ for a hom-set, only $A(x,y)$ or $hom_A(x,y)$ where $A$ is the category involved, and this is also the common practice in nearly all mathematics I have read. I have seen $[x,y]$ for an internal-hom object in a closed monoidal category, and for a hom-set in a homotopy category, but not for a hom-set in an arbitrary category.

I would be okay with calling the comma category (or more generally the comma object) $E(f,g)$ or $hom_E(f,g)$ if you are considering it as a discrete fibration from $A$ to $B$. But if you are considering it as a category in its own right, I think that such notation is confusing. I don’t mind the arrow notations, but I prefer $(f/g)$ as less visually distracting, and evidently a generalization of the common notation $C/x$ for a slice category.

Toby: Well, I never stick ‘$E$’ in there unless necessary to avoid ambiguity. I agree that the slice-generalising notation is also good. I'll use it too, but I edited the text to not denigrate the hom-set generalising notation so much.

Mike: The main reason I don’t like unadorned $(f,g)$ for either comma objects or hom-sets is that it’s already such an overloaded notation. My first thought when I see $(f,g)$ in a category is that we have $f:X\to A$ and $g:X\to B$ and we’re talking about the pair $(f,g):X\to A\times B$ — surely also a natural generalization of the very well-established notation for ordered pairs.

Toby: The notation $(f/g/h)$ for a double comma object makes me like $(f \to g \to h)$ even more!

Mike: I’d rather avoid using $\to$ in the name of an object; talking about projections $p:(f\to g)\to A$ looks a good deal more confusing to me than $p:(f/g)\to A$.

Toby: I can handle that, but after thinking about it more, I've realised that the arrow doesn't really work. If $f, g: A \to B$, then $f \to g$ ought to be the set of transformations between them. (Or $f \Rightarrow g$, but you can't keep that decoration up.)

Mike: Let me summarize this discussion so far, and try to get some other people into it. So far the only argument I have heard in favor of the notation $(f,g)$ is that it generalizes a notation for hom-sets. In my experience that notation for hom-sets is rare-to-nonexistent, nor do I like it as a notation for hom-sets: for one thing it doesn’t indicate the category in question, and for another it looks like an ordered pair. The notation $(f,g)$ for a comma category also looks like an ordered pair, which it isn’t. I also don’t think that a comma category is very much like a hom-set; it happens to be a hom-set when the domains of $f$ and $g$ are the point, but in general it seems to me that a more natural notion of hom-set between functors is a set of natural transformations. It’s really the fibers of the comma category, considered as a fibration from $C$ to $D$, that are hom-sets. Finally, I don’t think the notation $(f,g)$ scales well to double comma objects; we could write $(f,g,h)$ but it is now even less like a hom-set.

Urs: to be frank, I used it without thinking much about it. Which of the other two is your favorite? By the way, Kashiwara-Schapira use $M[C\stackrel{f}{\to} E \stackrel{g}{\leftarrow} D]$. Maybe $comma[C\stackrel{f}{\to} E \stackrel{g}{\leftarrow} D]$? Lengthy, but at least unambiguous. Or maybe ${}_f {E^I}_g$?

Zoran Skoda: $(f/g)$ or $(f\downarrow g)$ are the only two standard notations nowdays, I think the original $(f,g)$ which was done for typographical reasons in archaic period is abandonded by the LaTeX era. $(f/g)$ is more popular among practical mathematicians, and special cases, like when $g = id_D$) and $(f\downarrow g)$ among category experts…other possibilities for notation should be avoided I think.

Urs: sounds good. I’ll try to stick to $(f/g)$ then.

Mike: There are many category theorists who write $(f/g)$, including (in my experience) most Australians. I prefer $(f/g)$ myself, although I occasionally write $(f\downarrow g)$ if I’m talking to someone who I worry might be confused by $(f/g)$.

Urs: recently in a talk when an over-category appeared as $C/a$ somebody in the audience asked: “What’s that quotient?”. But $(C/a)$ already looks different. And of course the proper $(Id_C/const_a)$ even more so.

Anyway, that just to say: i like $(f/g)$, find it less cumbersome than $(f\downarrow g)$ and apologize for having written $(f,g)$ so often.

Toby: I find $(f \downarrow g)$ more self explanatory, but $(f/g)$ is cool. $(f,g)$ was reasonable, but we now have better options.

=–

• At comma object, Eduardo Pareja-Tobes put a query box which does not seem to have been ‘answered’. This was some time ago it seems.

• Created the entry

• Created page.

• Created page and added some references.

• removing query box from page

+– {: .query} Mike Shulman: Is there a formal statement in some formal system along the lines of “a non-extensional choice operator does not imply AC”?

Toby: I don't know about a formal statement, but I can give you an example.

Recall: In Per Martin-Löf's Intuitionistic Type Theory (and many other systems along similar lines), the basic notion axiomatised is not really that of a set (even though it might be called ’set’) but instead a preset (or ’type’). Often one hears that the axiom of choice does hold in these systems, which doesn't imply classical logic due to a lack of quotient (pre)sets. However, if we define a set to be a preset equipped with an equivalence predicate, then the axiom of choice fails (although we have COSHEP if presets come with an identity predicate).

A lot of these systems (including Martin-Löf's) use ’propositions as types’, in which $\exists_{x:A} P(x)$ is represented as $\sum_{x:A} P(x)$, which comes equipped with an operation $\pi: \sum_{x:A} P(x) \to A$. That is not going to get us our choice operator, but since a choice operator is constructively questionable anyway, then let's throw in excluded middle. This is known to not imply choice, but we do have, for every preset $A$, an element $\varepsilon_A$ of $A \vee \neg{A}$, that is of $A \uplus \empty^A$. It's not literally true that $\varepsilon_A$ is of type $A$, of course, but that would be unreasonable in a structural theory; what we do have is a fixed $\varepsilon_A$ such that, if $A$ is inhabited, then $\varepsilon_A = \iota_A(e)$ for some (necessarily unique) $e$ of type $A$ (where $\iota_A$ is the natural inclusion $A \to A \uplus \empty^A$), which I think should be considered good enough. This is for presets (types), but every set has a type of elements, so that gets us our operator.

How is this nonextensional? We do have $\varepsilon_A = \varepsilon_B$ if $A = B$ (which is a meaningful statement to Martin-Löf, albeit not a proposition exactly), but if $A$ and $B$ are given as subsets of some $U$, then we may well have $A = B$ as subsets of $U$ without $A = B$ in the sense of identity of their underlying (pre)sets. In particular, if $f: U \to V$ is a surjection and $A$ and $B$ are the preimages of elements $x$ and $y$ of $V$, then $x =_V y$ will not imply that $\varepsilon_A = \varepsilon_B$, and the proof of the axiom of choice does not go through. It will go through if $x$ and $y$ are identical, that is if $x = y$ in the underlying preset of $V$, so again we do get choice for presets (again), but not for sets.

I'm not certain that a nonextensional global choice operator won't imply excluded middle in some other way, but I don't see how it would. You'd want to do something with the idea that $\varepsilon_A$ always exists but belongs to $A$ if and only if $A$ is inhabited, but I don't see how to parse it (just by assuming that it exists) to decide the question.

Mike Shulman: That’s a very nice explanation/example, and it did help me to understand better what’s going on; thanks! (Did you mean to say “excluded middle” and not “AC” in your final paragraph?) What I would really like, though, is a statement like “the addition of a nonextensional global choice operator to ____ set theory is conservative” (i.e. doesn’t enable the proving of any new theorems that doen’t refer explicitly to the choice operator). Of course I am coming from this comment, wondering whether what you suggested really is a way to get a choice operator without implying the axiom of choice.

Toby: Yeah, I really did mean to say ’excluded middle’; remembering that comment, I assume that the real question is whether the thing is OK for a constructivist. I just argued $\mathbf{ITT} + EM \vDash CO$, and I know the result $\mathbf{ITT} + EM \not\vDash AC$, so I conclude $\mathbf{ITT} + CO \not\vDash AC$; but I don't know $\mathbf{ITT} + CO \not\vDash EM$ for certain. I certainly don't have $\mathbf{ITT} + CO$ conservative over $\mathbf{ITT}$, nor with any other theory (other than those that already model $CO$, obviously).

Mike Shulman: Where should I look for a proof that $\mathbf{ITT} + EM$ doesn’t imply AC?

Toby: I'm not sure, it's part of my folk knowledge now. Probably Michael J. Beeson's Foundations of Constructive Mathematics is the best bet. I'll try to get a look in there myself next week; I can see that it's not exactly obvious, and perhaps my memory is wrong now that I think about it.

Mike Shulman: I’m trying to prove the sort of statement I want over at SEAR+?.

Toby: No, I can't get anything at all out of Beeson (or other references) about full AC (for types equipped with equivalence relations) in $\mathbf{ITT}$.

Harry Gindi: I have references for this discussion that should settle the issue at hand:

Bell, J. L., 1993a. ’Hilbert’s epsilon-operator and classical logic’, Journal of Philosophical Logic, 22:1-18

Bell, J. L., 1993b. ’Hilbert’s epsilon operator in intuitionistic type theories’, Mathematical Logic Quarterly 39:323-337

Meyer Viol, W., 1995a. ’A proof-theoretic treatment of assignments’, Bulletin of the IGPL, 3:223-243

Toby: Thanks, Harry! Now I just have to find these journals at the library. =–

Anonymous

• Created the entry

• Created this page with the defintion of a terminating rewriting system. It was linked on the page “rewriting”.

• starting article on the differences between set theory and dependent type theory

Anonymous

• Only a stub at the moment, but I thought we needed to start a page on this. Looks like it’s going to become important.

• adding section on the universal quantifier in dependent type theory

Anonymous

• Change 1: Original page describes the fan theorem as requiring the bar to be decidable, claims that the “classical” fan theorem contradicts Brouwer’s continuity principle. The latter claim is not true; I corrected the error. I have stated the result as two separate theorems: the decidable fan theorem, about decidable bars, and the fan theorem, about bars in general.

Change 2: Slightly more information is provided about the relationship between the Fan Theorem and Bar Induction. Eventually, we should make a page about the latter.

Change 3: the section on equivalents to the fan theorem has been fixed somewhat. The section originally asserted that all of the statements provided were equivalent to the decidable fan theorem; in fact, some are equivalent to the decidable fan theorem and some to the full fan theorem.

• I have removed the bulk of the Idea section that I had written, starting way back when the entry was created in 2013.

I kept the other material that Mike (Shulman) had written.

I see now that mine was really besides the point.

Now that I finally understand this topic more deeply, maybe I find time to write a better explanation of what’s really going on.

• starting something

• I am finally giving this its own page, for ease of linking to it.

Unfortunately the term is not self-explanatory: it’s implicitly short for something like “dynamic lifting of quantum measurement results back into a classical computational context”

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• Init page and try to describe why some computer scientists have wacky names like catamorphism for a homomorphism out of an initial algebra.

Not sure what “context” sidebar to put here. Do we have one for just “computer science” or more specifically here “functional programming”?

• I tried to implement the connection between D-modules and quasicoherent sheaves a bit more

• added to D-module the alternative definition in terms of quasicoherent sheaves of the deRham space

• added to deRham space accordingly a pointer to D-modules (also fixed wrong notation in the formulas there)

• added to quasicoherent sheaf at the very bottom a pointer to D-modules.

This needs improving. Notably good references should be given.

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

Anonymous

• 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

• Started page.

• I am starting something at six operations.

(Do we already have an nLab page on this? I seemed to remember something, but can’t find it.)

• Added two propositions about the general case of monoids and comonoids in a closed monoidal categories. It looks that it could work in such a general context and thus be used in models of linear logic or in differential categories, so that’s exciting. I’ll try to prove them.

• giving this a little entry

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• stub entry, for the moment just to record some references

• brief category:people-entry for hyperlinking references

• in analogy to what I just did at classical mechanics, I have now added some basic but central content to quantum mechanics:

• Quantum mechanical systems

• States and observables

• Spaces of states

• Flows and time evolution

Still incomplete and rough. But I have to quit now.

• Wikipedia has a nice article on quantum operations.

The nLab also had a page quantum operations and channels (cache bug?), but I’ve renamed this to simply quantum operation since a quantum channel seems to be nothing but a quantum operation when viewed from the perspective of quantum information theory. Eventually, this page might need some disambiguation since there may be several uses of the term, but for now I think it is “ok”.

I think this page can be cleaned up. I started, but don’t think I will be able to finish.

In particular, there is some background material that might be better on separate pages. I’ll continue trying to clean things up, but family might be calling soon and I’ll need to run quickly whatever state it is in.

I also made the simple statement

In quantum mechanics, a quantum operation is a morphism in the category of density matrices

at the beginning of the Idea section motivated by O’Loan’s comment

A quantum channel is a mapping which sends density matrices to density matrices.

This seems innocent enough, but someone might check the statement. For one, I’ve never seen a category of density matrices, but the idea seems obvious enough. Maybe a word on density matrix would be good.

• now creating this entry.

The technical material under “Details” (here) is copied over from what I had written at reader monad – Examples – quantum reader monad. (There may still be room left to adjust the wording in order to reflect that this material moved to a new entry.)

To this I have now added an Idea-section (here) which highlights the relation to (equivalence with) Bob Coecke’s “classical structures” (which term I made redirect to here now)

• a stub entry, for the moment just to make links work