**Notes on notes on cubical type theory**

After a few days of looking at these notes, the implementation, and some random background material, I think I have a rough understanding of what's going on in cubical type theory. I've heard that there's some confusion amongst people who aren't the implementers as to what's going on, and it's fairly easy to understand why. Certain notation in the notes is both non-standard and completely unexplained. And some (I think) important subtleties with the rules are also unexplained.

Fortunately, I've implemented and used enough type theories that I can go read the implementation and figure out what the notation is actually supposed to mean (in some cases). I'm not sure if this puts me in a small, advantaged subset of people, or if the stuff I understand is trivial and the 'confusion' is over bigger issues. But, here are my notes on how to understand the notes, in case it helps anyone.

First some background. Cubical type theory is based on cubical sets, which are used in category theory as a model for homotopy. These are in turn based on the cube category, which is a category whose objects are n-dimensional cubes. The 0 cube is a point, the 1 cube is a line segment, the 2 cube is a square, etc.

Cubical sets are presheaves on the cube category. So A : Cube^op -> Sets. This should be thought of as taking the 0-cube to the type A, the 1-cube to identities between values of A, the 2-cube to identities between identities, etc.

So, the core idea behind cubical type theory is that we add the 1-cube, to the formalism. This can be thought of as an interval type 𝕀, which has two elements that are identical to each other (but only propositionally). Functions f : 𝕀 -> A are then like two elements of A together with a proof that they are identical. That is, 𝕀 -> A is like (Σ x y : A. Id A x y), which is the 1-cube portion of the cubical set for A. And we construct higher cubes by iterating the 𝕀 ->. This is like currying the product of intervals that form higher cubes.

The other angle is that when we have 𝕀 -> A, this can be flipped around to get back dependent types, because it can be used in slice categories. So, any particular t : 𝕀 -> A corresponds to an element in the fiber above its two values. So there is a corresponding eq : Id A (t 0) (t 1). This is what cubical type theory actually uses; there's a special lambda that lets us go from "Γ , i : 𝕀 ⊢ t(i) : A" to "Γ ⊢ <i> t(i) : Id A (t 0) (t 1)".

Now, onto the actual notes on the notes.

The first thing to know is the notation A(i0). This is used when A is defined in a context including i : 𝕀, and it means to substitute 0 in for i in A. This is one of the things that isn't explained anywhere in the notes, but reading the code makes it pretty clear that's the intention.

Another thing to know is that the above lambda is not the fully general formulation of things, I think. The code written in cubicaltt the language references an IdP type, and defines the normal identity in terms of it. This is used for type families *fibred over* the interval, which is written in the notes like "Γ, i : 𝕀 ⊢ A". This makes IdP actually a sort of heterogeneous equivalence type, mediated by a specified equivalence of types, and can be thought of as Πi:𝕀.A(i) instead of 𝕀 -> A (perhaps this is where the name IdP comes from? P for Π?). You can mimic this (I think) in something like Agda by defining a type:

IdP {A} {B} (AB : A == B) (x : A) (y : B) = subst id AB x == y

But needless to say, it seems significantly more convenient to work with in the cubical rules. This is something of a disconnect between the implementation and the rules, I should note. The implementation works with typing judgments as things being of type U, and appears to let you form functions 𝕀 -> U, because judgments are behind the scenes in an implementation. This is a slight mismatch, but it's pretty common when moving from typing rules to a computer implementation.

One of the reasons why this comes up is the very last set of rules about "glueing" (sic). Glue is (part of) how univalence is added to the theory; it lets you demonstrate an isomorphism (up to identity) and get an identity. The thing to note here is that there are two "glue"s. One is term-level, and the other is type-level. The notes write them almost identically, but I'll write the type level one with a capital. Anyhow, types built with Glue are an example of something that is fibred over the interval. You demonstrate an Iso(T, A), and using Glue with that lets you build a type family that will reduce to T when i = 1, and A when i = 0. And glue lets you move elements along that isomorphism, so it lets you create identity types that match up corresponding elements of the isomorphic types.

The last very cryptic thing is "formulas" in the context. There is pretty much no explanation for them, but they are used in Glue and comp. If you read some cubicaltt programs, you'll see that they look completely different there, like "i = 0". So what I think they are is a way to do case analysis on interval elements in a controlled way. The rules for using them ensure that you can only 'branch' in ways such that the result of each branch will be judged equal in a joint context. The formula 'i' corresponds to the case 'i = 1' and the formula '1 - i' corresponds to the case 'i = 0'. The weird "u_{φ,ψ}v" notation is a way to collect up two branches into one expression, and it's a value that reduces to u when φ = 1 and v when Ψ = 1.

The last problematic thing about formulas is how you even derive things with them in the context. I think one important thing that isn't explained is that you can probably weaken by formulas in some way. Like 'Γ ⊢ a : A' yields 'Γ, φ ⊢ a : A', possibly with side conditions. Or perhaps 'Γ ⊢ a : A' yields 'Γ, 1 ⊢ a : A'. Structural rules like this aren't given, though.

The last thing to understand is comp, but I already covered that in my last post. However, my explanation there might not give the clearest idea of how things work exactly. Namely, a 'x = y -> P x -> P y' type substitution is not fundamental in cubical type theory. To get that sort of substitution, you first prove 'P x = P y' and then use an operation 'comp' that takes 'A = B' to 'A -> B'. So, you never need to inspect a function like P, you only need to inspect its application to things. You can build expressions that demonstrate (effectively) 'P x = P y' in completely abstract contexts, using (interval) lambda and application, and induction on types is used to figure out how those lambda terms need to compute on values.

The last notational bit about comp is that it binds a variable. The hypotheses of comp formation include 'i : 𝕀' in the context, and then 'comp^i' binds i for its subexpressions. But 'fill', which is defined in terms of comp, and uses a similar notation, does not bind its superscript.

I think that's about it. With the above, I think it's possible to get a feeling for the cubicaltt notes on a sort of operational level (figuring out why the computation rules for comp are what they are is then the difficult part). Whether it's any good as a model of homotopy stuff, I can't say, because I know very little about homotopy/topology. But maybe it can help some other folks like me who are more interested in the computational aspects than a syntactic theory of a branch of mathematics (or maybe it will help the latter folk, too; who knows).