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

  • : extension types, PathP A a b in Agda corresponds to .
  • is sometimes used to denote and is used to denote .

Flattening

Used in higher inductive type elaboration.

Example

So the normal form of isSet is:

And is:

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.