I have never really moved past undergraduate mathematics. I think there is still much to figure out about basic mathematical objects. I think we have yet to find the true name of many basic objects. When the true name of an basic object is found, objects will only equal if they are intensionally equal and the basic operations will flow naturally from the definition.
The true name of basic objects seem to be inductive types, and the basic operations seem to be structurally recursive functions and compositions of these recursive functions. For example the true name of ℕ seems to be Peano’s definition. In Haskell it would be like:
> data NaturaNombro = Nulo
> | Sekva NaturaNombro
Primitive recursion is the basic structurally recursive function. Here is the non-dependent version of the primitive recursion function in Haskell.
> eliminuNaturaNombro :: a -> (a -> a) -> NaturaNombro -> a
> eliminuNaturaNombro x f Nulo = x
> eliminuNaturaNombro x f (Sekva n) = f (eliminuNaturaNombro x f n)
The true name of ℚ+ may be a path in the Stern-Brocot tree. Each rational number has a unique representation.
> data PozitivaProporcio = Unuo
> | PliGranda PozitivaProporcio
> | MalpliGranda PozitivaProporcio
These true names don’t seem to yield the most efficient definitions. For instance, operations such as addition and multiplication on ℕ are more efficent when operating on a binary representation such as:
> data MalnaturaNombro = Nulo
> | SekvaDuobla MalnaturaNombro
> | SekvaSekvaDuobla MalnaturaNombro
Or perhaps ℕ+ is more appropriate.
> data PozitivaMalnaturaNombro = Unuo
> | Duobla PozitivaMalnaturaNombro
> | SekvaDuobla PozitivaMalnaturaNombro
But in the end you always count with ℕ (otherwise why are you using it?) and need to take time proportional to the size of n.
These representations of binary numbers are not quite the usual definition. The problem is that in the usual definition both “0” and “00” represent zero, so equality is not intensional equality. I assume that there are fast addition and multiplication for the above representations.
It also interesting that PozitivaProporcio,
MalnaturaNombro, and PozitivaMalnaturaNombro
are isomorphic data structures. Only the semantics of the data differ.
I think that pfloide might say the same things except he would use words like “initial algebra” instead of “inductive types” and “catamorphism” instead of “structural recursion”.