Skip to content

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

  • [i]X{φu}[\overline i] X\{\overline{φ↦ u}\}: extension types, PathP A a b in Agda corresponds to [i]A i{i=0a,i=1b}[i] A~i\{i=0↦ a, i=1↦ b\}.
  • ii is sometimes used to denote i=1i=1 and ¬i¬ i is used to denote i=0i=0.

Flattening

Used in higher inductive type elaboration.

A[i]X{}AΠ(x:X)Yflatten(A):=A\newcommand{\flattenOp}[1]{\textsf{flatten}(#1)} \cfrac{A \ne [\overline i] X\set{\cdots} \quad A\ne Π(x:X)→ Y} {\flattenOp{A} := A}

flatten(X):=[j]Y{φu}flatten([i]X{φu}):=[i,j]Y{φu @ j,φu}\newcommand{\flattenOp}[1]{\textsf{flatten}(#1)} \cfrac {\flattenOp{X}:=[\overline j] Y\set{\overline{φ'↦ u'}}} {\flattenOp{[\overline i] X\set{\overline{φ↦ u}}} := [\overline i,\overline j] Y\set{\overline{φ'↦ u'~@~\overline j},\overline{φ↦ u}}}

flatten(Π(x:X)Y):=Π(x:X)flatten(Y)\newcommand{\flattenOp}[1]{\textsf{flatten}(#1)} \cfrac{} {\flattenOp{Π(x:X)→ Y}:=Π(x:X)→ \flattenOp{Y}}

Example

isProp(A):=Π(a b:A)[i]A{ia,¬ib}isSet(A):=Π(a b:A)isProp([i]A{ia,¬ib})\begin{align*} \textsf{isProp}(A)&:=Π(a~b:A) → [i]A\set{i↦ a,¬ i↦ b}\\ \textsf{isSet}(A)&:=Π(a~b:A)→\textsf{isProp}([i]A\set{i↦ a,¬ i↦ b})\\ \end{align*}

So the normal form of isSet is:

Π(a b:A)Π(p q:[i]A{ia,¬ib})[j]([i]A{ia,¬ib}){jq,¬jp}\begin{align*} Π(a~b:A)&→Π(p~q:[i]A\set{i↦ a,¬ i↦ b})\\ &→ \big[j\big] \big([i]A\set{i↦ a,¬ i↦ b}\big) \Set{j↦ q, ¬ j↦ p}\\ \end{align*}

And flattenOp(isSet(A))\textsf{flattenOp}(\textsf{isSet}(A)) is:

Π(a b:A)Π(p q:[i]A{ia,¬ib})[j i]A{ia,¬ib,jq @ i,¬jp @ i}\begin{align*} Π(a~b:A)&→Π(p~q:[i]A\set{i↦ a,¬ i↦ b})\\ &→ \big[j~i\big] A \Set{i↦ a,¬ i↦ b,j↦ q~@~i, ¬ j↦ p~@~i}\\ \end{align*}

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

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
  }

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.