# Cubical¶

The Cubical mode extends Agda with a variety of features from Cubical Type Theory. In particular, computational univalence and higher inductive types which hence gives computational meaning to Homotopy Type Theory and Univalent Foundations. The version of Cubical Type Theory that Agda implements is a variation of the CCHM Cubical Type Theory where the Kan composition operations are decomposed into homogeneous composition and generalized transport. This is what makes the general schema for higher inductive types work, following the CHM paper.

To use the cubical mode Agda needs to be run with the
`--cubical`

command-line-option or with ```
{-#
OPTIONS --cubical #-}
```

at the top of the file. There is also a
variant of the cubical mode, activated using
`--erased-cubical`

, which is described
below.

The cubical mode adds the following features to Agda:

An interval type and path types

Generalized transport (

`transp`

)Partial elements

Homogeneous composition (

`hcomp`

)Glue types

Higher inductive types

Cubical identity types

There is a standard `agda/cubical`

library for Cubical Agda
available at https://github.com/agda/cubical. This documentation uses
the naming conventions of this library, for a detailed list of all of
the built-in Cubical Agda files and primitives see
Appendix: Cubical Agda primitives. The main design choices of the core part of the
library are explained in
https://homotopytypetheory.org/2018/12/06/cubical-agda/
(lagda rendered version:
https://ice1000.org/2018/12-06-CubicalAgda.html).

The recommended way to get access to the Cubical primitives is to add
the following to the top of a file (this assumes that the
`agda/cubical`

library is installed and visible to Agda).

```
{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything
```

For detailed install instructions for `agda/cubical`

see:
https://github.com/agda/cubical/blob/master/INSTALL.md. In order to
make this library visible to Agda add
`/path/to/cubical/cubical.agda-lib`

to `.agda/libraries`

and
`cubical`

to `.agda/defaults`

(where `path/to`

is the absolute
path to where the `agda/cubical`

library has been installed). For
details of Agda’s library management see Library Management.

Expert users who do not want to rely on `agda/cubical`

can just add
the relevant import statements at the top of their file (for details
see Appendix: Cubical Agda primitives). However, for beginners it is
recommended that one uses at least the core part of the
`agda/cubical`

library.

There is also an older version of the library available at https://github.com/Saizan/cubical-demo/. However this is relying on deprecated features and is not recommended to use.

## The interval and path types¶

The key idea of Cubical Type Theory is to add an interval type ```
I :
IUniv
```

(the reason this is in a special sort `IUniv`

is because it
doesn’t support the `transp`

and `hcomp`

operations). A variable
`i : I`

intuitively corresponds to a point in the real unit interval. In an empty context,
there are only two values of type `I`

: the two endpoints of the
interval, `i0`

and `i1`

.

```
i0 : I
i1 : I
```

Elements of the interval form a De Morgan algebra, with minimum
(`∧`

), maximum (`∨`

) and negation (`~`

).

```
_∧_ : I → I → I
_∨_ : I → I → I
~_ : I → I
```

All the properties of De Morgan algebras hold definitionally. The
endpoints of the interval `i0`

and `i1`

are the bottom and top
elements, respectively.

```
i0 ∨ i = i
i ∨ i1 = i1
i ∨ j = j ∨ i
i0 ∧ i = i0
i1 ∧ i = i
i ∧ j = j ∧ i
~ (~ i) = i
i0 = ~ i1
~ (i ∨ j) = ~ i ∧ ~ j
~ (i ∧ j) = ~ i ∨ ~ j
```

The core idea of Homotopy Type Theory and Univalent Foundations is a
correspondence between paths (as in topology) and (proof-relevant)
equalities (as in Martin-Löf’s identity type). This correspondence is
taken very literally in Cubical Agda where a path in a type `A`

is
represented like a function out of the interval, `I → A`

. A
path type is in fact a special case of the more general built-in
heterogeneous path types:

```
-- PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ
-- Non dependent path types
Path : ∀ {ℓ} (A : Set ℓ) → A → A → Set ℓ
Path A a b = PathP (λ _ → A) a b
```

The central notion of equality in Cubical Agda is hence heterogeneous
equality (in the sense of `PathOver`

in HoTT). To define paths we
use λ-abstractions and to apply them we use regular application. For
example, this is the definition of the constant path (or proof of
reflexivity):

```
refl : ∀ {ℓ} {A : Set ℓ} {x : A} → Path A x x
refl {x = x} = λ i → x
```

Although they use the same syntax, a path is not exactly the same as a function. For example, the following is not valid:

```
refl : ∀ {ℓ} {A : Set ℓ} {x : A} → Path A x x
refl {x = x} = λ (i : I) → x
```

Because of the intuition that paths correspond to equality ```
PathP (λ
i → A) x y
```

gets printed as `x ≡ y`

when `A`

does not mention
`i`

. By iterating the path type we can define squares, cubes, and
higher cubes in Agda, making the type theory cubical. For example a
square in `A`

is built out of 4 points and 4 lines:

```
Square : ∀ {ℓ} {A : Set ℓ} {x0 x1 y0 y1 : A} →
x0 ≡ x1 → y0 ≡ y1 → x0 ≡ y0 → x1 ≡ y1 → Set ℓ
Square p q r s = PathP (λ i → p i ≡ q i) r s
```

Viewing equalities as functions out of the interval makes it possible to do a lot of equality reasoning in a very direct way:

```
sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → y ≡ x
sym p = λ i → p (~ i)
cong : ∀ {ℓ} {A : Set ℓ} {x y : A} {B : A → Set ℓ} (f : (a : A) → B a) (p : x ≡ y)
→ PathP (λ i → B (p i)) (f x) (f y)
cong f p i = f (p i)
```

Because of the way functions compute these satisfy some new definitional equalities compared to the standard Agda definitions:

```
symInv : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
symInv p = refl
congId : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → cong (λ a → a) p ≡ p
congId p = refl
congComp : ∀ {ℓ} {A B C : Set ℓ} (f : A → B) (g : B → C) {x y : A} (p : x ≡ y) →
cong (λ a → g (f a)) p ≡ cong g (cong f p)
congComp f g p = refl
```

Path types also lets us prove new things are not provable in standard Agda, for example function extensionality (pointwise equal functions are equal) has an extremely simple proof:

```
funExt : ∀ {ℓ} {A : Set ℓ} {B : A → Set ℓ} {f g : (x : A) → B x} →
((x : A) → f x ≡ g x) → f ≡ g
funExt p i x = p x i
```

## Transport¶

While path types are great for reasoning about equality they don’t let us transport along paths between types or even compose paths, which in particular means that we cannot yet prove the induction principle for paths. In order to remedy this we also have a built-in (generalized) transport operation transp and homogeneous composition operations hcomp. The transport operation is generalized in the sense that it lets us specify where it is the identity function.

```
transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1
```

There is an additional side condition to be satisfied for a usage of `transp`

to type-check: `A`

should be a constant function whenever the constraint `r = i1`

is satisfied. By constant here we mean that `A`

is definitionally equal to `λ _ → A i0`

, which in turn requires `A i0`

and `A i1`

to be definitionally equal as well.

When `r`

is `i1`

, `transp A r`

will compute as the identity function.

```
transp A i1 a = a
```

This is only sound if in such a case `A`

is a trivial path, as the side condition requires.

It might seems strange that the side condition expects `r`

and
`A`

to interact, but both of them can depend on any of the
interval variables in scope, so assuming a specific value for `r`

can affect what `A`

looks like.

Some examples of the side condition for different values of `r`

:

If

`r`

is some in-scope variable`i`

, on which`A`

may depend as well, then`A`

only needs to be a constant function when substituting`i1`

for`i`

.If

`r`

is`i0`

then there is no restrition on`A`

, since the side condition is vacuously true.If

`r`

is`i1`

then`A`

must be a constant function.

We can use `transp`

to define regular transport:

```
transport : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a
```

By combining the transport and min operations we can define the induction principle for paths:

```
J : ∀ {ℓ} {A : Set ℓ} {x : A} (P : ∀ y → x ≡ y → Set ℓ)
(d : P x refl) {y : A} (p : x ≡ y)
→ P y p
J P d p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d
```

One subtle difference between paths and the propositional equality
type of Agda is that the computation rule for `J`

does not hold
definitionally. If `J`

is defined using pattern-matching as in the
Agda standard library then this holds, however as the path types are
not inductively defined this does not hold for the above definition of
`J`

. In particular, transport in a constant family is only the
identity function up to a path which implies that the computation rule
for `J`

only holds up to a path:

```
transportRefl : ∀ {ℓ} {A : Set ℓ} (x : A) → transport refl x ≡ x
transportRefl {A = A} x i = transp (λ _ → A) i x
JRefl : ∀ {ℓ} {A : Set ℓ} {x : A} (P : ∀ y → x ≡ y → Set ℓ)
(d : P x refl) → J P d refl ≡ d
JRefl P d = transportRefl d
```

Internally in Agda the `transp`

operation computes by cases on the
type, so for example for Σ-types it is computed elementwise. For path
types it is however not yet possible to provide the computation rule
as we need some way to remember the endpoints of the path after
transporting it. Furthermore, this must work for arbitrary higher
dimensional cubes (as we can iterate the path types). For this we
introduce the “homogeneous composition operations” (`hcomp`

) that
generalize binary composition of paths to n-ary composition of higher
dimensional cubes.

## Partial elements¶

In order to describe the homogeneous composition operations we need to
be able to write partially specified n-dimensional cubes (i.e. cubes
where some faces are missing). Given an element of the interval ```
r :
I
```

there is a predicate `IsOne`

which represents the constraint ```
r
= i1
```

. This comes with a proof that `i1`

is in fact equal to `i1`

called `1=1 : IsOne i1`

. We use Greek letters like `φ`

or `ψ`

when such an `r`

should be thought of as being in the domain of
`IsOne`

.

Using this we introduce a type of partial elements called ```
Partial φ
A
```

, this is a special version of `IsOne φ → A`

with a more
extensional judgmental equality (two elements of `Partial φ A`

are
considered equal if they represent the same subcube, so the faces of
the cubes can for example be given in different order and the two
elements will still be considered the same). The idea is that
`Partial φ A`

is the type of cubes in `A`

that are only defined
when `IsOne φ`

. There is also a dependent version of this called
`PartialP φ A`

which allows `A`

to be defined only when ```
IsOne
φ
```

.

```
Partial : ∀ {ℓ} → I → Set ℓ → SSet ℓ
PartialP : ∀ {ℓ} → (φ : I) → Partial φ (Set ℓ) → SSet ℓ
```

There is a new form of pattern matching that can be used to introduce partial elements:

```
partialBool : ∀ i → Partial (i ∨ ~ i) Bool
partialBool i (i = i0) = true
partialBool i (i = i1) = false
```

The term `partialBool i`

should be thought of a boolean with different
values when `(i = i0)`

and `(i = i1)`

. Terms of type ```
Partial φ
A
```

can also be introduced using a Pattern matching lambda.

```
partialBool' : ∀ i → Partial (i ∨ ~ i) Bool
partialBool' i = λ { (i = i0) → true
; (i = i1) → false }
```

When the cases overlap they must agree (note that the order of the cases doesn’t have to match the interval formula exactly):

```
partialBool'' : ∀ i j → Partial (~ i ∨ i ∨ (i ∧ j)) Bool
partialBool'' i j = λ { (i = i1) → true
; (i = i1) (j = i1) → true
; (i = i0) → false }
```

Furthermore `IsOne i0`

is actually absurd.

```
empty : {A : Set} → Partial i0 A
empty = λ { () }
```

Cubical Agda also has cubical subtypes as in the CCHM type theory:

```
_[_↦_] : ∀ {ℓ} (A : Set ℓ) (φ : I) (u : Partial φ A) → SSet ℓ
A [ φ ↦ u ] = Sub A φ u
```

A term `v : A [ φ ↦ u ]`

should be thought of as a term of type
`A`

which is definitionally equal to `u : A`

when `IsOne φ`

is
satisfied. Any term `u : A`

can be seen as an term of ```
A [ φ ↦ u
]
```

which agrees with itself on `φ`

:

```
inS : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : A) → A [ φ ↦ (λ _ → u) ]
```

One can also forget that a partial element agrees with `u`

on `φ`

:

```
outS : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → A [ φ ↦ u ] → A
```

They satisfy the following equalities:

```
outS (inS a) = a
inS {φ = φ} (outS {φ = φ} a) = a
outS {φ = i1} {u} _ = u 1=1
```

Note that given `a : A [ φ ↦ u ]`

and `α : IsOne φ`

, it is not the case
that `outS a = u α`

; however, underneath the pattern binding `(φ = i1)`

,
one has `outS a = u 1=1`

.

With all of this cubical infrastructure we can now describe the
`hcomp`

operations.

## Homogeneous composition¶

The homogeneous composition operations generalize binary composition of paths so that we can compose multiple composable cubes.

```
hcomp : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : I → Partial φ A) (u0 : A) → A
```

When calling `hcomp {φ = φ} u u0`

Agda makes sure that `u0`

agrees
with `u i0`

on `φ`

. The idea is that `u0`

is the base and `u`

specifies the sides of an open box. This is hence an open (higher
dimensional) cube where the side opposite of `u0`

is missing. The
`hcomp`

operation then gives us the missing side opposite of
`u0`

. For example binary composition of paths can be written as:

```
compPath : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
compPath {x = x} p q i = hcomp (λ j → λ { (i = i0) → x
; (i = i1) → q j })
(p i)
```

Pictorially we are given `p : x ≡ y`

and `q : y ≡ z`

, and the
composite of the two paths is obtained by computing the missing lid of
this open square:

```
x z
^ ^
| |
x | | q j
| |
x ----------> y
p i
```

In the drawing the direction `i`

goes left-to-right and `j`

goes
bottom-to-top. As we are constructing a path from `x`

to `z`

along
`i`

we have `i : I`

in the context already and we put `p i`

as
bottom. The direction `j`

that we are doing the composition in is
abstracted in the first argument to `hcomp`

.

Note that the partial element `u`

does not have to specify
all the sides of the open box, giving more sides simply gives you
more control on the result of `hcomp`

.
For example if we omit the `(i = i0) → x`

side in the
definition of `compPath`

we still get a valid term of type
`A`

. However, that term would reduce to `hcomp (\ j → \ { () }) x`

when `i = i0`

and so that definition would not build
a path that starts from `x`

.

We can also define homogeneous filling of cubes as

```
hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
(u : ∀ i → Partial φ A) (u0 : A [ φ ↦ u i0 ])
(i : I) → A
hfill {φ = φ} u u0 i = hcomp (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
; (i = i0) → outS u0 })
(outS u0)
```

When `i`

is `i0`

this is `u0`

and when `i`

is `i1`

this is
`hcomp u u0`

. This can hence be seen as giving us the interior of an
open box. In the special case of the square above `hfill`

gives us a
direct cubical proof that composing `p`

with `refl`

is `p`

.

```
compPathRefl : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → compPath p refl ≡ p
compPathRefl {x = x} {y = y} p j i = hfill (λ _ → λ { (i = i0) → x
; (i = i1) → y })
(inS (p i))
(~ j)
```

## Glue types¶

In order to be able to prove the univalence theorem we also have to
add “Glue” types. These lets us turn equivalences between types into
paths between types. An equivalence of types `A`

and `B`

is
defined as a map `f : A → B`

such that its fibers are contractible.

```
fiber : ∀ {ℓ} {A B : Set ℓ} (f : A → B) (y : B) → Set ℓ
fiber {A = A} f y = Σ[ x ∈ A ] f x ≡ y
isContr : ∀ {ℓ} → Set ℓ → Set ℓ
isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)
record isEquiv {ℓ} {A B : Set ℓ} (f : A → B) : Set ℓ where
field
equiv-proof : (y : B) → isContr (fiber f y)
_≃_ : ∀ {ℓ} (A B : Set ℓ) → Set ℓ
A ≃ B = Σ[ f ∈ (A → B) ] (isEquiv f)
```

The simplest example of an equivalence is the identity function.

```
idfun : ∀ {ℓ} → (A : Set ℓ) → A → A
idfun _ x = x
idIsEquiv : ∀ {ℓ} (A : Set ℓ) → isEquiv (idfun A)
equiv-proof (idIsEquiv A) y =
((y , refl) , λ z i → z .snd (~ i) , λ j → z .snd (~ i ∨ j))
idEquiv : ∀ {ℓ} (A : Set ℓ) → A ≃ A
idEquiv A = (idfun A , idIsEquiv A)
```

An important special case of equivalent types are isomorphic types (i.e. types with maps going back and forth which are mutually inverse): https://github.com/agda/cubical/blob/master/Cubical/Foundations/Isomorphism.agda.

As everything has to work up to higher dimensions the Glue types take
a partial family of types that are equivalent to the base type `A`

:

```
Glue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
→ Partial φ (Σ[ T ∈ Set ℓ' ] T ≃ A) → Set ℓ'
```

These come with a constructor and eliminator:

```
glue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I} {Te : Partial φ (Σ[ T ∈ Set ℓ' ] T ≃ A)}
→ PartialP φ T → A → Glue A Te
unglue : ∀ {ℓ ℓ'} {A : Set ℓ} (φ : I) {Te : Partial φ (Σ[ T ∈ Set ℓ' ] T ≃ A)}
→ Glue A Te → A
```

Using Glue types we can turn an equivalence of types into a path as follows:

```
ua : ∀ {ℓ} {A B : Set ℓ} → A ≃ B → A ≡ B
ua {_} {A} {B} e i = Glue B (λ { (i = i0) → (A , e)
; (i = i1) → (B , idEquiv B) })
```

The idea is that we glue `A`

together with `B`

when `i = i0`

using `e`

and `B`

with itself when `i = i1`

using the identity
equivalence. This hence gives us the key part of univalence: a
function for turning equivalences into paths. The other part of
univalence is that this map itself is an equivalence which follows
from the computation rule for `ua`

:

```
uaβ : ∀ {ℓ} {A B : Set ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ e .fst x
uaβ e x = transportRefl (e .fst x)
```

Transporting along the path that we get from applying `ua`

to an
equivalence is hence the same as applying the equivalence. This is
what makes it possible to use the univalence axiom computationally in
Cubical Agda: we can package up our equivalences as paths, do equality
reasoning using these paths, and in the end transport along the paths
in order to compute with the equivalences.

We have the following equalities:

```
Glue A {i1} Te = Te 1=1 .fst
unglue φ (glue t a) = a
glue (\ { (φ = i1) -> g}) (unglue φ g) = g
unglue i1 {Te} g = Te 1=1 .snd .fst g
glue {φ = i1} t a = t 1=1
```

For more results about Glue types and univalence see https://github.com/agda/cubical/blob/master/Cubical/Core/Glue.agda and https://github.com/agda/cubical/blob/master/Cubical/Foundations/Univalence.agda. For some examples of what can be done with this for working with binary and unary numbers see https://github.com/agda/cubical/blob/master/Cubical/Data/BinNat/BinNat.agda.

## Higher inductive types¶

Cubical Agda also lets us directly define higher inductive types as datatypes with path constructors. For example the circle and torus can be defined as:

```
data S¹ : Set where
base : S¹
loop : base ≡ base
data Torus : Set where
point : Torus
line1 : point ≡ point
line2 : point ≡ point
square : PathP (λ i → line1 i ≡ line1 i) line2 line2
```

Functions out of higher inductive types can then be defined using pattern-matching:

```
t2c : Torus → S¹ × S¹
t2c point = (base , base)
t2c (line1 i) = (loop i , base)
t2c (line2 j) = (base , loop j)
t2c (square i j) = (loop i , loop j)
c2t : S¹ × S¹ → Torus
c2t (base , base) = point
c2t (loop i , base) = line1 i
c2t (base , loop j) = line2 j
c2t (loop i , loop j) = square i j
```

When giving the cases for the path and square constructors we have to
make sure that the function maps the boundary to the right thing. For
instance the following definition does not pass Agda’s typechecker as
the boundary of the last case does not match up with the expected
boundary of the square constructor (as the `line1`

and `line2`

cases are mixed up).

```
c2t_bad : S¹ × S¹ → Torus
c2t_bad (base , base) = point
c2t_bad (loop i , base) = line2 i
c2t_bad (base , loop j) = line1 j
c2t_bad (loop i , loop j) = square i j
```

Functions defined by pattern-matching on higher inductive types compute definitionally, for all constructors.

```
c2t-t2c : ∀ (t : Torus) → c2t (t2c t) ≡ t
c2t-t2c point = refl
c2t-t2c (line1 _) = refl
c2t-t2c (line2 _) = refl
c2t-t2c (square _ _) = refl
t2c-c2t : ∀ (p : S¹ × S¹) → t2c (c2t p) ≡ p
t2c-c2t (base , base) = refl
t2c-c2t (base , loop _) = refl
t2c-c2t (loop _ , base) = refl
t2c-c2t (loop _ , loop _) = refl
```

By turning this isomorphism into an equivalence we get a direct proof that the torus is equal to two circles.

```
Torus≡S¹×S¹ : Torus ≡ S¹ × S¹
Torus≡S¹×S¹ = isoToPath (iso t2c c2t t2c-c2t c2t-t2c)
```

Cubical Agda also supports parameterized and recursive higher inductive types, for example propositional truncation (squash types) is defined as:

```
data ∥_∥ {ℓ} (A : Set ℓ) : Set ℓ where
∣_∣ : A → ∥ A ∥
squash : ∀ (x y : ∥ A ∥) → x ≡ y
isProp : ∀ {ℓ} → Set ℓ → Set ℓ
isProp A = (x y : A) → x ≡ y
recPropTrunc : ∀ {ℓ} {A : Set ℓ} {P : Set ℓ} → isProp P → (A → P) → ∥ A ∥ → P
recPropTrunc Pprop f ∣ x ∣ = f x
recPropTrunc Pprop f (squash x y i) =
Pprop (recPropTrunc Pprop f x) (recPropTrunc Pprop f y) i
```

For many more examples of higher inductive types see: https://github.com/agda/cubical/tree/master/Cubical/HITs.

## Indexed inductive types¶

Cubical Agda has experimental support for the `transp`

primitive when
used to substitute the indices of an indexed inductive type. A handful
of definitions (satisfying a technical restriction on their pattern
matching) will compute when applied to a transport along indices. As an
example of what works, let us consider the following running example:

```
data Eq {a} {A : Set a} (x : A) : A → Set a where
reflEq : Eq x x
data Vec {a} (A : Set a) : Nat → Set a where
[] : Vec A zero
_∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
```

Functions which match on `Eq`

when all of its endpoints are variables,
that is, very generic lemmas like `symEq`

and `transpEq`

below, will
compute on all cases: they will compute to the given right-hand-side
definitionally when their argument is `reflEq`

, and will compute to a
transport in the codomain when their argument has been transported in
the second variable.

```
symEq : ∀ {a} {A : Set a} {x y : A} → Eq x y → Eq y x
symEq reflEq = reflEq
transpEq : ∀ {a} {A B : Set a} → Eq A B → A → B
transpEq reflEq x = x
pathToEq : ∀ {a} {A : Set a} {x y : A} → x ≡ y → Eq x y
pathToEq {x = x} p = transp (λ i → Eq x (p i)) i0 reflEq
module _ {a} {A B : Set a} {x y : A} {f : A ≃ B} where
_ : symEq (reflEq {x = x}) ≡ reflEq
_ = refl
_ : transpEq (pathToEq (ua (idEquiv Bool))) ≡ λ x → x
_ = refl
```

Matching on indexed types in situations where types are assumed (so
their transports are also open) often generates many more transports
than the comparable construction with paths would. As an example,
compare the proof of `uaβEq`

below has four pending transports,
whereas `uaβ`

only has one!

```
uaβEq : transpEq (pathToEq (ua f)) ≡ f .fst
uaβEq = funExt λ z →
compPath (transportRefl (f .fst _))
(cong (f .fst) (compPath
(transportRefl _)
(compPath
(transportRefl _)
(transportRefl _))))
```

In more concrete situations, such as when the indices are constructors of some other inductive type, pattern-matching definitions will not compute when applied to transports. For specific unsupported cases, see What works, and what doesn’t.

If the `UnsupportedIndexedMatch`

warning is enabled (it is by default),
Agda will print a warning for every definition whose computational
behaviour could not be extended to cover transports. Internally,
transports are represented by an additional constructor, and
pattern-matching definitions must be extended to cover these
constructors. To do this, the results of pattern-matching unification
must be translated into an embedding (in the HoTT sense).
**This is work-in-progress.**

For the day-to-day use of Cubical Agda, it is advisable to disable the
`UnsupportedIndexedMatch`

warnings. You can do this using the
`-WnoUnsupportedIndexedMatch`

option in an `OPTIONS`

pragma or in your
`agda-lib`

file.

### What works, and what doesn’t¶

This section lists some of the common cases where pattern-matching unification produces something that can not be extended to cover transports, and the cases in which it can.

The following pair of definitions relies on injectivity for data
constructors (specifically of the constructor `suc`

), and so will not
compute on transported values.

```
sucInjEq : ∀ {n k} → Eq (suc n) (suc k) → Eq n k
sucInjEq reflEq = reflEq
head : ∀ {n} {a} {A : Set a} → Vec A (suc n) → A
head (x ∷ _) = x
```

To demonstrate the failure of computation, we can set up the following
artificial example using `head`

. By passing the vector `true ∷ []`

through two transports, even if they would cancel out, `head`

’s
computation gets stuck.

```
module _ (n : Nat) (p : n ≡ 1) where private
vec : Vec Bool n
vec = transport (λ i → Vec Bool (p (~ i))) (true ∷ [])
hd : Bool
hd = head (transport (λ i → Vec Bool (p i)) vec)
-- Does not type-check:
-- _ : hd ≡ true
-- _ = refl
-- Instead, hd is some big expression involving head applied to a
-- transport
```

If a definition is stuck on a transport, often the best workaround is to
avoid treating it like the reducible expression it should be, and
managing the transports yourself. For example, using the proof that
`transport (sym p) (transport p x) ≡ x`

, we can compute with `hd`

up
to a path, even if it’s definitionally stuck.

```
-- Continuing from above..
_ : hd ≡ true
_ = cong head (transport⁻Transport (λ i → Vec Bool (p (~ i))) (true ∷ []))
```

In other cases, it may be possible to rephrase the proof in ways that
avoid unsupported cases in pattern matching, and so, compute. For
example, returning to `sucInj`

, we can define it in terms of `apEq`

(which always computes), and the fact that `suc`

has a
partially-defined inverse:

```
apEq : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y : A}
→ Eq x y → Eq (f x) (f y)
apEq f reflEq = reflEq
sucInjEq′ : ∀ {n k} → Eq (suc n) (suc k) → Eq n k
sucInjEq′ = apEq λ { (suc n) → n ; zero → zero }
```

Definitions which rely on principles incompatible with Cubical Agda (K,
injectivity of type constructors) will never compute on transports. Note
that enabling both Cubical and K is not compatible with `--safe`

.

Absurd clauses do not need any special handling (since the transport of
an absurdity is still absurd), so definitions which rely on Agda’s
ability to automatically separate constructors of inductive types will
not generate a `UnsupportedIndexedMatch`

warning.

```
zeroNotSucEq : ∀ {n} {a} {A : Set a} → Eq zero (suc n) → A
zeroNotSucEq ()
```

Definitions whose elaboration involves using an equality derived from
pattern-matching in a type in `Setω`

can not be extended yet. The
following example is very artificial because it minimises
an example from the Cubical library.
The point is that to extend `test`

to cover transports, we would need
to, given `p : ℓ′ ≡ ℓ`

, produce a `PathP (λ i → Argh ℓ (p i)) _ _`

,
but `Setω`

is not considered fibrant yet.

```
data Argh (ℓ : Level) : Level → Setω where
argh : ∀ {ℓ′} → Argh ℓ ℓ′ → Argh ℓ ℓ′
test : ∀ {ℓ ℓ′} → Argh ℓ ℓ′ → Bool
test {ℓ} (argh _) = true
```

### Modalities & indexed matching¶

When using indexed matching in Cubical Agda, clauses’ arguments (and
their right-hand-sides) need to be transported to account for indexing,
meaning that the *types* of those arguments must be well-formed *terms*.

For example, the following code is forbidden in Cubical Agda, and when
`--without-K`

is enabled:

```
subst : (@0 P : A → Set p) → x ≡ y → P x → P y
subst _ refl p = p
```

This is because the predicate `P`

is erased, but internally, we have
to transport along the argument `p`

along a path involving `P`

, in a
relevant position.

Any argument which is used in the result type, or appears after a forced (dot) pattern, must have a modality-correct type.

## Cubical identity types and computational HoTT/UF¶

As mentioned above the computation rule for `J`

does not hold
definitionally for path types. Cubical Agda solves this by introducing
a cubical identity type. The
https://github.com/agda/cubical/blob/master/Cubical/Core/Id.agda file
exports all of the primitives for this type, including the notation
`_≡_`

and a `J`

eliminator that computes definitionally on
`refl`

.

The cubical identity types and path types are equivalent, so all of the results for one can be transported to the other one (using univalence). Using this we have implemented an interface to HoTT/UF which provides the user with the key primitives of Homotopy Type Theory and Univalent Foundations implemented using cubical primitives under the hood. This hence gives an axiom free version of HoTT/UF which computes properly.

```
module Cubical.Core.HoTT-UF where
open import Cubical.Core.Id public
using ( _≡_ -- The identity type.
; refl -- Its constructor.
; J -- Its eliminator (can be defined by pattern matching)
; transport -- As in the HoTT Book.
; ap
; _∙_
; _⁻¹
; _≡⟨_⟩_ -- Standard equational reasoning.
; _∎
; funExt -- Function extensionality
-- (can also be derived from univalence).
; Σ -- Sum type. Needed to define contractible types, equivalences
; _,_ -- and univalence.
; pr₁ -- The eta rule is available.
; pr₂
; isProp -- The usual notions of proposition, contractible type, set.
; isContr
; isSet
; isEquiv -- A map with contractible fibers
-- (Voevodsky's version of the notion).
; _≃_ -- The type of equivalences between two given types.
; EquivContr -- A formulation of univalence.
; ∥_∥ -- Propositional truncation.
; ∣_∣ -- Map into the propositional truncation.
; ∥∥-isProp -- A truncated type is a proposition.
; ∥∥-recursion -- Non-dependent elimination.
; ∥∥-induction -- Dependent elimination.
)
```

In order to get access to only the HoTT/UF primitives start a file as follows:

```
{-# OPTIONS --cubical #-}
open import Cubical.Core.HoTT-UF
```

However, even though this interface exists, we recommend that users of
cubical mode use the path types rather than the cubical identity types.
Primarily, this is because many operations for path types are
implemented directly, rather than by induction (e.g. `ap`

, `funExt`

,
`happly`

, `sym`

, etc), and thus enjoy better computational
behaviour. In addition to using `J`

directly, it is possible to match
on the reflexivity constructor, as if `Id`

were an inductive type:

```
symId : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → Id y x
symId reflId = reflId
```

Cubical identity types are *not* inductively defined, and we may observe
this using the primitives `conid`

and `primIdElim`

. These primitives
expose underlying representation: terms of the cubical identity type can
be thought of pairs consisting of a path p and a cofibration φ, such
that, under the cofibration φ, the path p is the reflexivty path.
These primitives are very low-level, and their use is not recommended.

```
apId : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} (f : A → B)
→ {x y : A} → Id x y → Id (f x) (f y)
apId f {x = x} = primIdElim (λ y _ → Id (f x) (f y))
λ φ y w → conid φ λ i → f (outS w i)
```

Even though it is possible to define the reflexivity path using
`conid`

, the name `reflId`

is special, in that it is treated as a
“matchable” constructor, whereas `conid`

is not. Depending on your
syntax highlighting scheme, this can be observed using agda-mode: they
are different colours. However, for computation, they are treated as the
same:

```
_ : ∀ {ℓ} {A : Set ℓ} {x : A} → reflId ≡ conid i1 (λ _ → x)
_ = refl
```

## Cubical Agda with erased Glue¶

The option `--erased-cubical`

enables a variant of Cubical
Agda in which Glue (and the other builtins defined in
`Agda.Builtin.Cubical.Glue`

) must only be used in
erased settings.

Regular Cubical Agda code can import code that uses
`--erased-cubical`

. Regular Cubical Agda code can also be
imported from code that uses `--erased-cubical`

, but names
defined using Cubical Agda can only be used if the option
`--erasure`

is used. In that case the names are treated as if
they had been marked as erased, with an exception related to pattern
matching:

Matching on a non-erased imported constructor does not, on its own, make Agda treat the right-hand side as erased.

The reason for this exception is that it should be possible to import
the code from modules that use `--cubical`

, in which the
non-erased constructors are not treated as erased.

Note that names that are re-exported from a Cubical Agda module using
`open import M args public`

are seen as defined using Cubical Agda.

## References¶

Cyril Cohen, Thierry Coquand, Simon Huber and Anders Mörtberg; “Cubical Type Theory: a constructive interpretation of the univalence axiom”.

Thierry Coquand, Simon Huber, Anders Mörtberg; “On Higher Inductive Types in Cubical Type Theory”.

## Appendix: Cubical Agda primitives¶

The Cubical Agda primitives and internals are exported by a series of
files found in the `lib/prim/Agda/Builtin/Cubical`

directory of
Agda. The `agda/cubical`

library exports all of these primitives
with the names used throughout this document. Experts might find it
useful to know what is actually exported as there are quite a few
primitives available that are not really exported by `agda/cubical`

,
so the goal of this section is to list the contents of these
files. However, for regular users and beginners the `agda/cubical`

library should be sufficient and this section can safely be ignored.

**Warning**: Many of the built-ins whose definitions can be written in
Agda are nonetheless used internally in the implementation of cubical Agda,
and using different implementations can easily lead to unsoundness. Even
though they are definable in user code, this is not a supported
use-case.

The key file with primitives is `Agda.Primitive.Cubical`

. It exports
the following `BUILTIN`

, primitives and postulates:

```
{-# BUILTIN CUBEINTERVALUNIV IUniv #-} -- IUniv : SSet₁
{-# BUILTIN INTERVAL I #-} -- I : IUniv
{-# BUILTIN IZERO i0 #-}
{-# BUILTIN IONE i1 #-}
infix 30 primINeg
infixr 20 primIMin primIMax
primitive
primIMin : I → I → I -- _∧_
primIMax : I → I → I -- _∨_
primINeg : I → I -- ~_
{-# BUILTIN ISONE IsOne #-} -- IsOne : I → SSet
postulate
itIsOne : IsOne i1 -- 1=1
IsOne1 : ∀ i j → IsOne i → IsOne (primIMax i j)
IsOne2 : ∀ i j → IsOne j → IsOne (primIMax i j)
{-# BUILTIN ITISONE itIsOne #-}
{-# BUILTIN ISONE1 IsOne1 #-}
{-# BUILTIN ISONE2 IsOne2 #-}
{-# BUILTIN PARTIAL Partial #-}
{-# BUILTIN PARTIALP PartialP #-}
postulate
isOneEmpty : ∀ {a} {A : Partial i0 (Set a)} → PartialP i0 A
{-# BUILTIN ISONEEMPTY isOneEmpty #-}
primitive
primPOr : ∀ {a} (i j : I) {A : Partial (primIMax i j) (Set a)}
→ PartialP i (λ z → A (IsOne1 i j z)) → PartialP j (λ z → A (IsOne2 i j z))
→ PartialP (primIMax i j) A
-- Computes in terms of primHComp and primTransp
primComp : ∀ {a} (A : (i : I) → Set (a i)) {φ : I} → (∀ i → Partial φ (A i)) → (a : A i0) → A i1
syntax primPOr p q u t = [ p ↦ u , q ↦ t ]
primitive
primTransp : ∀ {a} (A : (i : I) → Set (a i)) (φ : I) → (a : A i0) → A i1
primHComp : ∀ {a} {A : Set a} {φ : I} → (∀ i → Partial φ A) → A → A
```

The interval `I`

belongs to its own sort, `IUniv`

. Types in this sort
do not support composition and transport (unlike `Set`

), but function
types from types in this sort to types in `Set`

do (unlike SSet).

The Path types are exported by `Agda.Builtin.Cubical.Path`

:

```
postulate
PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ
{-# BUILTIN PATHP PathP #-}
infix 4 _≡_
_≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
_≡_ {A = A} = PathP (λ _ → A)
{-# BUILTIN PATH _≡_ #-}
```

The Cubical subtypes are exported by `Agda.Builtin.Cubical.Sub`

:

```
{-# BUILTIN SUB Sub #-}
postulate
inc : ∀ {ℓ} {A : Set ℓ} {φ} (x : A) → Sub A φ (λ _ → x)
{-# BUILTIN SUBIN inS #-}
primitive
primSubOut : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → Sub _ φ u → A
```

Equivalences are exported by `Agda.Builtin.Cubical.Equiv`

:

```
record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
field
equiv-proof : (y : B) → isContr (fiber f y)
infix 4 _≃_
_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) \ f → (isEquiv f)
equivFun : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A ≃ B → A → B
equivFun e = fst e
equivProof : ∀ {la lt} (T : Set la) (A : Set lt) → (w : T ≃ A) → (a : A)
→ ∀ ψ (f : Partial ψ (fiber (w .fst) a)) → fiber (w .fst) a [ ψ ↦ f ]
equivProof A B w a ψ fb = contr' {A = fiber (w .fst) a} (w .snd .equiv-proof a) ψ fb
where
contr' : ∀ {ℓ} {A : Set ℓ} → isContr A → (φ : I) → (u : Partial φ A) → A
contr' {A = A} (c , p) φ u = hcomp (λ i → λ { (φ = i1) → p (u 1=1) i
; (φ = i0) → c }) c
{-# BUILTIN EQUIV _≃_ #-}
{-# BUILTIN EQUIVFUN equivFun #-}
{-# BUILTIN EQUIVPROOF equivProof #-}
```

The Glue types are exported by `Agda.Builtin.Cubical.Glue`

:

```
open import Agda.Builtin.Cubical.Equiv public
primitive
primGlue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
→ (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A))
→ Set ℓ'
prim^glue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
→ {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
→ PartialP φ T → A → primGlue A T e
prim^unglue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
→ {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
→ primGlue A T e → A
primFaceForall : (I → I) → I
```

Note that the Glue types are uncurried in `agda/cubical`

to make
them more pleasant to use:

```
Glue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
→ (Te : Partial φ (Σ[ T ∈ Set ℓ' ] T ≃ A))
→ Set ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)
```

The `Agda.Builtin.Cubical.Id`

exports the cubical identity types:

```
postulate
Id : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
{-# BUILTIN ID Id #-}
{-# BUILTIN CONID conid #-}
{-# BUILTIN REFLID reflId #-}
primitive
primDepIMin : _
primIdFace : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → I
primIdPath : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → x ≡ y
primitive
primIdElim : ∀ {a c} {A : Set a} {x : A}
(C : (y : A) → Id x y → Set c) →
((φ : I) (y : A [ φ ↦ (λ _ → x) ])
(w : (x ≡ outS y) [ φ ↦ (λ { (φ = i1) → \ _ → x}) ]) →
C (outS y) (conid φ (outS w))) →
{y : A} (p : Id x y) → C y p
```