[David Benson asked me:
This looks extremely useful... Where might I read more about this formulation of limits?
The product of f: X -> M is then a universal solution to the problem of finding
g: YxM -> X over M
and this is equivalent to the usual characterization once you have chosen the isomorphism between M and 2.
Perhaps readers of the list can suggest sources I'd overlooked.] Dear David, The underlying idea is a very broad one, namely to look for limits of internal diagrams. You will find these described in Johnstone's "Topos Theory" and (I think - I haven't got it to hand) Mac Lane and Moerdijk. Suppose, working in a suitable category S (let's say a topos), you have an internal category C. Then you can define a notion of internal diagram over C (C-shaped diagram of S-objects) and they are the objects of an external category S^C, another topos. If D is another internal category in S and F: C -> D is a functor, then there is a functor F^*: S^D -> S^C defined using pullbacks in S and it has both right and left adjoints. In fact it defines an essential (if I remember the right word) geometric morphism from S^C to S^D. Now consider the situation when D is the terminal category, one object and one morphism. S^D is just S. The the right and left adjoints of F^* calculate internal limits and colimits of internal diagrams. This is easy to see, since F^*(X) is just the constant diagram, X everywhere, and a morphism (natural transformation) between an internal diagram D and F^*(X) is just a cone or cocone over D from or to X. The adjunctions then express exactly the universal properties of limits and colimits. I was describing situations where C was a discrete category, so the internal limit is an internal product. I also considered the question of whether the construction of the internal limit was geometric - preserved under inverse image functors of geometric morphisms. I have written about this kind of question in my own work, for instance "Topical Categories of Domains". (See my website, http://mcs.open.ac.uk/sjv22 .) Geometricity in general rules out the use of exponentiation in the topos, but exponentiation Y^X is geometric if X is finite with decidable equality (Johnstone and Wraith, ??"Algebraic theories in a topos"). My proposal is that the record type construction should be seen as a solution to the problem of internal products, but that it relies on finite decidability of the set of field names - hence it's related to geometricity of the internal product. In a different direction, note that internal products make sense in categories other than toposes, even if they don't always exist. For instance, if f: X -> Y is a continuous map of spaces, then the internal product, if it exists, is a space of continuous sections of f. I bet that's explored somewhere in the literature, but I don't know where. Best regards, Steve.