Okay, thanks!

]]>I have done that renaming and put an adjective page at canonical for now.

The newly named core-natural transformation still needs rewriting, but I need to go to bed now.

]]>Yes, let’s do that renaming, and then maybe someone can make a new page canonical that discusses all the possible meanings and points to this thread.

]]>Mike, as I said, maybe it’s a bad idea to try to formalize “canonical”, but if one does have an nLab page that claims to do so, then that should at least be a reasonable attempt – and currently it is not. One need not do it, but if one does it then one should do it right.

So maybe if we can’t figure out how to fully formalize “canonical”, then I guess we can still agree to rename the entry that is currently at *canonical morphism* to maybe *core-natural transformation*. Anyone opposed to doing that?

But if you “forget” that $X$ is a 2-element set then the only possible endomorphism is $id$.

If you're willing to use the law of excluded middle, then there *is* another definable endomorphism of $X$, which is (at least for some $X$) different. It just has a complicated definition that begins with a case analysis on whether $X$ is a $2$-element set or not.

By Jim’s definition

everymap between groupoids is canonical.

I think that you may be making a level slip here. Any functor $F\colon G \to H$ between groupoids may be used to define a canonical object of $H$, given an object of $G$. But there is no canonical functor between two groupoids, given those groupoids; that would be defined by a core-natural transformation between the projections $Gpd \times Gpd \to Gpd$, and there is no such thing. So, it would be a mistake to say that there is a canonical map between groupoids.

I like the term “core-natural” for transformations that are natural with respect to isomorphisms.

For that precise technical concept, you are probably correct. After all, that's what I have to say here when I find that I have to clarify what I mean! The current page is probably most easily turned into a page on those (which we should have since they are not an entirely trivial concept). But I would still like to have something on what it means to have a canonical such-and-such, with a discussion of the principle of equivalence, parametric polymorphism, and definability. (Maybe we're not in a position to write that yet.) Defining canonical morphisms by core-natural transformations is just one example of this.

And I really don't think that any of this has much to do with constructivism! The issue is definability. It's true, of course, that more things are classically definable than are constructively definable, and that's interesting, but this still applies to classical mathematics as well. (This is an anti-Jim argument, if I may put it that way. One might hope that bringing in constructivism would remove the allegedly pathological example of a canonical function from a set to itself, making his terminology seem more correct; but even constructively, there is still another canonical function from a *finite* set to itself.)

What’s next, a precise mathematical definition of “obvious”?

At least for theorems, ‘obvious’ means that you should be able to prove it, while ‘trivial’ means that you should have already proved it (perhaps immediately upon hearing it, perhaps earlier). People often mix these up. Of course, there are other meanings of ‘trivial’. I see here (which I found while searching fruitlessly for a different joke) that the tangent bundle of any orientable $3$-dimensional manifold is trivial but that this isn't obvious. (Of course, that depends on who you are!)

]]>Personally, I like the term “core-natural” for transformations that are natural with respect to isomorphisms. I would actually rather *not* try to give *any* precise mathematical meaning to “canonical”; I’d rather leave some common English words to use when speaking English. It’s bad enough that “natural” has a precise meaning. What’s next, a precise mathematical definition of “obvious”?

There has to be some context-dependence here. If you “know” that $X$ is a 2-element set, then there is certainly a definable non-trivial endomorphism of $X$. I think it’s reasonable to say that it is canonical. But if you “forget” that $X$ is a 2-element set then the only possible endomorphism is $id$. Similarly, if you “know” that $X$ is a object in an abelian category, then there is a definable automorphism of $X$ that is non-trivial in general, namely $- id$. If you “forget” the $Ab$-enrichment but remember the $CMon$-enrichment, then you can still define the $0$ endomorphism. And so on.

Perhaps one can apply a principle of simplicity?

]]>Thanks for all the input.

But I am not sure why you are all waiting for me to say again what I want. The colloquial notion “canonical element” is used all over the place in mathematical writing, so I think we all know what we want when we say we want a formal statement that at least comes close to characterizing what the colloquial term “canonical element” means.

And as Mike said in #9: what Toby suggests doesn’t seem to capture what we colloquially mean when we say “canonical” in mathematical writing.

It is true that I suggested that the answer has to do with terms that we can actually construct. But okay, to the extent then that Toby constructs more elements than should be called “canonical”, evidently we need to refine that proposal. Maybe add something like “without using this or that”.

I do see the point that Toby makes above: that Jim’s notion captures an “principle of equivalence” which is inherent in constructive mathematics. That’s nice. But I think it is clear that Jim’s notion has nothing much at all to do with the colloquial use of “canonical”. By Jim’s definition *every* map between groupoids is canonical. That is pretty much the opposite of what one usually means by “canonical”.

So I would suggest, if I may, that you constuctivism experts try to play a bit more with formalizing that idea that “A term is canonical if it can be constructed without… or in every context such that…”. I am not sure how to fill in the blanks, but I suppose you can figure it out. It must be some genericity condition that rules out the specifica case-analyses that Toby is suggesting above. A case-analysis, too, is somehow opposite to what “canonical” should be. For a canonical term I make no analysis and no choices. I just immediately know which one it should be. How can we formalize this?

]]>Are we really foundering over whether excluded middle is true?

