Extension types

In this tutorial, we introduce a simple extension to the traditional "path type" in cubical type theory -- the extension type. Basic knowledge on cubical type theory is assumed. Some primitive definitions:

prim I prim coe
prim intervalInv
prim intervalMax
inline def ~ ⇒ intervalInv
variable A B : Type
def Path (A : I → Type) (a : A 0) (b : A 1)
   ⇒ ⟦ i ⟧ A i { i := b | ~ i := a }
//     ^^^^^^^^^^^^^^^^^^^^^^
//    this is an extension type
def infix = {A : Type} ⇒ Path (fn x ⇒ A)
def refl {a : A} : a = a ⇒ fn i ⇒ a

The extension type is essentially a generalized version of the path type, which can be n-dimensional instead of just 1-dimensional like the path type, and the boundaries can be arbitrarily specified. For example, a = b in cubical type theory is essentially the same as [| i |] A { i := b | ~ i := a }, where A is the type of a and b. That i := b says "when the path is applied by 1, it should return b", and in general, φ := u says "when the path application makes φ equal to 1, then the path should return u".

When there are no boundaries specified, the extension type can be written as [| i |] A. For higher dimensional extension types, one write [| i j k |] A etc.

As a simple exercise, explain how ~ i := a works. Hint: ~ i is the same as 1 - i.

So, how are these types superior to the traditional path type?

Examples

The extension type reduces the unification burden. This is a traditional definition of path symmetry:

example def sym {a b : A} (p : a = b) : b = a ⇒ fn i ⇒ p (~ i)

Note that it has two implicit arguments, which will be figured out by the type checker. However, with the extension type, we do not have to specify the boundaries!

def sym (p : ⟦ i ⟧ A) : p 1 = p 0 ⇒ fn i ⇒ p (~ i)

Yes, by that we have inverted the path! This also happens to cong, which is renamed to pmap in Aya:

def pmap (f : A → B) (p : ⟦ i ⟧ A) : f (p 0) = f (p 1)
   ⇒ fn i ⇒ f (p i)

Now, let's take a look at the transitivity of paths:

def cast (p : A ↑ = B) : A → B ⇒ coe 0 1 (fn i ⇒ p i)
example def concat {a b c : A} (p : a = b) (q : b = c) : a = c ⇒
  cast (fn i ⇒ a = q i) p

We can make p boundary-free, and use p 1 as a replacement of b:

def concat (p : ⟦ i ⟧ A) (q : ⟦ i ⟧ A { ~ i := p 1 }) : p 0 = q 1
   ⇒ cast (fn i ⇒ p 0 = q i) p

Now we can say bye bye to these implicit arguments!

Higher inductive types

Higher inductive types in Aya are also defined using the extension type syntax. The Agda-style syntax is working in progress.

We first introduce a convenient function for "both boundaries":

inline def ∂ (i : I) ⇒ intervalMax i (~ i)

This function should be used when opposite boundaries are equal, for example, we may write the type of refl as:

example def Refl {a : A} ⇒ ⟦ i ⟧ A { ∂ i := a }

The simplest example is the definition of circles:

example open data S¹
| base
| loop : base = base

Aya will slightly analyze the definition and transform loop : base = base into loop (i : I) where either $i = 0$ or $i = 1$ makes it reduce to base:

open data S¹
| base
| loop (i : I) { ∂ i := base }

This means that loop i is equal to base when i is equal to 0 or 1. Aya has nice coercive subtyping between path and pi types, so we may say:

example def test : base = base ⇒ loop

As another example, the definition of torus in cubical Agda has a mysterious type for the face constructor, which looks like PathP (\i -> line1 i = line1 i) line2 line2. This is quite hard for beginners to read, but it can be made clear using the extension type:

open data T²
| point
| line1 (i : I) { ∂ i := point }
| line2 (i : I) { ∂ i := point }
| face (i j : I) { ∂ i := line2 j | ∂ j := line1 i }

The traditional type still works (due to a small problem we have to manually eta-expand it a little for now):

example def traditional
  : Path (\i ⇒ line1 i = line1 i) line2 line2
  ⇒ fn i ⇒ face i

For the record, one may also work with the HoTT-book definition of torus:

example data Torus
| pt
| l1 : pt = pt
| l2 : pt = pt
| tub : concat l1 l2 = concat l2 l1

But this is less pleasant to work with, because the boundaries are using concat which is a complicated definition.

Off-topic interesting results

There is a higher inductive type that is essentially the same as the interval type:

open data Interval
| left | right
| line : left = right

The elimination rule of Interval implies function extensionality. To avoid cheating, we will not use path application or path abstraction in the proof, to imitate pure MLTT with HITs.

private def lemma (f g : A → B) (∀ x → f x = g x) : Interval → A → B
| f, _, _, left, a ⇒ f a
| _, g, _, right, a ⇒ g a
| _, _, p, line i, a ⇒ p a i

def funExtFromInterval (f g : A → B) (p : ∀ x → f x = g x) : f = g ⇒
  pmap (lemma f g p) line

Note that even though we are using equation combinators like pmap which are implemented using path application and abstraction, it is not considered cheating because these are already theorems in MLTT anyway. One may also prove them by path induction in cubical type theory, but why bother!