(Fictive) story of a time where people reasoned only up to isomorphism

This sounds an awful lot like TWF week 121:

To understand this, the following parable may be useful. Long ago, when shepherds wanted to see if two herds of sheep were isomorphic, they would look for an explicit isomorphism. In other words, they would line up both herds and try to match each sheep in one herd with a sheep in the other. But one day, along came a shepherd who invented decategorification. She realized one could take each herd and "count" it, setting up an isomorphism between it and some set of "numbers", which were nonsense words like "one, two, three,..." specially designed for this purpose. By comparing the resulting numbers, she could show that two herds were isomorphic without explicitly establishing an isomorphism! In short, by decategorifying the category of finite sets, the set of natural numbers was invented.


As Todd has already written an answer for me, maybe I can claim it as an Answer:

Exercise 1.1 in my book Practical Foundations of Mathematics (CUP 1999) reads,

When Bo Peep got too many sheep to see where each one was throughout the day, she found a stick or a pebble for each individual sheep and moved them from a pile outside the pen to another inside, or vice versa, as the corresponding sheep went in or out. Then one evening there was a storm, and the sheep came home too quickly for her to find the proper objects, so for each sheep coming in she just moved ANY one object. She moved all of the objects, but she was still worried about the wolf. By the next morning she had satisfied herself that the less careful method of reckoning was sufficient. Explain her reasoning without the aid of numbers.

My reason for putting it in the book was to try to get some anthropologist to say when and what the original "proof" was, ie the cognitive basis of the long-universal belief that this is valid, which provides the justification of counting with numbers.

What I am trying to imagine is how one of our distant ancestors with the cognitive abilities but not the education of a mathematician might approach this. Of course they would not have formulated Peano Induction or Euclidean Infinite Descent. They would have an argument (that we would more or less accept as rigorous) that the result is true for three sheep, then four and five. After that they would use Induction in the naive epistemological sense to convince themselves that it is true for arbitrarily large sets.

It seems plausible that anyone who is challenged to come up with a proof would give the following (albeit non-constructive) proof.

Suppose that some sheep $s_0$ is missing in the evening. Then the pebble $p_0$ that served as its "name" in the morning was used for some other sheep $s_1$ in the evening. But then $s_1$ must have been named by a different pebble $p_1$ in the morning, which named yet another sheep $s_2$ in the evening. And so on. All of the sheep $s_0$, $s_1$, $s_2$, ... are different individuals, Likewise all of the pebbles $p_0$, $p_1$, $p_2$, ... But, essentially as Euclid says in Book VII, Proposition 31, this is impossible for a set of sheep.

By chance, this issue came up recently following an internal seminar by Martin Escardo in Birmingham (where I am now an Honorary Research Fellow). He was developing the foundations of arithmetic (in the setting of Homotopy Type Theory, though this was not essential) in such a way that $3\times 5=5\times 3$ could be seen in a primary-school fashion as transposing a rectangle.

He based this on a function $F:{\mathbb{N}}\to{\mathsf{Set}}$ with $F0=\emptyset$ and $F(\mathsf{succ} n)=F(n)\coprod{\mathbf{1}}$. In his treatment the most difficult Proposition is $$ F(n)\cong F(m) \Longrightarrow n=m, $$ which he deduced from the Lemma $$ X\coprod{\mathbf{1}}\cong Y\coprod{\mathbf{1}} \Longrightarrow X \cong Y. $$

This Lemma holds in any lextensive category, i.e. one with finite limits and stable disjoint coproducts. The Proposition follows using Peano induction, since then $$ F(n+1)\cong F(m+1) \Longrightarrow F(n)\cong F(m) \Longrightarrow n=m \Longrightarrow n+1=m+1. $$

I think it is reasonable to suppose that Bo Peep could formulate this Lemma, but I feel it is more plausible that she would use the "infinite descent" argument than the Proposition.

I am not sure whether this answers the original question about justifying "the use of categories, or isomorphisms or equivalences", although maybe Martin's treatment of arithmetic does so.