# Path type constructors in Cubical Type Theory

I have a question about the Path type in CuTT. As far as I know, they are basically functions (not really, since the interval isn't really a type; I'll abuse notation) of the form: $$\textrm{Path} : (i:\mathbb{I}) \to (A:\mathbb{I} \to \textrm{Type}) \to A(\textrm{i0}) \to A(\textrm{i1}) \to \textrm{Type}$$.

Let's suppose for simplicity that our $$A$$ is a constant family. Namely, let's suppose $$A = \mathbb{2}$$, the type with two terms. On each term, we can trivially construct the identity path: $$\operatorname{id} x = \left x$$.

But we can also construct a path by pattern matching, for example, the nontrivial loop on the circle is: $$\textrm{loop} = \left [(i=\textrm{i0}) \Rightarrow \textrm{base}, (i=\textrm{i1}) \Rightarrow \textrm{base}]$$.

Now, my question is: What prevents us from constructing a nontrivial path on other types, like $$\mathbb{2}$$? Consider: $$\textrm{hmm} = \left [(i=\textrm{i0}) \Rightarrow 0_\mathbb{2}, (i=\textrm{i1}) \Rightarrow 1_\mathbb{2}]$$. Is there a mechanism that prevents this?

I can imagine that in the case of $$\textrm{loop} = \left [(i=\textrm{i0}) \Rightarrow 0_\mathbb{2}, (i=\textrm{i1}) \Rightarrow 0_\mathbb{2}]$$, there could be an inference rule stating that this is equal (or homotopic, or whatever) to the identity path, but if the endpoints differ... ?


Some of the stuff you've written isn't quite right.

You cannot just construct paths by pattern matching. What you define by pattern matching are 'systems' or 'partial elements' of a type. So assuming $$i$$ is in scope:

$$[(i = 0) ⇒ 0_2, (i = 1) ⇒ 1_2]$$

is a 'partially defined' value of type $$2$$. The 'partiality' is that you have given values for the endpoints, but not shown how they should be connected. These partial elements can't be used like normal values; they are used with other constructions, like $$\comp$$ to give total values.

However, the rules for $$\comp$$ don't let you just connect up arbitrary points. You have to give an additional, already total value (defined for all $$i$$) that agrees at the points you've specified. In the case of $$\comp$$, your partial value is allowed to use an additional dimension (say $$k$$), and the total value you specify need only agree with the partial value for $$k = 0$$. Then $$\comp$$ constructs the $$k = 1$$ case, so I believe the idea is that you are pushing the total structure along this $$k$$ dimension to fill in the partial structure you've given.

The way things work out, there's no way to give a total witness to complete your partial value and get $$\Path\ 2\ 0_2\ 1_2$$. However (remembering your previous question here), $$\mathsf{not} : 2 → 2$$ is an equivalence, which allows us to define the family:

$$\Not(i) = \Glue\ 2\ \{(i = 0) ⇒ 2, \mathsf{not}; (i = 1) ⇒2,\mathsf{id}\}$$

Which is judgmentally equal to $$2$$ at the endpoints. And it happens that there are ways to obtain $$\Path\ \Not\ 0_2\ 1_2$$, namely:

$$\glue [(i = 0) ⇒ 0_2 , (i = 1) ⇒ 1_2]\ 1_2 : \Not(i)$$

which works because $$\mathsf{not}\ 0_2 = 1_2$$ and $$\mathsf{id}\ 1_2 = 1_2$$. So, $$\glue$$ is another example of something that lets you fill in a partial value, but this time you get to fill in a partial element whose image across some equivalences matches with a specified total value (here $$1_2$$), and the idea is that $$\glue$$ is pulling that total structure back across the equivalences. You get the term of the path type by using the path lambda on this $$\glue$$ term.

Lastly, $$\loop$$ isn't the partial value $$[(i = 0) ⇒ \base, (i = 1) ⇒ \base]$$. It is like an additional constructor of $$S^1$$, where $$\loop(i) : S^1$$, and $$\loop(0) = \loop(1) = \base$$ (where those equalities are judgmental). You can use $$\loop$$ as the total witness to fill in that partial value, for example:

$$\comp^k [(i = 0) ⇒ \base, (i = 1) ⇒ \base]\ (\loop(i))$$

Which is valid because $$\loop$$ matches $$\base$$ at the specified points of the partial value. This expression is equivalent to $$\loop(i)$$, and it is distinct from:

$$\comp^k[(i = 0) ⇒ \base, (i = 1) ⇒ \base]\ \base$$

which is itself equivalent to $$\mathsf{refl}_\base(i) = \base$$.

• Oh I see. So the pattern matching specifies how two paths should connect, and then the composition connects them into single path, provided that you input all the subpaths which agree with the pattern matching. But how does one prove that the comp expression is equivalent to the identity path at base? Sep 1, 2019 at 7:06
• There are probably multiple ways of proving it, and it might even depend on the particulars of which cubical type theory you're using. Here is an example in Agda. Sep 1, 2019 at 14:36