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.