Since this question has just popped up again to the the top of the stack, I can't resist adding one more response.
It occurs to me that constructive logic (or type theory) suggests a way to formalize the meaning of "canonical". The idea is that when you say "the canonical $x$ such that $P(x)$" (or "the canonical $x$ of type $P$"), your statement is implicitly justified by some proof that $\exists x . P(x)$ (or $\exists x : P$). If this proof is constructive, then it actually constructs a specific $x$ such that $P(x)$ or term $x$ of type $P$. When you say "the canonical $x$ ...", you "extract" that constructed $x$.
Whenever we talk about formalizing math, there must be some notion of "implicit" parts of a mathematical argument which must be reconstructed in order to formalize it. You might think that the implicit parts consist simply of implicit proofs, but the use of the word "canonical" actually allows us to leave implicit certain constructions. What the constructive logic (or type theory) does is to view all the implicit stuff, proofs and constructions alike, in the same light, since it treats a construction as a kind of proof.
It's also interesting that normally, if an argument relies on an implicit proof, then it doesn't matter what proof the reader supplies, so long as it's correct. But if your argument relies on an implicit construction witnessing an existence statement, and if you want to refer back to this construction as "the canonical $x$...", then it does matter what proof is supplied insofar as the proof has to construct the right witness. Maybe this starts to point toward homotopy aspects of the type theory involved?