Elaboration of path constructors ​

This is not a blog post, but a reference for developers and type theory implementers.

Content below assumes knowledge on cubical type theory, for example the extension type and higher inductive types.

Syntax ​

• $[\overline{i}]X\{\overline{\phi \mapsto u}\}$: extension types, PathP A a b in Agda corresponds to $[i]Ai\{i=0\mapsto a,i=1\mapsto b\}$.
• $i$ is sometimes used to denote $i=1$ and $\neg i$ is used to denote $i=0$.

Flattening ​

Used in higher inductive type elaboration.

$$\frac{A\ne [\overline{i}]X\{\cdots \}A\ne \Pi (x:X)\to Y}{\text{flatten}(A):=A}$$

$$\frac{\text{flatten}(X):=[\overline{j}]Y\{\overline{{\phi }^{\prime }\mapsto u^{\prime }}\}}{\text{flatten}([\overline{i}]X\{\overline{\phi \mapsto u}\}):=[\overline{i},\overline{j}]Y\{\overline{{\phi }^{\prime }\mapsto u^{\prime }@\overline{j}},\overline{\phi \mapsto u}\}}$$

$$\frac{}{\text{flatten}(\Pi (x:X)\to Y):=\Pi (x:X)\to \text{flatten}(Y)}$$

Example ​

$$\begin{array}{rl}\text{isProp}(A)& :=\Pi (ab:A)\to [i]A\{i\mapsto a,\neg i\mapsto b\}\\ \text{isSet}(A)& :=\Pi (ab:A)\to \text{isProp}([i]A\{i\mapsto a,\neg i\mapsto b\})\end{array}$$

So the normal form of isSet is:

$$\begin{array}{rl}\Pi (ab:A)& \to \Pi (pq:[i]A\{i\mapsto a,\neg i\mapsto b\})\\ & \to \left[j\right]([i]A\{i\mapsto a,\neg i\mapsto b\})\left\{j\mapsto q,\neg j\mapsto p\right\}\end{array}$$

And $\text{flattenOp}(\text{isSet}(A))$ is:

$$\begin{array}{rl}\Pi (ab:A)& \to \Pi (pq:[i]A\{i\mapsto a,\neg i\mapsto b\})\\ & \to \left[ji\right]A\left\{i\mapsto a,\neg i\mapsto b,j\mapsto q@i,\neg j\mapsto p@i\right\}\end{array}$$

So for example, set truncation from HoTT looks like this:

data SetTrunc (A : Type)
| mk : A -> SetTrunc A
| trunc : isSet (SetTrunc A)

data SetTrunc (A : Type)
| mk : A -> SetTrunc A
| trunc : isSet (SetTrunc A)

The trunc constructor is elaborated to cubical syntax by flattening the type and attach the partial on the return type to the constructor, something like this:

trunc : Π (a b : SetTrunc A)
    -> (p q : a = b)
    -> (j i : I) -> SetTrunc A
  { i = 1 -> a
  ; i = 0 -> b
  ; j = 1 -> q @ i
  ; j = 0 -> p @ i
  }

trunc : Π (a b : SetTrunc A)
    -> (p q : a = b)
    -> (j i : I) -> SetTrunc A
  { i = 1 -> a
  ; i = 0 -> b
  ; j = 1 -> q @ i
  ; j = 0 -> p @ i
  }

Aya is currently working on the so-called IApplyConfluence problem for recursive higher inductive types like SetTrunc, see this question which is a problem I'm wrapping my head around at the moment. More details will be posted later.