Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Integers object provenance

David Michael Roberts (Jun 08 2026 at 02:52):

The page [[integers object]] on the nLab has no citation, but it feels very much like something that should have appeared in the literature, or at the very least in some public discussion, but I searched the categories mailing list archives to the best of my ability and didn't uncover anything. Searching Google Scholar isn't turning up anything useful in short order.

David Michael Roberts (Jun 08 2026 at 02:52):

Does anyone recall or know where this could have come from?

David Wärn (Jun 08 2026 at 06:18):

This is something that has at least been discussed in the context of homotopy type theory, because $\Omega S^1$ can be shown to be an integer object. See this old discussion on the nForum and this more recent paper

David Michael Roberts (Jun 08 2026 at 08:03):

Thanks! On looking at the HoTT Zulip I found https://arxiv.org/abs/2007.00167, but since the comment by @Mike Shulman saying in 2017 that $\Omega S^1$ is "the initial type equipped with a point and an automorphism", it feels like some kind of folklore, that Altenkirch] and Scoccola were managing to review/unify/systematise to more or less extent.

Nathanael Arkor (Jun 08 2026 at 08:26):

An object of integers (as well as positive integers, rationals, etc.) is discussed on page 414 (Chapter 14) of Goldblatt's Topoi: The Categorial Analysis of Logic, which is from 1984.

Nathanael Arkor (Jun 08 2026 at 08:29):

(This is the earliest reference I can find easily for "integer object" "integers object" or "object of integers".)

David Michael Roberts (Jun 08 2026 at 09:04):

Sure, I already looked at my copy of it, but it doesn't axiomatise them as on the nLab page. It's really just "do the usual construction from the natural numbers object"

David Michael Roberts (Jun 08 2026 at 09:05):

If we can define an NNO in a category with finite products, then we should be able to do that for integers objects. Then you can define "cartesian category (or CCC) with integers" synthetically.

Mike Shulman (Jun 08 2026 at 09:27):

I suppose that property of $\Omega S^1$ could have been folklore at least in some circles (NPI). I don't have a definite memory of when I first heard/observed it.

David Michael Roberts (Jun 09 2026 at 06:17):

Looking at a citation trail I found this older paper

We shall now describe by an example the use of normalized types. We define the integers ($\mathbb{Z}$), using a type Int that has 3 constructors O, S and P, and a function nf that eliminates the useless combinations: (S (P _ )) and (P (S _ )).

from

• Courtieu, P. (2001). Normalized Types. In: Fribourg, L. (eds) Computer Science Logic. CSL 2001. Lecture Notes in Computer Science, vol 2142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44802-0_39

The Int is defined as

Inductive Int : Set := O: Int | S: Int -> Int | P: Int -> Int

I don't know precisely what the "eliminating" function nf is, theoretically speaking, but looking at the (pseudo)code the author supplies, it seems to indicate that applying S to something of the form P x you get x and similarly the other way (and there's a bunch of nested case stuff, it's defined as a fixpoint etc that I don't understand).

So at least this feels like it's a "smallest inhabited type with functions S and P that are inverse". Someone who knows about the semantics of 2000-era Coq in the category of sets might be able to set me straight.

David Michael Roberts (Jun 09 2026 at 06:33):

This feels like an idea that was probably in the air in different proof assistants for a while until it emerged to mathematicians' attention more recently. I'm aware of the problem of defining integers as a quotient type in Rocq, and certainly 25 years ago the system was a lot less well understood, not least because MLTT was not as well understood as today.

David Michael Roberts (Jun 09 2026 at 08:12):

