Cubical Type Theory

Stream: general

[Tim Daly]

I'm watching Buchholtz's talk at the CMU conference. From what I've studied about Cubical Type Theory I'm kinda confused.

1) From topology, a cube is isomorphic to a sphere
2) a cubical type can be mapped to a sphere where one corner is at the 'north' pole
3) a cubical type defines maps and their inverses for each corner.
4) start at the 'north' pole corner, walk a face forward, composing the forward maps.
5) after traversing one face (4 compositions) you end up at the 'north' pole again
6) start at the 'north' pole corner, walk a face backward, composing the inverse maps.
7) after traversing the same face (4 compositions) you end up at the 'north' pole again
8) so the forward and inverse functions collapse into the identity function on the 'north' pole point.
9) collapse the face into the identity function
10) iterate the above for every face
11) therefore, the cube is just the identity function

Clearly I'm confused because, in the course I took on Cubical Type Theory, nobody seemed to
view the cube as collapsing to the identity function.
Which step of reasoning is wrong?

[Jason Rute]

Cubical type theory is an extension of Martin Löf Type theory. It adds more rules which allow one to prove certain things are equal. It lets you prove the univalence axiom (in a constructive way) in Homotopy type theory. The name "cubical" comes from the concept of "cubical sets". I don't know what you mean by "Cubical type" in (2), but I think you are talking about something different. Cubical Type Theory is also a fairly recent invention, so I don't think you took a course on it, or if you did it was a different subject by the same name.

[Jason Rute]

Sorry. I think I was mistaken. Forget everything I just said.

[Jason Rute]

I don't know if this helps, but with a cube, you can collapse (or whatever the correct homotopy term is) all but one of the faces together, but not the final face. The same goes for a square. You can collapse all the edges together save for the last one. Indeed in HoTT, the "circle" S^1 is just a point and a loop (so basically a square where three of the four sides are collapsed together), but it is not contractible. (This sort of thing confused me for a while until I realized that a contraction needs to be uniform/continuous. There is not a uniform/continuous contraction which takes all points to the "north pole" of a cube.)

[Ulrik Buchholtz]

The “cubes” in cubical type theory are solid cubes., so they're geometrically contractible. This is in fact necessary so that cubical sets can model homotopy types. (Cf. solid simplices and simplicial sets.) The main ingredient for both simplices and cubes is that the 1-dimensional object is an interval with which we can model path types. They differ in how they extend to higher-dimensional shapes.

[Jason Rute]

Ok, I think it is safe to ignore everything I've written in this topic... :face_palm: Thanks Ulrik for providing actual expert insight.