Introduction
Suppose we are trying to prove that $\rm PSO_3\times PSO_3$ is isomorphic with $\rm PSO_4,$ and we catch on to the idea of using the quaternions to do so. We realize (as in Conway & Smith's On Quaternions and Octonions, whence the quotation) that we can encapsulate $\rm PSO_3$ as the set of all maps $x\mapsto\bar qxq$ for a unit quaternion $q$ operating on imaginary quaternions $x,$ and go on to trying to understand why $\rm PSO_4$ is the set of all maps $\pm(x\mapsto\bar lxr)$ for unit quaternions $l,r$ operating on quaternions $x.$
To show that all maps $\pm(x\mapsto\bar lxr)$ really are elements of $\rm PSO_4,$ we begin by showing this in the case $\bar l=\cos\theta+isin\theta,r=1.$ This is simple, since this operation rotates the plane spanned by $1$ and $i$ through an angle of $\theta,$ and rotates the plane spanned by $j$ and $k$ through an angle of $\theta$ at the same time.
But at this point, we really are done proving that all maps $\pm(x\mapsto\bar lxr)$ are elements of $\rm PSO_4,$ since, as in the book, "any imaginary unit may be called $i,$ and perpendicular one $j,$ and their product $k$" (although this was said at a different point), right-multiplication has the same geometric properties as left-multiplication, and the composition of any two elements of $\rm PSO_4$ is an element of $\rm PSO_4.$
Idea
It makes all the intuitive sense in the world to me that "any imaginary unit may be called $i,$" and I can really visualize this geometrically. Furthermore, I could go back through a proof, change all the $i$'s to $u$'s for an arbitrary imaginary unit quaternion $u,$ etc. But suppose I had a collection of proofs written by someone who wasn't very careful, and she/he had used $i, j,$ and $k$ for simplicity and computed examples, stating at the end of each one that it generalizes to all quaternions. Suppose I pored through these proofs and discovered that about a third of them were careless to the point of being false, because of some lack of care in going back/forth between general ($u,v,w$) and specific ($i,j,k$) contexts. To formalize this imaginary formalization attempt, suppose I had a computer that understood category theory really well and wanted to scan these proofs in for it and get it to check whether this person's proofs really proved whatever facts from geometry they purported to prove.
Question
In the specific example, the notion that any imaginary unit may be called $i$ and left-multiplication is like right-multiplication can be dealt with at a first approximation using the notion of automorphisms. There is a ring automorphism sending $u$ to $i$ and vice versa, and there is a group automorphism between the multiplicative group of the quaternions and its opposite group. But I wonder if it follows directly enough that geometric facts can be proved "by example."
Is there a category-theoretic context in which certain ring/group automorphisms are natural and in which their being natural is biconditional with their preserving geometric properties?
To explain why the notion of an automorphism by itself might not be enough, we can imagine $\mathbb{Q}[\sqrt{2}]$ acting on $\mathbb{R}$ by multiplication. Multiplication by $\sqrt{2}$ preserves order, but multiplication by $-\sqrt{2}$ reverses it, so in the context of orderings, it would not be accurate to say "any square root of 2 may be called $\sqrt{2}.$"
What I'm envisioning is a category $\mathcal{C}$ with an object $\mathbb{H},$ as well as a morphism for each automorphism of $\mathbb{H},$ an object $\mathbb{H}^\star,$ and a morphism for each group automorphism of $\mathbb{H}^\star,$ perhaps geometric objects or morphisms as well, and whenever we speak of "an instance of the quaternions" we are really speaking of a functor $\mathcal{C}\to\mathcal{C}$ at least one existing for each possibility of an imaginary unit being called $i,$ a perpendicular one $j,$ and their product $k.$ I know this doesn't work out as stated, because the identity morphism doesn't go to the identity morphism, but perhaps there's a way to fix that. Then an automorphism of the quaternions can be viewed as a natural transformation between functors $\mathcal{C}\to\mathcal{C},$ one preserving the hidden (say, setwise) structure of the quaternions, and another preserving their apparent ($i,j,k$) structure and for some reason, because it's natural, the geometry comes out alright.