Even better: in the original Miranda (https://en.wikipedia.org/wiki/Miranda_(programming_language)) paper in 1985 Turner defines the integers this way, with no citation to prior art. Looking at the description of the axioms for integers in a 1973 LCF document it's using a positivity predicate, negation and how succ and pred are intertwined by negation, so I guess somewhere after LCF and at latest Miranda.... I can't yet find a description of the intervening languages SASL and KRC (“Kent Recursive Calculator”) to see how they do it.

Nathanael Arkor (Jun 10 2026 at 06:16):

David Michael Roberts said:

Sure, I already looked at my copy of it, but it doesn't axiomatise them as on the nLab page. It's really just "do the usual construction from the natural numbers object"

It gives a construction from which the universal property can be easily extracted, which I feel is tantamount to axiomatising them.

David Michael Roberts (Jun 10 2026 at 06:18):

Except "the usual construction" a priori only works when there are colimits to make it - and in a category with finite products or a CCC you can't follow the recipe.

Nathanael Arkor (Jun 10 2026 at 06:25):

But an integers object has a mapping-out universal property, so you can unwind the definitions of the colimits to obtain a description in a category with finite products.

David Michael Roberts (Jun 10 2026 at 06:26):

Hmm, it's not obvious to me. Given an object X. When is it an integers object, coming from the definition of ordinary integers as a quotient in Set, or in a Topos?

David Michael Roberts (Jun 10 2026 at 06:28):

Only using finite products as your available tool

David Michael Roberts (Jun 10 2026 at 06:29):

I guess my issue is that I am actually working out how to construct an integers object in that generality, assuming an NNO :-)

David Michael Roberts (Jun 10 2026 at 06:54):

It's also nice if this is not a setoid

David Michael Roberts (Jun 10 2026 at 06:59):

But this is off-topic for the thread. I was really after some actual journal or conference paper in category theory where this was written down, and not just folklore. The 1970s were notorious, and I'm happy to say it was folklore, but I have yet to email the wider community to even get someone to say "oh, yes, we knew that". I'm not going to assume they will. That it's not blindingly obvious is perhaps mildly suggested that there were other representations of the integers as a data type that I found, or instance using a positive cone and negation that intertwines successor and predecessor. Or a specification in a really old language where all kinds of extra properties were included in the definition, so it can't have been obvious that they were not needed, at least to those authors.

But I think I need to let this rest for now, and actually do some maths, less literature digging while I'm off work sick.

Nathanael Arkor (Jun 10 2026 at 07:12):

For others' convenience, here's the relevant paragraph in the book by Goldblatt:

Recalling (e.g. from the nLab page) that a natural numbers object in $\mathbf C$ may be defined as the initial algebra for the endodistributor $N := \mathbf C(1, -) \times \mathbf C(=, -)$, we can define a "pair of natural numbers" object as an initial algebra for $N + N$. This would already be enough to capture the integers in $\mathbf{Set}$. I suppose in a topos, it's not necessarily true that the successor morphism is monic, which is why Goldblatt needs to consider non-negative integers? I imagine this can be captured by modifying the endodistributor slightly, though I don't have time to check this right now.

Nathanael Arkor (Jun 10 2026 at 07:13):

David Michael Roberts said:

But this is off-topic for the thread. I was really after some actual journal or conference paper in category theory where this was written down, and not just folklore.

But Goldblatt's book contains the definition for an integers object in an elementary topos with a NNO, so I think it is reasonable to claim (for now) that this is the earliest reference.

Nathanael Arkor (Jun 10 2026 at 07:15):

It may not be the earliest explicit reference for an integers object in a category with a terminal object, but there are presumably several inequivalent definitions of integers objects in such minimal settings, depending on which presentation of the integers in $\mathbf{Set}$ one takes.

David Michael Roberts (Jun 10 2026 at 07:24):

Sorry, I didn't mean to say what you were saying was off-topic, @Nathanael Arkor ! But rather my comment about my other line of thinking on this.

David Michael Roberts (Jun 10 2026 at 07:28):

there are presumably several inequivalent definitions of integers objects in such minimal settings,

this is precisely a thing I'm thinking of. I could also simply define an integers object as having the universal property of group completion of the local NNO, and that makes sense in any finite-product category. But I was wanting to track the provenance of this set of axioms in the literature, not as a mathematical concept or as a known fact no one wrote down, but a verbal report from a 1970s topos theorist who said it was discussed generally by participants at La Jolla 1965 would be useful, too ^_^