Internal categories in the category of groupoids. David Yetter asked whether there is a structure theorem for "groups in GROUPOIDS". I interpret this question as "models of the finite-product theory of groups in the category (which has finite products) of groupoids and homomorphisms". I have a suspicion that David had something different in mind, such as "groupoids in groups", but shall consider the question as posed. Remember, incidentally, that the category of sets is a full subcategory (preserving all sorts of structure) of the category of groupoids. [The latter is, unlike groups, (locally?) cartesian closed as well.] Now internal *categories* in groupoids [and this easily specialises to groups] seem a natural generalisation of the quotienting of a preorder to give a poset, ie the "skeletalisation". We know that there's no natural way of just picking one object from each isomorphism class - so instead take the entire isomorphism class and consider it as a group, ie as a component of the groupoid of objects. Commutative squares with two sides isomorphisms provide the groupoid of morphisms. The construction is universal in a way which I shall leave to the reader to formulate. This idea has an application to polymorphism. Eugenio Moggi and Martin Hyland once proposed as a categorical interpretation of quantification over types simply taking the product indexed by the set of [names of] objects of the category. [We have in mind categories with a small number of isomorphism classes of objects - it's quite possible to have a cartesian closed category with exactly two (nonisomorphic) objects - we call it a model of the lambda calculus with eta and surjective pairing.] Unfortunately this idea is not invariant under categorical equivalence, and is therefore objectionable to the sensibilities of semantic categoricians such as myself. However the idea may be re-interpreted internally in the category of groupoids, and then becomes invariant, as Edmund Robinson observed. In fact something similar, though slightly more complicated, arises naturally in stable domain theory. The trace factorisation (see my unpublished 1988 paper, available by anonymous FTP from theory.doc.ic.ac.uk) expresses stable functors as spans and cartesian transformations as rigid comparisons between them, making the original 2-category an internal category in the category of domains and rigid comparisons. In the case of coherence spaces, the latter is equivalent to just the category of graphs and embeddings; this easily generalises to dI-domains. For (my) quantitative domains [see my paper in the Manchester Category Theory and Computer Science proceedings, LNCS 389, also FTP] it is the category of groupoids and homomorphisms. In both these cases, second order quantification in the standard domain way [which has been attributed to Girard, but was in my thesis before, and I didn't regard it as original, though I don't know to whom to attribute it - probably Plotkin] coincides with the Moggi-Hyland-Robinson interpretation. Paul Taylor ======================================