A hands-on introduction to cubicaltt

Some months ago I gave a series of hands-on lectures on cubicaltt at Inria Sophia Antipolis that can be found at:

https://github.com/mortberg/cubicaltt/tree/master/lectures

The lectures cover the main features of the system and don’t assume any prior knowledge of Homotopy Type Theory or Univalent Foundations. Only basic familiarity with type theory and proof assistants based on type theory is assumed. The lectures are in the form of cubicaltt files and can be loaded in the cubicaltt proof assistant.

cubicaltt is based on a novel type theory called Cubical Type Theory that provides new ways to reason about equality. Most notably it makes various extensionality principles, like function extensionality and Voevodsky’s univalence axiom, into theorems instead of axioms. This is done such that these principles have computational content and in particular that we can transport structures between equivalent types and that these transports compute. This is different from when one postulates the univalence axiom in a proof assistant like Coq or Agda. If one just adds an axiom there is no way for Coq or Agda to know how it should compute and one looses the good computational properties of type theory. In particular canonicity no longer holds and one can produce terms that are stuck (e.g. booleans that are neither true nor false but don’t reduce further). In other words this is like having a programming language in which one doesn’t know how to run the programs. So cubicaltt provides an operational semantics for Homotopy Type Theory and Univalent Foundations by giving a computational justification for the univalence axiom and (some) higher inductive types.

Cubical Type Theory has a model in cubical sets with lots of structure (symmetries, connections, diagonals) and is hence consistent. Furthermore, Simon Huber has proved that Cubical Type Theory satisfies canonicity for natural numbers which gives a syntactic proof of consistency. Many of the features of the type theory are very inspired by the model, but for more syntactically minded people I believe that it is definitely possible to use cubicaltt without knowing anything about the model. The lecture notes are hence written with almost no references to the model.

The cubicaltt system is based on Mini-TT:

"A simple type-theoretic language: Mini-TT" (2009)
Thierry Coquand, Yoshiki Kinoshita, Bengt Nordström and Makoto Takeya
In "From Semantics to Computer Science; Essays in Honour of Gilles Kahn"

Mini-TT is a variant Martin-Löf type theory with datatypes and cubicaltt extends Mini-TT with:

  1. Path types
  2. Compositions
  3. Glue types
  4. Id types
  5. Some higher inductive types

The lectures cover the first 3 of these and hence correspond to sections 2-7 of:

"Cubical Type Theory: a constructive interpretation of the univalence axiom"
Cyril Cohen, Thierry Coquand, Simon Huber and Anders Mörtberg
To appear in post-proceedings of TYPES 2016
https://arxiv.org/abs/1611.02108

I should say that cubicaltt is mainly meant to be a prototype implementation of Cubical Type Theory in which we can do experiments, however it was never our goal to implement a competitor to any of the more established proof assistants. Because of this there are no implicit arguments, type classes, proper universe management, termination checker, etc… Proofs in cubicaltt hence tend to get quite verbose, but it is definitely possible to do some fun things. See for example:

  • binnat.ctt – Binary natural numbers and isomorphism to unary numbers. Example of data and program refinement by doing a proof for unary numbers by computation with binary numbers.
  • setquot.ctt – Formalization of impredicative set quotients á la Voevodsky.
  • hz.ctt\mathbb{Z} defined as an (impredicative set) quotient of nat * nat.
  • category.ctt – Categories. Structure identity principle. Pullbacks. (Due to Rafaël Bocquet)
  • csystem.ctt – Definition of C-systems and universe categories. Construction of a C-system from a universe category. (Due to Rafaël Bocquet)

For a complete list of all the examples see:

https://github.com/mortberg/cubicaltt/tree/master/examples

For those who cannot live without implicit arguments and other features of modern proof assistants there is now an experimental cubical mode shipped with the master branch of Agda. For installation instructions and examples see:

https://agda.readthedocs.io/en/latest/language/cubical.html
https://github.com/Saizan/cubical-demo

In this post I will give some examples of the main features of cubicaltt, but for a more comprehensive introduction see the lecture notes. As cubicaltt is an experimental prototype things can (and probably will) change in the future (e.g. see the paragraph on HITs below).

