Hi all, I'm requiring the brains trust of the older generation to let me know if the following definition (as exactly like this as possible) was in the air or written down pre-1980. I will assume C is a cartesian closed category, but perhaps it was stated for C a topos at the time. Definition: Let C be a cartesian closed category. An _integers object_ is a pointed object 0 : 1 --> Z with the data s : Z ---> Z and p : Z ---> Z such that p = s^{-1}, and is the initial among pointed objects with an automorphism. I have found this definition published in a computer science paper: * Turner, D.A. (1985). Miranda: A non-strict functional language with polymorphic types. In: Jouannaud, JP. (eds) Functional Programming Languages and Computer Architecture. FPCA 1985. Lecture Notes in Computer Science, vol 201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15975-4_26 and something very similar in papers in 1982 and 1980 coming from the ADJ school of computer science (heavily influenced by category theory). There it's stated more in terms of giving the definition of a algebraic data type in some inductive means. But I can't find it in the category theory literature proper. I don't know if it came from some old logic/set theory paper, or was from CT, or was just first written down by computer scientists, but it was so incredibly obvious no one wrote it down in mathematics. Please note that "well the definition is obvious" _now_ is not really sufficient, I'd like to hear from someone from pre-1980 who can say "I recall discussing this definition at the time and it was so obvious then that no one wrote it down" if this is the type of answer I'm going to get. Moreover, since I'm interested in the case where I can't assume I have colimits, any early mention _constructing_ an object of integers from the NNO in a topos in "the usual way" also isn't useful (what colimits does a CCC have for free? Certainly not quotients or pushouts) More recently (in the last decade) this characteristion has been used in MLTT/Homotopy Type Theory, and this being written on the nLab in a purely categorical way is what alerted me to the characterisation. I'm hoping to get a reference to add there, aside from the computer science ones which strike me as very likely influenced by something a category theorist could have written down. Thanks in advance, David -- Dr David Roberts http://ncatlab.org/nlab/show/David+Roberts Adjunct Associate Lecturer School of Mathematical Sciences Adelaide University — Tirkangkaku SA 5005 AUSTRALIA Australian University Provider Number PRV14404 CRICOS Provider Number 04249J ----------------------------------------------------- IMPORTANT: This email may be privileged and/or confidential, and the sender does not waive any related rights and obligations. Any distribution, use or copying of this email or the information it contains by other than an intended recipient is unauthorised. If you receive this email in error, please advise me (by return email or otherwise) immediately.