I think I’ve figured out most parts of the cubical type theory paper(s); I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.
Q: What is cubical type theory? A: It’s a type theory giving homotopy type theory its computational meaning.
Q: What is homotopy type theory then? A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.
Q: So what are HIT and UA? A: A HIT is a type equipped with custom equality, as an example, you can write a type similar to the natural numbers but with an equality between all even numbers. Well, it cannot be called natural numbers then.
Q: And UA? A: It gives the universe the strongest possible equality in advance, because we don’t define another universe.
Q: But now we lose the ability to treat types that are alike differently! A: We don’t, similar to that you can treat some American and some Chinese differently even if all men are created equal. They’re just equal in some sense.
Q: In which sense? A: In the sense that statements about a member of one type can be turned into statements about the identified member of another equivalent type, which sounds like some reasonable minimal requirement.
Q: Are all types equal then? A: No. It’s absurd to say the empty type and the unit type are equal. Types with different number of members are never equal.
Q: What is equality? A: In traditional type theory, it could be said that people assume everything is merely equal to itself. However, in homotopy type theory, it’s allowed for types within which different equalities are defined from your perspective, even between two specific objects, and by different equalities, we mean equalities that are not equal, resulting in a complex structure of possibly infinite layers of equalities defined upon equalities.
Q: How do we, uh, let’s say, perserve equality after progressing? A: We make sure there’s a corresponding equality after any transformation by treating it as a proper case while doing any case study; it’s worthwhile to mention equalities are special in that they themselves are also bonds between cases; I’d like to think an equality as a dependent case.
Q: Can you be specific about, well … manipulating equalities?
A: Here comes the subject of cubical type theory, in which indices are assigned to referents of a single equality; By default, the left hand side of an equality is assigned index 0, and the right hand side is assigned 1. We can also combine different equalities to form new ones by attaching indices also to the equalities themselves by hand.
Q: This is still too vague!
A: The foundamental operation on equalities is what I call capping. The intuition of capping is to construct the ceiling of a cubical building given its floor and pillars, where the whole structure is made of equalities, hence the name cubical type theory. In the second-simplest example, the cap of a square can be built from 3 probably different equalities, namely the floor, the wall on the left and the wall on the right. Putting more concretely, If you use a=b as the floor, the wall on the left must have the form of a=c for some c, where c is at the top-left corner, and the right one must have the form of b=d for some d, where d is at the top-right corner. Given the 3 equalities above, capping outputs the equality c=d. Because of the fact that equalities are symmetric, what capping does on a square is just concatenation in the sense that the cap from c to d is calculated by going counterclockwise from c to a to b to d.
Q: You said the above example is the second-simplest. What’s the simplest one?
A: The above capping makes use of 2 dimensions; the simplest one would be to only depend on 1 dimension. In that case, no pillars are needed. It’s worthwhile to mention that dimensions are no more than a fancy way to reason about the indices of equalities. The established mathematical convention is to represent smaller values at the left and the bottom, thus, if the horizontal axis is, say, i, the left pillar would have the index i=0, and the right one would be i=1. Similarly, if the floor is j=0, the ceiling would be j=1.
Let’s turn back to the 1-dimensional capping operation. Now I can rephrase it as the following sentence:
Given a dimension i and a value at i=0, capping produces the corresponding value at i=1.
If you just assign that dimension to a single equality, capping produces the other end given one end of it. This explained how we traverse through 3 equalities in 2-dimensional capping; its procedure can be done not only in the metatheory but also manually. However, we want to provide special treatment in the type system to generalize the idea that an equality is a line to a square built from equalities being a face, and ultimately unify the idea of values belonging to a type in logic with points belonging to a space in geometry; equalities are lines.
Q: What if what you have is the point at i=1 but you want that of i=0?
A: There are 3 built-in operators for dimensions. First, we have ~i=0 for i=1 and ~i=1 for i=0. Therefore, capping along ~i does the above job. I think here’s some very useful intuition that a dimension, as an index, is a fuzzy boolean. It’s similar to a boolean in that it also has two obvious values. However, we can leave the index unspecified and just rely on other orthogonal dimensions as in the example to select the right-hand side of a square with only i=1. If you specify all dimensions, you can only select the vertices of a cube. From this point of view, ~i, the opposite of i, is a fuzzy NOT gate, and equalities are a distinct sort of functions from a fuzzy boolean to a value, namely one of its endpoint.
Naturally, there are also fuzzy variants of OR and AND, denoted \/ and /\ respectively; they work as expected at the endpoints of lines and provide a way to collapse dimensions, or to say, form connections between different dimensionalities.
Q: What are the available dimensions?
A: It’s up to the user to introduce new ones. In traditional type theory, the variables in scope are those binded with lambdas; similarly, equalities can be written as lambdas ranging over dimensions. An example on the paper shows how to map a function over an equality: given f:A->B and an equality x=y in A, one can derive f x=f y in B. The proof is
map (x:A) (y:A) (f:A->B) (e:x=y) = \(i: dim) -> f (e i)
e i is an application to the fuzzy boolean i. If i=0, e i would be x, and if i=1, e i would be y, so we get f x=f y. There’s also a proof of function extensionality on the paper, which basically states the reverse of the above map also holds.
Q: You still haven’t constructed any actual 2-dimensional face of let’s say, a cube, right? The aforementioned square was a hollow one. A: Yeah I’m finally ready. I would like to introduce more syntax at this point. Now I present the syntax of capping as:
cap h T {
... pattern matching through dimensions ...
} t
where h is the dimension introduced as the height of the cube, T is the space inside which we are building structures, the patterns match through the pillars or more generally higher-dimensional walls, and t is the floor of the structure whereas h=0. Later arguments of cap may depend on the previous ones: it’s cumbersome to write down all the details, but they’re pretty obvious as long as you’ve got it.
For instance, 2-dimensional capping in T is achieved by
\(d: a=b)(l: a=c)(r: b=d) -> \(i: dim) -> cap j T {
(i=0) => l j,
(i=1) => r j,
} (d i)
Pass some a=a to l and then you get the normal transitivity law for equality. Draw a square with dimensions i and j if you still don’t get it.
The operation of filling a cube is then defined as:
fill h T {
pat1 => faces1
pat2 => faces2
...
patn => facesn
} t :=
cap i T(h:=h/\i) {
pat1 => faces1(h:=h/\i)
pat2 => faces2(h:=h/\i)
...
patn => facesn(h:=h/\i)
(h=0) => t
} t
If i=1, because of the fact that 1/\h=h, filling gives us the ceiling modulo the name of a dimension which is not important at all. However, at h=0 it’s just t, which is the floor. All walls are preserved by the patterns. The seams between faces are always type checked to be undetectable, that is, to have a unique representation, to make sure the surface is smooth or to make the whole cube still works like a huge equality if you prefer the type theoretic interpretation.