The basic type theory

The basic type theory on which cubicaltt is based has Π and ∑ types (with eta and surjective pairing), a universe U, datatypes, recursive definitions and mutually recursive definitions (in particular inductive-recursive definitions). Note that general datatypes and (mutually recursive) definitions are not part of the version of Cubical Type Theory in the paper.

Below is an example of how natural numbers and addition are defined:

data nat = zero
         | suc (n : nat)

add (m : nat) : nat -> nat = split
  zero -> m
  suc n -> suc (add m n)

If one loads this in the cubicaltt read-eval-print-loop one can compute things:

> add (suc zero) (suc zero)
EVAL: suc (suc zero)

Path types

The homotopical interpretation of equality tells us that we can think of an equality proof between a and b in a type A as a path between a and b in a space A. cubicaltt takes this literally and adds a primitive Path type that should be thought of as a function out of an abstract interval \mathbb{I} with fixed endpoints.

We call the elements of the interval \mathbb{I} names/directions/dimensions and typically use i, j, k to denote them. The elements of the interval \mathbb{I} are generated by the following grammar (where dim is a dimension like i, j, k…):

r,s := 0
     | 1
     | dim
     | - r
     | r /\ s
     | r \/ s

The endpoints are 0 and 1, – corresponds to symmetry (r in \mathbb{I} is mapped to 1-r), while /\ and \/ are so called “connections”. The connections can be thought of mapping r and s in \mathbb{I} to min(r,s) and max(r,s) respectively. As Path types behave like functions out of the interval there is both path abstraction and application (just like for function types). Reflexivity is written:

refl (A : U) (a : A) : Path A a a = <i> a

and corresponds to a constant path:

        <i> a
   a -----------> a

with the intuition is that <i> a is a function \(i : \mathbb{I}) -> a. However for deep reasons the interval isn’t a type (as it isn’t fibrant) so we cannot write functions out of it directly and hence we have this special notation for path abstraction.

If we have a path from a to b then we can compute its left end-point by applying it to 0:

face0 (A : U) (a b : A) (p : Path A a b) : A = p @ 0

This is of course convertible to a. We can also reverse a path by using symmetry:

sym (A : U) (a b : A) (p : Path A a b) : Path A b a =
  <i> p @ -i

Assuming that some arguments could be made implicit this satisfies the equality

sym (sym p) == p

judgmentally. This is one of many examples of equalities that hold judgmentally in cubicaltt but not in standard type theory where sym would be defined by induction on p. This is useful for formalizing mathematics, for example we get the judgmental equality C^op^op == C for a category C that cannot be obtained in standard type theory with the usual definition of category without using any tricks (see opposite.ctt for a formal proof of this).

We can also directly define cong (or ap or mapOnPath):

cong (A B : U) (f : A -> B) (a b : A) (p : Path A a b) :
     Path B (f a) (f b) = <i> f (p @ i)

Once again this satisfies some equations judgmentally that we don’t get in standard type theory where this would have been defined by induction on p:

cong id p == p
cong g (cong f p) == cong (g o f) p

Finally the connections can be used to construct higher dimensional cubes from lower dimensional ones (e.g. squares from lines). If p : Path A a b then <i j> p @ i /\ j is the interior of the square:

                  p
        a -----------------> b
        ^                    ^
        |                    |
        |                    |
  <j> a |                    | p
        |                    |
        |                    |
        |                    |
        a -----------------> a
                <i> a

Here i corresponds to the left-to-right dimension and j corresponds to the down-to-up dimension. To compute the left and right sides just plug in i=0 and i=1 in the term inside the square:

<j> p @ 0 /\ j = <j> p @ 0 = <j> a   (p is a path from a to b)
<j> p @ 1 /\ j = <j> p @ j = p       (using eta for Path types)

These give a short proof of contractibility of singletons (i.e. that the type (x : A) * Path A a x is contractible for all a : A), for details see the lecture notes or the paper. Because connections allow us to build higher dimensional cubes from lower dimensional ones they are extremely useful for reasoning about higher dimensional equality proofs.

