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.
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
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.
jcreed