Mastodawn

Suppose A is a bipointed type, that is, there exist specified terms 0, 1 : A. Then we define the "simplex" type [n] inductively as follows:
[0] = 1
[n+1] = [n] → A
For example, [1] ≅ A and [2] ≅ A → A and [3] ≅ (A → A) → A and so on, creating more deeply left-nested higher order types involving A.

Show thread

jcreed

We can identify the "vertices" of the simplices as follows.
The two vertices of the "line" [1] are simply 0, 1 : A.
The three vertices of the "triangle" [2] are the functions A → A as follows:
λ x → 0
λ x → x
λ x → 1
The four vertices of the "tetrahedron" [3] are the functions (A → A) → A:
λ f → 0
λ f → f 0
λ f → f 1
λ f → 1

Show thread

jcreed 3d ago

In general, we can inductively define v_{ni} : [n] for 0 ≤ i ≤ n, the n+1 vertices of the n-simplex. When n ≥ 2, and 1 ≤ i ≤ n-1, we can say
v_{n0} = λ k → 0
v_{ni} = λ k → k (v_{(n-2}(i-1)})
v_{nn} = λ k → 1
Notice that this typechecks. We need v_{ni} : [n] = ([n-2] → A) → A, therefore the variable k in its definition has type [n-2] → A, therefore the argument to k must have type [n-2], and indeed v_{(n-2}(i-1)} will have this type.

Show thread

jcreed 3d ago

Question: are there additional operations/equations we can put on A so that syntactically expressible maps [n] → [m] are in fact the expected simplex maps, i.e. the monotone maps from (0,…,n) to (0,…,m)? It seems to me that we would at least want A to be a distributive lattice. (although note that not all expressible maps will be lattice homomorphisms; they don't typically preserve 0 and 1)

Show thread

jcreed 3d ago

With that structure we can locate the three nondegenerate "edges" of the "triangle" via maps [1] → [2], i.e. A → A → A, as
λ x y → x ∩ y
λ x y → x
λ x y → x ∪ y
with the degenerate edges (i.e. reflexive edges at vertices) being
λ x y → 0
λ x y → y
λ x y → 1
but my understanding gets fuzzier when I try to think of higher-dimensional
faces.