# 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 }$: extension types,
`PathP A a b`

in Agda corresponds to $[i]Ai{i=0↦a,i=1↦b}$. - $i$ is sometimes used to denote $i=1$ and $¬i$ is used to denote $i=0$.

## Flattening

Used in higher inductive type elaboration.

$flatten(A):=AA=[i]X{⋯}A=Π(x:X)→Y $

$flatten([i]X{φ↦u }):=[i,j ]Y{φ_{′}↦u_{′}@j ,φ↦u }flatten(X):=[j ]Y{φ_{′}↦u_{′} } $

$flatten(Π(x:X)→Y):=Π(x:X)→flatten(Y) $

## Example

$isProp(A)isSet(A) :=Π(ab:A)→[i]A{i↦a,¬i↦b}:=Π(ab:A)→isProp([i]A{i↦a,¬i↦b}) $

So the normal form of `isSet`

is:

$Π(ab:A) →Π(pq:[i]A{i↦a,¬i↦b})→[j]([i]A{i↦a,¬i↦b}){j↦q,¬j↦p} $

And $flattenOp(isSet(A))$ is:

$Π(ab:A) →Π(pq:[i]A{i↦a,¬i↦b})→[ji]A{i↦a,¬i↦b,j↦q@i,¬j↦p@i} $

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.