"I knew it was a spoonbill [at least]"
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.
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)
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.
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
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.
oof power still out after 24h
You are faced with two shakiras, one of whose hips *always* tells only lies, and the oth
oh oh no big walk is out? this looks so delightful
https://www.youtube.com/watch?v=Y-0rj_BcYsI
We Played BIG WALK and it's Wonderful - Exclusive Gameplay Demo
YouTube"Arbitrary precision arithmetic, now with 100% more Euclid. Featuring a functional modified Game Boy emulator where every ALU opcode is implemented entirely through geometric constructions."
https://github.com/0x0mer/CasNum

GitHub - 0x0mer/CasNum
Contribute to 0x0mer/CasNum development by creating an account on GitHub.
GitHub