Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
@YemonChoi In light of Ruy's response, might there be a way of making the question precise to your satisfaction? It sounds like OP is saying: I don't know of any examples of ternary $C^\ast$-rings except the ones of Ruy's form (up to isomorphism).
Nico "Taking stalks" (not fibers). In brief: taking stalks of sheaves $F$ at points $x$ is a colimit of functors $F \mapsto F(U)$ where $U$ ranges over open neighborhoods of $x$ (more precisely, over the system of natural transformations $F(U) \to F(V)$ where $V \subseteq U$ are open neighborhoods). All these functors preserve colimits (and also finite limits), so a colimit of them will also preserve colimits. But the crucial fact is that the colimit over the system is a filtered colimit, and that a filtered colimit of functors to sets preserving finite limits again preserves finite limits.
Within a doctrine which roughly speaking expresses a type of logic, one can discuss "theories", which describe structures and axioms that one can formulate within the doctrine, and that objects of the doctrine may carry. Typically one can form a "universal" or "classifying" object for the theory, so that morphisms out of the classifier to another object $X$ correspond one to one with structures carried by $X$ that obey the axioms of the given theory. There is a strong parallel to the theory of classifying bundles of groups $G$ (which broadly speaking are universal models of torsors of $G$).
Well, I should probably add a little more to my answer to give a clearer idea. Certainly (1), about expressivity, can be asked. Question (2) depends on what rules of inference can be expected to hold; expressivity and rules of inference can be broadly studied according to classes of categories and how "nice" they are (e.g., are there direct images so that we can internally existentially quantify, and are there enough exactness properties so that the usual rules of inference are valid). These classes are called "doctrines". (Continued)
Yes, very much in the spirit of the Freyd-Mitchell embedding theorem for abelian categories. The close connection between embedding theorems and completeness theorems became appreciated over time.
Your guesses are good ones, but I would caution against a rigidifying tendency of settling on a particular "right place" like toposes. Depending on the mathematical proposition, you can interpret it as internalizing far beyond just toposes. But toposes are a very general playing ground if you are surveying the corpus of all mathematical propositions that can be formulated in higher-order logic.