Another cool thing with Path types is that they allow us to give a direct proof of function extensionality by just swapping the path and lambda abstractions:

funExt (A B : U) (f g : A -> B)
       (p : (x : A) -> Path B (f x) (g x)) :
       Path (A -> B) f g = <i> \(a : A) -> (p a) @ i

To see that this makes sense we can compute the end-points:

(<i> \(a : A) -> (p a) @ i) @ 0 = \(a : A) -> (p a) @ 0
                                = \(a : A) -> f a
                                = f

and similarly for the right end-point. Note that the last equality follows from eta for Π types.

We have now seen that Path types allows us to define the constants of HoTT (like cong or funExt), but when doing proofs with Path types one rarely uses these constants explicitly. Instead one can directly prove things with the Path type primitives, for example the proof of function extensionality for dependent functions is exactly the same as the one for non-dependent functions above.

We cannot yet prove the principle of path induction (or J) with what we have seen so far. In order to do this we need to be able to turn any path between types A and B into a function from A to B, in other words we need to be able to define transport (or cast or coe):

transport : Path U A B -> A -> B

Composition, filling and transport

The computation rules for the transport operation in cubicaltt is introduced by recursion on the type one is transporting in. This is quite different from traditional type theory where the identity type is introduced as an inductive family with one constructor (refl). A difficulty with this approach is that in order to be able to define transport in a Path type we need to keep track of the end-points of the Path type we are transporting in. To solve this we introduce a more general operation called composition.

Composition can be used to define the composition of paths (hence the name). Given paths p : Path A a b and q : Path A b c the composite is obtained by computing the missing top line of this open square:

        a                   c
        ^                   ^
        |                   |
        |                   |
  <j> a |                   | q
        |                   |
        |                   |
        |                   |
        a ----------------> b
                p @ i

In the drawing I’m assuming that we have a direction i : \mathbb{I} in context that goes left-to-right and that the j goes down-to-up (but it’s not in context, rather it’s implicitly bound by the comp operation). As we are constructing a Path from a to c we can use the i and put p @ i as bottom. The code for this is as follows:

compPath (A : U) (a b c : A)
  (p : Path A a b) (q : Path A b c) : Path A a c =
   <i> comp (<_> A) (p @ i)
                    [ (i = 0) -> <j> a
                    , (i = 1) -> q ]

One way to summarize what compositions gives us is the so called “box principle” that says that “any open box has a lid”. Here “box” means (n+1)-dimensional cube and the lid is an n-dimensional cube. The comp operation takes as second argument the bottom of the box and then a list of sides. Note that the collection of sides doesn’t have to be exhaustive (as opposed to the original cubical set model) and one way to think about the sides is as a collection of constraints that the resulting lid has to satisfy. The first argument of comp is a path between types, in the above example this path is constant but it doesn’t have to be. This is what allows us to define transport:

transport (A B : U) (p : Path U A B) (a : A) : B =
  comp p a []

Combining this with the contractibility of singletons we can easily prove the elimination principle for Path types. However the computation rule does not hold judgmentally. This is often not too much of a problem in practice as the Path types satisfy various judgmental equalities that normal Id types don’t. Also, having the possibility to reason about higher equalities directly using path types and compositions is often very convenient and leads to very nice and new ways to construct proofs about higher equalities in a geometric way by directly reasoning about higher dimensional cubes.

The composition operations are related to the filling operations (as in Kan simplicial sets) in the sense that the filling operations takes an open box and computes a filler with the composition as one of its faces. One of the great things about cubical sets with connections is that we can reduce the filling of an open box to its composition. This is a difference compared to the original cubical set model and it provides a significant simplification as we only have to explain how to do compositions in open boxes and not also how to fill them.

Glue types and univalence

The final main ingredient of cubicaltt are the Glue types. These are what allows us to have a direct algorithm for composition in the universe and to prove the univalence axiom. These types add the possibility to glue types along equivalences (i.e. maps with contractible fibers) onto another type. In particular this allows us to directly define one of the key ingredients of the univalence axiom:

