Introducing these generators as objects feels like new technology perhaps not so available in Gauss' time: codata/corecursion! The idea of a finite datum (ie a

Introducing these generators as objects feels like new technology perhaps not so available in Gauss' time: codata/corecursion! The idea of a finite datum (ie a finitely specified program) which produces infinite "unfoldings" or operations is pretty formalized today, but not exactly amenable to standard set theory (or anything available in Gauss' time). For instance, usually in order to formulate these things in a set-theoretic method you need to reject the foundation axiom and replace it with the (aptly named) "anti-foundation axiom" which basically says that we can define "sets" which uniquely satisfy any recursive set of equations satisfying some properties. From here you get generator "objects", bisimilarity, and enough mechanism to formalize this proof nicely.