Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeSep 16th 2013
   • (edited Sep 16th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThis came up in another thread, where it was not really on-topic. I want to re-post it here so that it gets due attention and maybe finds a resolution: I find the content at _[[canonical morphism]]_ unsatisfactory to the extent that I am voting to replace it by something else. First why I find it unsatisfactory: the entry describes a proposal by Jim Dolan from some time ago for how to give a formal meaning to the colloquial use of "canonical" in mathematics, but it seems to me that 1. nobody, not even Jim Dolan himself, ever used that in practice; 1. it does not actually capture much at all about the colloquial use of "canonical" (see below for a proposal of mine of what a proper formalization would involve); 1. the only almost-application mentioned at the bottom of the entry, which is about morphisms of QFTs, has nothing of the "canonical" flavor to it at all (on the contrary!), and the curious notion discussed there actually becomes natural if one instead considers QFTs with boundaries, as formalized on the last pages of Lurie's "classification of TFT" article. In summary, I find that the article gives an ill-motivated definition which is actually misleading and has no support from usage/practice. If this sounds harsh, please take it as motivation to convince me otherwise. I'll be happy to be convinced by a good argument and will use it to improve the entry accordingly. But currently I think the entry content should be replaced with something else. I would tend to think that a formalization of "canonical" should involve something as follows, instead. It should involve some notion of constructiveness. What is _canonical_, in colloquial meaning of the word, is that which we can actually construct, with given data (given _terms_). For instance for $X$ just any set without further information, the reason why $id \colon X \to X$ is the _canonical_ map from $X$ to itself is because this is the only one we can actually _name_, whose term we can actually construct. There are all these other maps, but we can't actually name them with the given information. Or: the reason why $(x,y) \colon \mathbb{R}^2 \longrightarrow \mathbb{R}$ are the _canonical_ coordinates on the plane is because they are the two which one can actually construct given the data by which the plane $\mathbb{R}^2$ was constructed, namely the two projection maps out of the project. The reason why all the other coordinates that we might put on $\mathbb{R}^2$ are "not canonical" is that while they "exist" in the sense of existence of mathematics, we cannot actually _construct_ them with the given data. I expect that somebody with more genuine type-theoretical practice can easily see what I am getting at here and maybe give it a more pronounced formulation.

   This came up in another thread, where it was not really on-topic. I want to re-post it here so that it gets due attention and maybe finds a resolution:

   I find the content at canonical morphism unsatisfactory to the extent that I am voting to replace it by something else.

   First why I find it unsatisfactory: the entry describes a proposal by Jim Dolan from some time ago for how to give a formal meaning to the colloquial use of “canonical” in mathematics, but it seems to me that

   1. nobody, not even Jim Dolan himself, ever used that in practice;

   2. it does not actually capture much at all about the colloquial use of “canonical” (see below for a proposal of mine of what a proper formalization would involve);

   3. the only almost-application mentioned at the bottom of the entry, which is about morphisms of QFTs, has nothing of the “canonical” flavor to it at all (on the contrary!), and the curious notion discussed there actually becomes natural if one instead considers QFTs with boundaries, as formalized on the last pages of Lurie’s “classification of TFT” article.

   In summary, I find that the article gives an ill-motivated definition which is actually misleading and has no support from usage/practice.

   If this sounds harsh, please take it as motivation to convince me otherwise. I’ll be happy to be convinced by a good argument and will use it to improve the entry accordingly.

   But currently I think the entry content should be replaced with something else. I would tend to think that a formalization of “canonical” should involve something as follows, instead.

   It should involve some notion of constructiveness. What is canonical, in colloquial meaning of the word, is that which we can actually construct, with given data (given terms).

   For instance for $X$ just any set without further information, the reason why $id \colon X \to X$ is the canonical map from $X$ to itself is because this is the only one we can actually name, whose term we can actually construct. There are all these other maps, but we can’t actually name them with the given information.

   Or: the reason why $(x,y) \colon \mathbb{R}^2 \longrightarrow \mathbb{R}$ are the canonical coordinates on the plane is because they are the two which one can actually construct given the data by which the plane $\mathbb{R}^2$ was constructed, namely the two projection maps out of the project. The reason why all the other coordinates that we might put on $\mathbb{R}^2$ are “not canonical” is that while they “exist” in the sense of existence of mathematics, we cannot actually construct them with the given data.

   I expect that somebody with more genuine type-theoretical practice can easily see what I am getting at here and maybe give it a more pronounced formulation.

2. • CommentRowNumber2.
   • CommentAuthorZhen Lin
   • CommentTimeSep 16th 2013
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexNeil Ghani suggested that this is answered in part by the theory of "logical relations", but I confess I didn't completely understand his talk. Perhaps Mike knows, since he [wrote](http://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html) about them once.

   Neil Ghani suggested that this is answered in part by the theory of “logical relations”, but I confess I didn’t completely understand his talk. Perhaps Mike knows, since he wrote about them once.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeSep 16th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI guess probably what Neil is thinking of is that a "canonicity" property of a type $A$ in a type theory says that every term of type $A$ which is definable in the empty context is automatically equal to one of a specified ("canonical") list. For instance, canonicity for $\mathbb{N}$ says that every term of type $\mathbb{N}$ definable in the empty context is equal to a [[numeral]]. At higher types a similar property is called "parametricity", e.g. the only term of type $\prod_{(X:Type)} X\to X$ that is definable in the empty context is the polymorphic identity function.

   I guess probably what Neil is thinking of is that a “canonicity” property of a type $A$ in a type theory says that every term of type $A$ which is definable in the empty context is automatically equal to one of a specified (“canonical”) list. For instance, canonicity for $\mathbb{N}$ says that every term of type $\mathbb{N}$ definable in the empty context is equal to a numeral. At higher types a similar property is called “parametricity”, e.g. the only term of type $\prod_{(X:Type)} X\to X$ that is definable in the empty context is the polymorphic identity function.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeSep 16th 2013
   • (edited Sep 16th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOkay, 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeSep 16th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexInteresting 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 _canonical_ map from $X$ to itself is because this is the only one we can actually _name_ 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.

   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 canonical map from $X$ to itself is because this is the only one we can actually name

   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.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeSep 16th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexAh, I see. Okay, thanks! Now hopefully some day somebody finds the time to sort this out and edit the nLab entry accordingly.

   Ah, I see. Okay, thanks!

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

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeSep 16th 2013
   • (edited Sep 16th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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".

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

8. • CommentRowNumber8.
   • CommentAuthorTobyBartels
   • CommentTimeSep 19th 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexIf 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).

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

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeSep 19th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> 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.

   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.

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeSep 19th 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexIf 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.

    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.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeSep 19th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWell, 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?

    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?

12. • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeSep 20th 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex>You can't *construct* this 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.

    You can’t construct this 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.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeSep 20th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRight, 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.

    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.

14. • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeSep 20th 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexNote 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.)

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

15. • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeSep 20th 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexIf 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*?

    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?

16. • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeSep 20th 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexUrs 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.

    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.

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeSep 20th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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.

    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.

18. • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 20th 2013
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItex> Are we really foundering over whether excluded middle is true? Heh, I believe in EM when I'm playing Minesweeper. :-)

    Are we really foundering over whether excluded middle is true?

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

19. • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeSep 20th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks 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?

    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?

20. • CommentRowNumber20.
    • CommentAuthorZhen Lin
    • CommentTimeSep 20th 2013
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexThere 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?

    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?

21. • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeSep 21st 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexPersonally, 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"?

    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”?

22. • CommentRowNumber22.
    • CommentAuthorTobyBartels
    • CommentTimeSep 21st 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex>By Jim's definition _every_ map 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](http://mathforum.org/kb/message.jspa?messageID=3824572) (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!)

    By Jim’s definition every map 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!)

23. • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeSep 21st 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex>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.

    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.

24. • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeSep 21st 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexMike, 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?

    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?

25. • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeSep 21st 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, 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.

    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.

26. • CommentRowNumber26.
    • CommentAuthorTobyBartels
    • CommentTimeSep 22nd 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexI have done that renaming and put an [adjective](http://ncatlab.org/nlab/list/adjective) page at [[canonical]] for now. The newly named [[core-natural transformation]] still needs rewriting, but I need to go to bed now.

    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.

27. • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeSep 22nd 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, thanks!

    Okay, thanks!