ua (A B : U) (e : equiv A B) : Path U A B =
  <i> Glue B [ (i = 0) -> (A,e)
             , (i = 1) -> (B,idEquiv B) ]

This corresponds to the missing line at the top of:

        A           B
        |           |
      e |           | idEquiv B
        |           |
        V           V
        B --------> B
              B

The sides of this square are equivalences while the bottom and top are lines in direction i (so this produces a path from A to B as desired).

We have formalized three proofs of the univalence axiom in cubicaltt:

  1. A very direct proof due to Simon Huber and me using higher dimensional glueing.
  2. The more conceptual proof from section 7.2 of the paper in which we show that the unglue function is an equivalence (formalized by Fabian Ruch).
  3. A proof from ua and its computation rule (uabeta). Both of these constants are easy to define and are sufficient for the full univalence axiom as noted in a post by Dan Licata on the HoTT google group.

All of these proofs can be found in the file univalence.ctt and are explained in the paper (proofs 1 and 3 are in Appendix B).

Note that one often doesn’t need full univalence to do interesting things. So just like for Path types it’s often easier to just use the Glue primitives directly instead of invoking the full univalence axiom. For instance if we have proved that negation is an involution for bool we can directly get a non-trivial path from bool to bool using ua (which is just a Glue):

notEq : Path U bool bool = ua boob bool notEquiv

And we can use this non-trivial equality to transport true and compute the result:

> transport notEq true
EVAL: false

This is all that the lectures cover, in the rest of this post I will discuss the two extensions of cubicaltt from the paper and their status in cubicaltt.

Identity types and higher inductive types

As pointed out above the computation rule for Path types doesn’t hold judgmentally. Luckily there is a neat trick due to Andrew Swan that allows us to define a new type that is equivalent to Path A a b for which the computation rule holds judgmentally. For details see section 9.1 of the paper. We call this type Id A a b as it corresponds to Martin-Löf’s identity type. We have implemented this in cubicaltt and proved the univalence axiom expressed exclusively using Id types, for details see idtypes.ctt.

For practical formalizations it is probably often more convenient to use the Path types directly as they have the nice primitives discussed above, but the fact that we can define Id types is very important from a theoretical point of view as it shows that cubicaltt with Id is really an extension of Martin-Löf type theory. Furthermore as we can prove univalence expressed using Id types we get that any proof in univalent type theory (MLTT extended with the univalence axiom) can be translated into cubicaltt.

The second extension to cubicaltt are HITs. We have a general syntax for adding these and some of them work fine on the master branch, see for example:

  • circle.ctt – The circle as a HIT. Computation of winding numbers.
  • helix.ctt – The loop space of the circle is equal to Z.
  • susp.ctt – Suspension and n-spheres.
  • torsor.ctt – Torsors. Proof that S1 is equal to BZ, the classifying
    space of Z. (Due to Rafaël Bocquet)
  • torus.ctt – Proof that Torus = S1 * S1 in only 100 loc (due to Dan
    Licata).

However there are various known issues with how the composition operations compute for recursive HITs (e.g. truncations) and HITs where the end-points contain function applications (e.g. pushouts). We have a very experimental branch that tries to resolve these issues called “hcomptrans”. This branch contains some new (currently undocumented) primitives that we are experimenting with and so far it seems like these are solving the various issues for the above two classes of more complicated HITs that don’t work on the master branch. So hopefully there will soon be a new cubical type theory with support for a large class of HITs.

That’s all I wanted to say about cubicaltt in this post. If someone plays around with the system and proves something cool don’t hesitate to file a pull request or file issues if you find some bugs.

This entry was posted in Uncategorized. Bookmark the permalink.

