Does inner model theory seek canonical models for large cardinals? Like the author of this question, I have heard that a main goal of inner model theory is building canonical inner models for large cardinals.  My questions are: (a) Is this accurate? (b) If so, in what sense is it thought to be possible?
We know that $L$ is a completely canonical model of ZFC constructed along the ordinals.  A remarkable result is that given an ordinal $\kappa$, if there is a model $L[U]$ in which $\kappa$ is measurable and $U$ is a normal measure on $\kappa$, then there is exactly one inner model of this form in which $\kappa$ is measurable.  This is a strong form of canonicity for inner models with one measurable cardinal.
However, canonicity seems to disappear already for models with a proper class of measurables.  (Lower strength is needed for the following, but let’s stick with measurables for now.)  As discussed in the book by Paul Larson, one may force over such a model with the stationary tower, a proper-class partial order definable without parameters.  One obtains a model $V[G]$ satisfying ZFC and a generic extender-ultrapower elementary embedding $j : V \to V[G]$.  The map is amenable to $V[G]$, meaning that $j \restriction \alpha \in V[G]$ for all ordinals $\alpha$.  Also, one may take any measurable $\kappa$ and take the ultrapower map $j : V \to M$ definable from a parameter in $V$.  So we have $M \subsetneq V \subsetneq V[G]$, each with the same ordinals and same theory.  Indeed, repeating this construction shows that, in the appropriate multiverse, every model $N$ of ZFC + "There is a class of measurables" is a member of a sequence $\langle N_i : i \in \mathbb Z \rangle$ of models with the same theory and ordinals, where $i<j$ implies $N_i \subsetneq N_j$.
It seems that a moral of this situation is that there cannot be a canonical model for a theory extending ZFC + “There is a class of measurables.”  If we were in such a model $N$, we could have always done with more or fewer sets. We cannot hope for a canonical construction dictated by a first-order theory and the class of ordinals, and instead, whatever proper-class transitive model we come up with will depend on some non-canonical sets that happen to be lying around.
Now, we could consider adding a resource to our constructions, some $A \subset Ord$.  The problem: (1) If $A$ is a set and some construction of a class from $A$ models ZFC + “There is a proper class of measurables,” then we can force the stationary tower embedding to have critical point above $\sup A$, or select a measurable cardinal above $\sup A$.  The set $A$ can be fixed among all the elements in the above $\mathbb Z$-chains.  So adding a set-sized but possibly infinitary piece of information will not nail down a unique inner model for a theory that allows class-many measurables.  (2) If we allow $A$ to be any proper class of ordinals, then we can take $A$ to code all sets, but this seems like cheating.  (Yes, the construction of the universe using exactly all information about it is canonical.)
The notion of categoricity is central to model theory. A first-order theory $T$ is said to be $\kappa$-categorical if every two models of $T$ of cardinality $\kappa$ are isomorphic. Because well-foundedness is not a purely first-order property, this kind of categoricity is not possible for models of set theory. But a categoricity among models with certain other specified features is possible. For example, ZF+”V=L” could be said to be Ord-categorical:  Any two models with the same ordinals are isomorphic. Similarly, ZF+”V=L[U]” is categorical up to a specification of the ordinals and the measurable cardinal of the model.
Is there a theory extending ZFC+”There are class many measurables” that is categorical up the specification of some reasonable parameters?  If not, what is the sense of “canonical” in the inner model program for class-many large enough cardinals?
 A: Woodin's result about sc refers to V models. nothing stops from there being a countable object with a sc cardinal up to a measurable. this won't be a sharp to the weak extender model, the smallest such thing will in fact be in this weak extender model.
"canonical" is not word that has a precise definition, at least not in inner model theory. it is simply used to express the fact that sets in mice have a very concrete definitions. for example if you have a countable mouse then a K^c construction (which you can think of as an algorithm) will eventually produce an iterate of that mouse, and so the mouse you have in a way appears in this K^c construction (it embeds into a model appearing in it). if in addition your mouse projects to omega then in fact the mouse will actually appear in the K^c construction (as apposed to being embedded into some model of the construction).
another way canonicity can be expressed this days is via OD definability.
the reals of a mouse are exactly those reals that are ordinal definable in a model of determinacy whose sets of reals consist of universally Baire sets (this is not fully known, left to right is always true if you in addition assume that the strategy of the mouse is universally Baire (which can be shown if you have class of Woodins), the other direction is the Mouse Set Conjecture.)
there is also Ultimate-L and HOD of L(Gamma_uB, bR) and etc, all of these point to the fact that sets in mice are very concrete objects.
another examples is that if you do L[E] constructions over universally Baire sets than you will not destroy determinacy, which says mice don't come with bad sets of reals.
in short, there is no definition of canonicity, but there are a lot of instances.
