# 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!