8 Responses to A hands-on introduction to cubicaltt

  1. Mike Shulman says:

    Thanks for this very nice introduction! It’s exciting that we have cubicaltt to experiment with.

    I find it interesting that you say that connections make things simpler; I would rather do without them if I could. The connections introduce lots of judgmental equalities (the axioms of a de Morgan algebra) that don’t feel “computational” to me — in particular, they’re not “directed” — whereas box-filling is an operation that could be computed. It seems that the only real reason that connections are needed is to make singletons contractible, and the algebraic theory of a de Morgan algebra seems like a lot of complicated judgmental machinery in order to achieve that simple result. Is there a theoretical obstacle to doing cubical type theory without connections, or is it just a choice that could be made either way?

    I also find it conceptually unsatisfying that function extensionality arises by simple rearranging of lambdas — and hence holds “judgmentally” in some sense — whereas univalence requires postulating these new “Glue” types. I wish there were some way to make univalence hold judgmentally too, but I haven’t been able to think of any such, and I presume no one else has either. Would it at least be possible to replace the Glue types with operations that literally say “every equivalence gives rise to a path in the universe” and so on, rather than transporting an existing path along an equivalence?

    • mortberg says:

      Thank you Mike! I was hoping someone would ask about the connections. In the beginning when we switched to cubical sets with connections I also felt like they were quite complicated. But the key point is that they allow us to reduce filling to composition which is a huge simplification for the model as we now only have to define the algorithm for composition and get filling for free. In the BCH cubical set model this is not the case and for Pi one has to first define composition and then filling (see Thm. 6.2 in the BCH paper). The same goes for the symmetries, without them we have to explain how to do comp/fill both up and down. The algorithms are of course the same up to symmetry, but without symmetries we need to give both of them. So it seems to me like the more structure you have in the base site the simpler the comp/fill structures become for your cubical sets. As comp/fill are the most subtle part of the system I think you really want to have them as simple as possible if you want to construct a type theory from the model.

      I should also say that for formalization in cubicaltt the connections are very useful. Once one get used to them they are quite ubiquitous, especially when doing higher dimensional compositions. I have a hard time imagining using a cubical type theory without them these days. One could of course do the proofs like in traditional type theory using only J, but as we don’t have the computation rule for J judgmentally this is not very nice. Also it is not very fun to do the same old proofs in cubicaltt, it is much more fun to do things with the new primitives cubicaltt gives us (I tried to illustrate this in some of the exercises in the lecture notes). I also feel like that there must be some examples of where the proof using J is very long and complicated, but where the proof using comp and connections is a lot simpler.

      I’ll say something about Glue types in another comment later.

      • Mike Shulman says:

        I’m allergic to any mention of “constructing a type theory from the (i.e.from one specific) model”. (-: In my view, a respectable type theory should have models in a general class of categories. This is one of the things that makes me most suspicious of cubical type theory, and hesitant to use it for any substantial synthetic homotopy theory. We understand (modulo initiality theorems and strictness of the universe) how traditional MLTT has semantics in any nice simplicial model category, in particular including models for any locally cartesian closed locally presentable (\infty,1)-category. But such a result still seems to be lacking for cubical type theories, and it seems to me that the strict de Morgan algebra structure of the connections would make it harder. If we left them out, we could in principle interpret the cubical interval as an arbitrary interval object (although we’d still have to deal with uniformity).

        • mortberg says:

          I’m allergic to type theories that don’t enjoy canonicity. In my view, a respectable type theory shouldn’t have any axioms. 🙂 More seriously though, I haven’t been thinking much about more general classes of models for cubicaltt yet, but as you probably know there is some work in this direction (Orton & Pitts, Sattler, Guarded CTT…). But as far as I know the connections seem necessary in order to give a reasonably simple operational semantics for comp/fill when formulated the way we do things. There is also the computational higher-dimensional type theory of Angiuli, Harper and Wilson that uses a different notion of composition structure where filling can be reduced to comp without connections, but as far as I know they haven’t gotten the universe to work yet… Designing cubical type theories is a bit like chemistry, there are a lot of things you can throw in the mix but if you don’t get things right the experiment doesn’t work out (or it blows up in your face).

          I guess one could imagine designing a version of cubicaltt without connections. The main drawback for the formulation of the type theory would be that we have to do twice as much work for some type formers (I guess as least for Pi and Glue) as we have to define first the equality judgment for comp and then fill. But it could maybe work out. However as I said in my previous message the connections are very useful for practical formalization. I rarely formalize any statement without at least one connection in it when working in cubicaltt, so removing them would make working in the type theory a lot less convenient and fun. So maybe one should first figure out if it’s possible or not to interpret cubicaltt in the classes of models you are interested in before throwing out the connections.

          • Mike Shulman says:

            I do appreciate the importance of canonicity! I have faith that it’s possible to design a type theory that both of us would consider respectable. I certainly see that from an implementation perspective, it would be more work to define how fill computes than to include connections; but conceptually I think I would find it simpler, since the computation laws feel “secondary” relative to the specification of the terms (even though formally, in dependent type theory all the judgments are bound up in one big mutual induction).

            Can you point to some good examples of where you’ve found connections useful in formalization?

    • mortberg says:

      About Glue types: I think it is interesting that function extensionality has this very simple proof while univalence is very complicated. Maybe one hint at why this is the case comes from looking at the attempts to make an OTT style theory higher dimensional (i.e. define HOTT 🙂 ). In OTT the equality judgments are defined by induction on the type (just like in cubicaltt). For Pi types the equality is defined to be extensional (in the sense of function extensionality) and this is not too complicated, however when trying to make the equality for the universe into something like univalence in the non-truncated theory one seem to end up with a combinatorial explosion. As far as I know noone has figured out a way to do this yet.

      The Glue types are used for 2 things in cubicaltt:

      1. Prove univalence
      2. Define composition for U

      Is it clear that we can do 2 from what you suggest? If not we would have to define this separately which is about as complicated as composition for Glue…

      • Mike Shulman says:

        In principle I find it clear that it should be possible. For instance, consider composition of a 1-box in U with sides p,q,r. In CCHM cubical type theory, we do this by making the paths p and r into equivalences and using a Glue type to transport q along these equivalences. In my proposal, we would do it by making all three of p,q,r into equivalences, composing these equivalences as equivalences, and then making the result back into a path. Higher composition is, I agree, much more combinatorially complicated: for instance, a square in U corresponds to a homotopy between the top-right and bottom-left composites of equivalences, and to compose a 2-box in U we need to compose five of these homotopies whiskered in appropriate ways. But in principle it should be possible, because there is an \infty-groupoid whose objects are \infty-groupoids, whose morphisms are equivalences, whose 2-morphisms are homotopies, etc. Making this precise is basically the problem of relating globular and cubical notions of \infty-groupoid explicitly and algebraically, which is hard but should be possible. (-:

  2. Mike Shulman says:

    Here is another reason that I dislike connections. One of the things I like so much about Book HoTT is how we don’t have to stipulate that types are \infty-groupoids; we just decline to assert UIP, and all the structure of an \infty-groupoid emerges automatically from J. I find this philosophically very appealing: it means that the notion of \infty-groupoid is implicit in the very notion of “equality”.

    At first glance, cubical type theory destroys all this, since it builds all the higher-dimensional structure of an \infty-groupoid into the composition operations. But there is a different way of looking at cubical type theory that retains some of the pleasing philosophy; I’m not sure who first explained this to me, but I’ve only recently come to really appreciate it.

    In Book HoTT, operations such as transport and path composition are defined by induction on the paths; thus they reduce when the paths are reflexivity, but are stuck otherwise. However, we can prove (as in Chapter 2) that they also reduce typally (i.e. up to an identification rather than a judgmental equality) based on the form of the type we are composing in or transporting along. Moreover, experience suggests that these “reductions” are used more often than the reduction on reflexivity paths, so it’s natural to “change the rules” to make the type-based reductions judgmental instead of the path-based ones.

    On the surface this doesn’t seem to require anything higher-dimensional, but it turns out to give rise to box filling filling/composition in all dimensions because of path-types: transport in \mathrm{Path}_A reduces to 1-box filling in A, 1-box filling in \mathrm{Path}_A reduces to 2-box filling in A, and so on. So once again the \infty-groupoid structure “arises automatically” rather than being “put in by hand because we want types to be \infty-groupoids”; the only difference is that this “arising” happens at the level of the design of the type theory rather than when working inside an already extant theory.

    However, while it’s quite easy to explain/motivate box-filling in addition to mere composition this way, I have a harder time thinking of how to motivate connections.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s