Path type constructors in Cubical Type Theory

Question

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<i\right> x$.

But we can also construct a path by pattern matching, for example, the nontrivial loop on the circle is: $\textrm{loop} = \left<i\right> [(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\right> [(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\right> [(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... ?

Answer 1

$\newcommand{\comp}{\mathsf{comp}}$ $\newcommand{\Path}{\mathsf{Path}}$ $\newcommand{\Not}{\mathsf{Not}}$ $\newcommand{\Glue}{\mathsf{Glue}}$ $\newcommand{\glue}{\mathsf{glue}}$ $\newcommand{\base}{\mathsf{base}}$ $\newcommand{\loop}{\mathsf{loop}}$

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$.