I think I’ve figured out most parts of the cubical type theory papers; 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 some 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 for types to be equal.
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 of an equality as a dependent case.
Q: Can you be specific about, well ... manipulating equalities?
A: I'm going to jump into the main paper for cubical type theory because it is 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 fundamental 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 (I'll just write "cube" for a higher dimensional cube.) is then defined as:
fill h T {
pat_1 => faces_1,
pat_2 => faces_2,
...
pat_n => faces_n,
} t :=
cap new T {
pat_1 => faces_1(h := h /\ new),
pat_2 => faces_2(h := h /\ new),
...
pat_n => faces_n(h := h /\ new),
(h = 0) => t,
} t
The syntax faces(a := b) substitutes a in faces for b. If h = 1, because 1 /\ new = new by definition, filling gives us the ceiling modulo the name of a dimension which is not important at all. (I should now mention cap and fill binds the dimension right after its name so the dimension is invisible from the outside to clarify.) However, at h = 0 the output of cap is just t, which is the floor. All walls are preserved by the patterns. The seams between faces are always machine 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.
Below I'll introduce some syntax to represent multiple times of the presence of some similar code snippets. In such style, the above definition of filling can be written as:
fill h T {
$($pat => $faces,)*
} t :=
cap i T {
$($pat => $faces(h := h /\ i),)*
(h = 0) => t,
} t
Q: But how is cap computed?
A: The compiler generates a different implementation for each type. Below is one of the simplest HIT, S1. It's usually called a circle since it is just a line but with the two endpoints sticked together.
type S1 {
base : S1,
cycle : S1 = S1,
}
As mentioned before, you are able to not only provide constructors for the type but also ones for its (higher) equalities in the definition of a HIT. I think it's time to tell you HIT is the acronym for "High Inductive Type". I'm not quite in favor of such vague usage of the word "higher" though.
Capping for all types needs providing all pillars in order to build the cap, but in the case of S1 we have cycle 0 = cycle 1 so that two pillars coincide and therefore is only one. That "all pillars" could be satisfied more loosely for dimensions in some types is the reason for different types to deserve different caps.
Q: How is it possible to write a function out of a HIT?
A: You just match through constructors as before! To illustrate, let's write a function from S1 to the unit type.
shrink : S1 -> ()
shrink base := ()
shrink cycle := \(_ : dim) -> ()
But wait ... cycle has type S1 = S1 and should not be applied by shrink! How could it be matched over then? Here I'm actually being a little sloppy that I wrote shrink (line : base = base) := a for map base base shrink line := a : shrink base = shrink base. I think the best way to think about it is that with the introduction of HIT, all functions become higher dimensionality-wise, so the language must provide some mechanism to let the user specify the behavior of all functions when mapping any of them over an equality, and it would therefore be fine for the sloppy syntax for application to represent application to both sides of an equation.
Back to the implementation of shrink. \(_ : dim) -> () is a line that depends on no dimensions and is therefore a zero-length line we can map our cycle to. It is also the trivial equality in traditional type theory where there isn't any concept about dimensions and all types are just seperate points with no lines between them. People usually give the trivial line the name refl a := \(_ : dim) -> a.
Q: How is capping of type formers implemented?
A: I would like to defer the discussion of them because equalities within a dependent type former can be heterogeneous, which means two sides of an equation would possibly be in different types. It was not possible to establish such equality but is if we have UA where two types may be equal in a non-trivial way. For instance, to provide a cap for (l, r), we would like to construct the cap of l and that of r, but due to that the type of r could depend on l, the pillars may have to be hetergeneous equalities the type of two sides of which are different. However, I haven't shown how we can build a cap in another type.
Q: How can different types be equal?
A: In the 1930s researchers proposed 3 models to perform arbitrary computations and found they are all equivalent. It's a bit mindblowing that mathematicians have also found 3 ways to define equivalence from scratch between types in type theory ... and they are all equivalent too.
It might be self-referential at first sight, but it needs not be. Let's give 2 of the 3 definitionally different equivalences some names. Take ~=_1 and ~=_2. Equivalences being equivalent means something like the following:
(A ~=_1 B) ~=_1 (A ~=_2 B)
So we are just calling ~=_1 inside a ~=_1 which isn't a problem at all. It's just recursion. A possible question is why ~=_1 is preferred over ~=_2 in the middle. The answer is we simple have to pick one but it is really not that important considering equivalences are defined as a particular kind of invertible function so we can do another recursive call to transform the whole statement from ~=_1 to ~=_2, that is:
((A ~=_1 B) ~=_1 (A ~=_2 B)) ->
((A ~=_1 B) ~=_2 (A ~=_2 B))
Thus, it's mostly okay for us to drop the _1 and _2 and just write ~= for any one of them.
Three formulations of computation being equivalent suggested we've found the universal definition, and the same applies to equivalences. However, we still have another different, rather useless traditional equality type for types. It would be wonderful if they can also be merged together so we can get something like:
(A = B) ~= (A ~= B)
And that is UA, the univalence axiom. Dispite having a similar shape, UA is very different from the above equivalences being equivalent. Equivalences are equivalent by its nature, but it takes a hard work to add UA to the type system if you want it to compute. If UA were (A = B) = (A ~= B), you would need to construct a nested equality type from the ground up which seems even harder, so it's arguably obvious the middle relationship ought to be ~=.
To make UA a theorem, we need to at least be able to build heterogeneous cubes, in which faces may belong to different types. But how do we make the cube seamless? The solution presented in cubical type theory is that we have to pick a base type for an underlying homogeneous cube, and each face of the heterogeneous cube is associated with an equivalence to the base type. This way, we can go from the heterogeneous cube to the homogeneous one to perform capping and transform it back to the heterogeneous one to get the cap in the heterogeneous cube. In fact, that's all we need, but it's already complicated as hell.
Constructing the heterogeneous cube is mentioned as "glueing" in the paper; I'm okay with this term. We have a glue operation to specify fragments of a heterogeneous cube, which I'll write as Glued. The syntax to write down the Glued type is:
Glued {
$($pat => (\$F ** $Eq),)*
} U
In the above code, \a ** b represents a dependent pair of a and b and $Eq has type $F ~= U. To elaborate on this kind of syntax more, $F means the type $F could be different in any patterns, and similar for $Eq. The sole constructor of Glued is:
glue {
$($pat => $t,)*
} u :
Glued {
$($pat => (\$F ** $Eq),)*
} U
Where $t : $F for each fragment of the cube and u : U and the compiler must check $t is equal to u along the correct $Eq. There's also an unglue operation to produce the underlying cube of the glued one. Some rules are further enforced by the compiler to ensure an element of Glued is the same as a normal cube if it is homogeneous and glue and unglue act like inverses.
Q: How do we get a cap from another equivalent type?
A: Let's step back from the glued cube. We would likely want to know how to get a simpler dependent capping operation, that is for pillars that are T = U we want to get the ceiling in U from the floor in T. To achieve it, another primitive operation coerce is introduced. This is the last primitive operation in the theory. For simpler HITs, coerce just gives t back but with a (slightly) different type, from a T to a U. However, the general implementation for all HITs is pretty hard to do right and I defer it. The syntax of coerce for t : Line(i := 0) is:
coerce i Line { $($pat,)* } t : Line(i := 1)
Where those $pat stand for the sub-cube to be coerced.
Our next goal would be to see how we can define capd to get the cap in a cube that the floor and ceiling of it are homogeneous, but the type along the vertical dimension h could depend on that dimension. You can view it as the stepstone to the fully heterogeneous cube. Here the approach is to swap the type of the lower part of the cube to the one of the upper part of the cube. To swap the floor we can apply coerce, but we also need to swap the lower part of each wall. This kind of swapping is given a name "squeeze" in this paper.
squeeze i Line { $($pat,)* } t :=
coerce new Line(i := i \/ new) {
$($pat,)*
i = 1,
} t
Some useful intuition is that operations along \/ lower the dimensionality while those along /\ raise it. For i = 0, squeezing is some useful coercing for each face; to speed up the process, we make the coercion trivial while i = 1 as it should be. capd is then :
capd h Line { $($pat => $faces,)* } t :=
cap h Line(h := 1) {
$($pat => squeeze h Line {} $faces,)*
} (coerce h Line {} t)
We don't need to specify any patterns in squeeze and coerce because there's not much to do when only one dimension affects the type. It's similar to 1-dimensional capping in which no patterns are required either.
Now it's time to formulate capping for type formers. Remember the problem was the dependency on the bound variable causing the latter type not to be strictly equal. With capd we can sidestep that problem.
you accidentally wrote "high inductive types" as opposed to "higher inductive types" when you explained what the axiom was lol.
Fantastic article though