The Positive Rationals

Composition of lists of relations can be used to construct a notion of repetition.

For any natural n and relation r, there is a unique ({r}:|n) – i.e. relation whose left values are all r, with all members of n as right values. As this is has only one left value, it is trivially a mapping; as its (:|) is a natural, it's thus a list, of length n, each entry in which is r. For n = 0, that's [] regardless of r; ({r}:|1) = [r], ({r}:|2) = [r,r], … ({r}:|n) being thus [r,…,r] of length n.

Composition of lists is implemented by a mapping

where a&on;…&on;z relates p to q iff a relates p to some f, which … relates to some g, which z relates to q. If we apply this to ({r}:|n), we get the result of r repeated n times; when r is a displacement in some linear space, compose({r}:|n) is a displacement n times as big. Now, while I can give compose([]), hence repeat(0), a sensible meaning, it proves unhelpful in the following, so I'll define:

whose typical output is repeat(1+n) for some natural n; i.e. repeat(m) for some positive natural m; and I shan't give repeat(0) a value. Now, repeat(1+n,successor,0) is unavoidably 1+n, so repeat has an inverse, namely s(successor,0) ←s, which guarantees that it is a monic mapping.

Now, for any list h of positive naturals, repeat&on;h is a list of outputs of repeat so repeat begets

wherein: transpose maps repeat&on;h to p = (: (: p(r,i) ←r :) ←r :{relations}), in which p(r,i) is repeat(h(i),r), so that p(r) is a list for each r; its entries are all repeats of r; compose maps this list to compose(: repeat(h(i),r) ←i :) which is compose(: compose({r}:|h(i)) ←i ) which – using @ as the list-append operator, [a,…,f]@[g,…,z] = [a,…,f,g,…z], and supposing h to be (:h|1+n) – is compose(({r}:|h(0))@…@({r}:|h(n))), which is compose({r}:|k) for some natural k since the input to compose is a list whose entries are all r; thus compose(p(r)) is indeed repeat(k,r) for some k, so compose&on;p = repeat(k) is an output of repeat. Thus sum may be construed as a pull-back of compose&on;transpose, through repeat; in like manner, product is a pull-back of compose itself.