Heh, I believe in EM when I’m playing Minesweeper. :-)

]]>I think we need Urs to clarify what he meant. He said that his notion of canonical “should involve some notion of constructiveness”, which I thought could be interpreted to mean constructive in the constructivism sense.

]]>Urs suggested in his warning query box on the page:

canonical elements are those that are given by parametric polymorphism

I entirely agree! But polymorphism is a concept from the logical side of computational trinitarianism. Core-functoriality/naturality is the corresponding concept on the categorial side. And that's exactly what Jim was talking about.

]]>If you believe in excluded middle, then you *have* a surjection $2 \to \Omega$.

Are we really foundering over whether excluded middle is true? Don't we all agree that this sort of thing is simply *optional*?

Note also that this example (the nonstandard but still canonical = core-natural/functorial = definable endomap on an arbitrary finite set $X$) is definable by parametric polymorphism (which is another formalization that captures the same idea). You can write down the definition by doing a case analysis on the cardinality. (The version for an arbitrary set would require a case analysis on the proposition that the set has cardinality $2$, which could be done with an LEM-parsing operation in the underlying type theory.)

]]>Right, but in neither case can you construct it given *only* the set $X$. In the first case you have to also be given the surjection $2\twoheadrightarrow\Omega$ and in the second case you have to be given a proof that $X$ is finite.

You can’t

constructthis map in the sense that a constructivist would mean, since you used LEM.

I can construct it out of an arbitrary set $X$ and a surjection from $2$ to $\Omega$. Of course, a constructivist may not believe that the latter exists, but the construction is still a perfectly valid hypothetical construction out of that data.

Alternatively, take the starting datum $X$ to be a finite set (in the strictest sense of ‘finite’). The map that I mentioned can be constructed from that datum alone. That is probably a better example, so as not to be distracted by LEM. The real issue is definability.

]]>Well, Urs did say “construct”. You can’t *construct* this map in the sense that a constructivist would mean, since you used LEM. Maybe Urs could clarify what he meant?

If you say ‘the’, then you're using the meaning of ‘canonical’ as ‘usual’. This is an odd map, sure enough, but it *is* definable from the data at hand, which is the meaning of ‘canonical’ that Urs has been discussing.

use the swap function if X has exactly 2 elements but the identity function otherwise.

That doesn’t feel very “canonical” to me. If someone said “the canonical map $X\to X$” I would never guess that they meant that one.

]]>If the set $X$ has exactly $2$ elements, then there is another function from $X$ to $X$ that you can actually name with the given information: the swap function (the nontrivial auto-bijection of $X$). If you're willing to assume the law of excluded middle (so still talking about what you can construct but not actually being a constructivist), then you can generalize this to an *arbitrary* set $X$: use the swap function if $X$ has exactly $2$ elements but the identity function otherwise. That you can define this with the information at hand (and in fact write this down with a term in a type theory that has an LEM-parsing operation) is precisely what Jim meant to formalize.

This is not to defend the current state of the article, only to defend Jim's definition. The article focusses on defining a morphism of a category from an object of a category (because that's the context that Jim discussed with me once), which led to using the term ‘canonical transformation’ (which was already taken!) and then ‘canonical morphism’ (which is ambiguous since it leaves out the data). But really, the point is that ‘canonical’ (definable from the information at hand) means the same as ‘non-evil’ (respecting the operations of the relevant (higher) groupoids). I think that this is an important insight, showing (in a way that David Corfield would like) how (higher) category theory has philosophical implications and properly organizes logic (where people usually discuss definability issues).

]]>I don’t have time to dig deeper into this right now, though I would very much enjoy reading an account of Ghani’s proposed formalization of “canonical elements”, as that sounds right (now that I get the above comments).

For the moment I have just droppped a query box into the beginning of the entry *canonical morphism* “flagging it as problematic”.

Ah, I see. Okay, thanks!

Now hopefully some day somebody finds the time to sort this out and edit the nLab entry accordingly.

]]>Interesting that you say this is different from what you were aiming for, since your first example:

For instance for $X$ just any set without further information, the reason why $id \colon X \to X$ is the

canonicalmap from $X$ to itself is because this is the only one we can actuallyname

is also a standard example of parametricity. Similarly, I expect that the two projections out of a cartesian product can be identified in this way as the canonical/parametric elements of $\prod_{(X:Type)} X\times X\to X$. If you look beyond the *use* of syntax and normal forms to describe the definition, I think there is a certain relationship to what you’re thinking of.

Okay, this is a notion of “canonicity” different from the one I was aiming for and different from what the entry canonical morphism is supposed to be aiming for. This “canoninicity” is more like “admits normal form”.

What I am after here the problem of approximate formalization of what one means in mathematical writing when one says things like “consider now the canonical element of…”.

One says this all the time to mean that there is only one such element which the reader will immediately understand.

One may or may not care about giving this colloquial use of the word “canonical” a precise sense. Maybe it’s not too interesting. However, I do remember MO discussion where people were asking for a kind fo definition. But in any case, since we do have an entry that tries to formalize “canonical” in the above sense, we should at least make sure that the entry at least not increases the confusion. I think currently it does.

]]>