Given the naturals, {0, 1, 2, 3, ...}, we can define repetition on relations:
One may as readily take repeat(0,r) = (|r:) with repeat(1+n,r) = repeat(n,r)&on;r, but the choice above works well for mappings: repeating no times a mapping which doesn't deliver all of its inputs as outputs has the desired effect of accepting the same inputs as the mapping (and considering the same ones equivalent), but `doing nothing to them' (aside from declaring that it considers some of them equivalent).
There's a natural addition on naturals, and a natural multiplication; these may, indeed, be defined by:
with both + and . being symmetric, i.e. n+m = m+n and n.m = m.n, obtained by inductive proofs. The structure of the naturals makes these interact well with repeat: repeat(n+m) = (: repeat(n,f)&on;repeat(m,f) ←f :) and repeat(n.m) = repeat(n)&on;repeat(m).
Now, for natural n, repeat(1+n) maps mappings to mappings and maps monics to monics; in contrast, repeat(0) doesn't - though it does maps each relation to an equivalence and both mappings and relations to identities, i.e. collections. As a result, I'm going to leave 0 out of the discussion hereafter.
Now, as each repeat(n) is a relation, we may take its reverse, (: r ← repeat(n,r) :), so define:
Which is pretty much reverse&on;repeat, save for restricting out n=0. (Note that this is a quite different thing from reverse(repeat) = ({naturals}: n ← repeat(n) :) - quite another matter). Note that share(n) is, in general, a relation - if repeat(n) maps two relations to the same value, share(n) relates that value to each of them.
When we compose repeat(n)&on;share(m), we get (: repeat(n,f) ← repeat(m,f) :), whose inputs are all outputs of repeat(m), i.e. in (| repeat(m) :), even if n and m have a common factor, i, and some f in (| repeat(i) :) aren't in (| repeat(m) :). Still, repeat(n)&on;share(m) relates x to y if x is repeat(n,f) and y is repeat(m,f) for some relation f; so repeat(m,x) is repeat(n.m,f), as is repeat(n,y).
Composing in the other order, share(m)&on;repeat(n) gives (: repeat(m,f) = repeat(n,g), f←g :), which patently subsumes repeat(n)&on;share(m) - read f for x, g for y in the foregoing. [So, given the choice, share(m)&on;repeat(n) is the more helpful representation of n/m, for which m\n seems an appropriate synonym.]
One may thus construe the positive rationals as {share(1+i)&on;repeat(1+j): i, j are naturals} or, at worst, the collection of composites of its members.
Now, to describe (m\n).(q\p), take share(m)&on;repeat(n)&on;share(q)&on;repeat(p) and observe that it's subsumed by share(m)&on;share(q)&on;repeat(n)&on;repeat(p) = share(m.q)&on;repeat(n.p), i.e. (m.q)\(n.p).
Now, consider addition: repeat(n+p) = (: repeat(n,f)&on;repeat(p,f) ←f :) and use share(m)&on;repeat(n) in place of repeat n, and likewise with q for p, noting that, were it but a mapping, the former would map f to share(m,repeat(n,f)), so our putative replacement for repeat(n,f)&on;repeat(p,f) is share(m,repeat(n,f))&on;share(q,repeat(p,f)). Fortunately, cheating is easy: we know (m\n)+(q\p) has to be (m.q)\(n.q+m.p), i.e. share(m.q)&on;repeat(n.q+m.p) which would map f to share(m.q, repeat(n.q, f)&on;repeat(m.p,f)), which we now merely need to relate to the above.
Not that it's pretty yet.
This construction yields a natural consequence for any commutative binary operator; characterise the last by a mapping V, for which each f in (|V:) has (:f|) = (:V|) and this subsumes (|f:), V combines a with b to yield V(a,b) also written a+b, so that V = (: (: a+b ←a :) ←b :), with a+b = b+a for all a, b in (:V|). (:V|) will be `closed under' the `addition' denoted by + only if (|V:) is closed under composition, i.e. f, g in (|V:) implies f&on;g in (|V:). When V is monic, V embeds (:V|) in (|V:), which is a collection of relations (V: :(:V|)). As relations these are amenable to repeat and share; if (|V:) is closed under composition, repeating any of its members produces another, so (|V:) will be closed under repeat(1+i) for each natural i; if V is also monic, we'll be able to infer, for any given a in (:V|), a unique member of (:V|) which V maps to repeat(n,V(a)); we can describe this member of (:V|) as n.a, thereby establishing reverse(V)&on;repeat(n)&on;V as a `scaling' of (:V|) by each positive natural n.
Equally, reverse(V)&on;share(m)&on;repeat(n)&on;V enables us to express the rationals as scalings of (:V|); notably, reverse(V)&on;share(m) is simply reverse(repeat(m)&on;V), which gives the expression a clearer form.
The crucial properties of V were: it's monic; {relations} subsumes (|V:) so we can apply repeat's outputs to its members; every composite of members of (|V:) is a member of (|V:). We may be able to relax the last to require composites, or even just repeats, of members to be, each, subsumed by a unique member of (|V:), probably imposing, in such a case, that, given two members of (|V:), either one of them subsumes the other or their intersection is empty. These suffice, in any case, to express V as the binary operator
a.k.a. (: (: reverse(V, V(a)&on;V(b)) ←a :) ←b :), further exposing the parallels with the action of the rationals - which naturally also apply themselves as `scalings' for the `addition' inferred from V.
When all that works, we get a V for which {(V:|(:V|))} subsumes (|V:).
Write P for the collection of positive rationals, on which I'll suppose I've built addition and multiplication, each of which is commutative and cuddly, along with a strict order respected by both. From addition we obtain (P: sum |{non-empty finite (P:f:)}), extending the bulk action of addition on lists by; exploiting the natural one-to-one relation between any given finite (:f|) and some natural (backed up, when f isn't a mapping, by the implied finite enumeration of each (|f:{x}) with x in (:f|), required for f to be `finite' as a relation, i.e. the union of some list of atomic relations), while; relying on commutativity to ensure that sum(f) won't depend on which one-to-one relation you use, between F and that natural (and, likewise, between each (|f:{x}) and its associated natural).
For distinctness, while keeping the the names 0 and 1 for the naturals {} and {{}}, I'll refer to the rational identity, share(1) = share(1)&on;repeat(1) = repeat(1), as `one' and, in so far as I chose to talk about it, I'll refer to the rational additive identity, share(1)&on;repeat(0) = repeat(0), as `zero'; but note that zero isn't in P, whereas one is; and, since sum is defined on non-empty mappings to P, which is closed under addition, sum's outputs are all in P.
Among mappings (P::), I can define an addition by:
This means (f+g)(x) is f(x)+g(x) when both accept x as input, is f(x) when only f accepts x and is g(x) when only g accepts x; if neither f nor g accepts x as input, nor does f+g. [In the specification given, these cases are catered to by applying sum to (: k(x)←k :)&on;[f,g], for given x (note: [f,g] is a list; it maps 0 to f, 1 to g); the composite maps 0 to f(x) if f accepts x as input, otherwise it ignores f; likewise for 1 and g. If both ignore some value (offered as x), the composite is empty, so not in (:sum|), so sum(...)←x rejects the value - refuses to let us bind x to it. If either accepts a value, however, the composite is a non-empty mapping (P: :{0,1}), which sum duly accept; our value is mapped to the sum of the outputs of this, whether there be one or two of them.]
These suffice to define the universal simplex, Simplex = {mappings (P:f:n): sum(f) = one, n is natural}. Note that (P:f:n) isn't constrained to accept all members of n as inputs; only to draw its inputs only from n, delivering outputs in P; it may `ignore' some members of n. Since sum(f) is involved in the constraint, f is implicitly obliged to be non-empty (i.e. accept at least one input); but the constraint sum(f) = one equally obliges f to be non-empty, even if sum's definition is extended to allow sum(empty) = zero. [Since sum respects addition on mappings, sum(f)+sum(g) = sum(f+g), and f+empty = f for every (P:f:), we're obliged to have sum(f)+sum(empty) = sum(f), making sum(empty) an additive identity - i.e. zero.]
Now, Simplex spans an infinite-dimensional linear domain within {(P::)}, under the addition just given and the scalings natural to that domain (induced by composing each (P:f:) before (: a.x ← x :P) for some a in P, to give (P: a.f(y)←y :) as a.f; then (: a.f←f :{(P::)}) is `scale by a' for any a in P). When describing a finite-dimensional simplex, we can readily restrict to {(::n) in Simplex} for any natural n. When n is 0, this is clearly empty, as 0 is empty, i.e. {}, so the only (P:f:0) is f = empty, which sum definitely doesn't map to one.
Next we have {(P::1) in Simplex}, with 1 = {0} having only one element, and (P:f:1) in Simplex forbids f to be empty, so f is simply the list [f(0)], its sum is f(0), so f(0) must be one, making f = [one], so {(::1) in Simplex} = {[one]}, a.k.a. {[{{}}]}. This has exactly one member; I'll call this member, [one], `the canonical vertex'.
So far so dull. For collections M, N of naturals, describe {(::N) in Simplex} as a `face' of {(::M) in Simplex} precisely if M subsumes N; and as a `proper face' if N and M are distinct. Taking N = M = {naturals}, Simplex = {(::{naturals}) in Simplex} is a face of itself; likewise, any face of Simplex is a face of itself. Describe a one-to-one correspondence between two faces, (F|g|H), as `simplicial' if (hmm, well ... it's continuous and) for each face E of F or I of H, (|g:I) is a face of F and (E:g|) is a face of H; describe F and H as simplicially equivalent in such a case - that this is an equivalence is easy to verify.
Whenever there is a one-to-one correspondence, (N|s|M), between two collections of naturals, it induces ({(P::M) in Simplex}: f&on;s ← f :{(P::N) in Simplex}) as a (very well-behaved, e.g. continuous) simplicial equivalence between their respective faces. For every collection of naturals, M, there is some such (N|s|M) with N either {naturals} or a natural, so every face of Simplex is simplicially equivalent either to Simplex itself or to some {(::n) in Simplex} with n natural; call these the `natural' faces of Simplex. For any two members of {{naturals}, n: n is natural}, one of them subsumes the other; so, for any two natural faces, one of them is a face of the other. Thus, for any two faces of Simplex, one of them is simplicially equivalent to a face of the other.
Note that Simplex has plenty of proper faces (associated with infinite collections of naturals) with which it is simplicially equivalent. Describe a face of Simplex as `finite-dimensional' iff it isn't simplicially equivalent to Simplex, i.e. iff it is simplicially equivalent to {(::n) in Simplex} for some natural n. Since every f in Simplex is (P:f:n) for some finite n, hence in a finite-dimensional face, Simplex (though infinite-dimensional) is the union of its finite-dimensional faces. Further, every finite-dimensional face of Simplex is {(::N) in Simplex} for some finite collection, N, of naturals; if we take successor(unite(N)) we get a natural which subsumes N; so every finite-dimensional face of Simplex is a face of a natural face of Simplex, so Simplex is the union of its natural faces, each of which is finite-dimensional.
The mappings (P: f(n) ←f :Simplex), for natural n, are `scalar functions of position' on Simplex; their sum is ({one}::Simplex) but they are otherwise as independent as this allows. On any finite-dimensional face, only finitely-many of these functions accept any f in the face; if we partition these scalar fields into those with n in N and those with n in M, for some disjoint finite collections N, M of naturals, we can define scalar fields (P: sum(:f:N) ←f :Simplex) and (P: sum(:f:M) ←f :Simplex); the first is undefined on {(::M) in Simplex} and one on {(::N) in Simplex}; likewise for the second but with the two faces swapped; on the original face, {(::U) in Simplex} with U the union of N and M, these two scalar fields sum to one everywhere. In this sense, the faces associated with N and M are `opposite' faces of the face associated with U.
Earlier we visited the empty face, {(::0) in Simplex}, and the canonical vertex, {(::1) in Simplex}. We now have the means to continue with the faces associated with progressively larger naturals. First, note that any natural face {(::n) in Simplex} has, for each i in n, a face {(::{i}) in Simplex}; and a mapping (P:f:{i}) with sum(f) = one must be, as f accepts only one input, the unique mapping ({one}:|{i}), so each {(::{i}) in Simplex} face is simplicially equivalent to the canonical vertex, and {(::n) in Simplex} has n such faces. A face simplicially equivalent to the canonical vertex is described as a vertex; every vertex of Simplex is just {({one}:|{n})} for some natural n. (Note that all faces simplicially equivalent to the empty face are, in fact, empty, so identically the same thing as one another: there is only one empty face, whereas there are many distinct vertices.)
For the natural face S = {(::1+n) in Simplex}, for some natural n > 0, we have a vertex {(::{n}) in S} = {({one}:|{n})}; this is opposite the face {(::n) in S}, which I'll suppose we've already described. We have complementary scalar functions (P::S) defined by f(n)←f and sum(:f:n)←f; the former is one on the {n}-vertex, the latter is one on the face opposite it; the latter is defined everywhere except on the vertex, the former everywhere except on the opposite face. Whenever one = p+q in P, we have (S: ({q}::{n}) +p.f ←f |{(::n) in S}) as an embedding of the face, opposite our {n}-vertex, in S. This clearly varies continuously in p, q and f; its outputs are in S, every position in S appears as an output and, for every g in S, there's a unique choice of p, q and f (namely q = g(n), p = one-q, f = (:g:n)/p) which yields that g as output, unless g is in either the {n}-vertex or the face opposite this. At these two ends, the above function approaches the identity on {(::n) in S} and the constant mapping which maps this whole face to the opposite vertex. We may, thus, construe the function as a continuous deformation of the face down on to the point.
Thus the face {(::2) in Simplex} is just the trail left by moving its {0}-vertex to its {1}-vertex - i.e. it's a line. Likewise, {(::3) in Simplex} is obtained by scaling down this line, by the varying factor p < one, while moving it towards the {2}-vertex, forming a triangle.
Written by Eddy.