# Cubical Type Theory in Agda¶

Cubical Type Theory Cohen et al., Cubical is implemented in Agda (beta version).

To use cubical type theory, you need to run Agda with the `--cubical` command-line-option. You can also write `{-# OPTIONS --cubical #-}` at the top of the file.

To define paths, use λ abstractions. For example, this is the definition of the constant path:

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

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

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

## The interval type (`I`)¶

The variable `i` in the definition of `refl` has type `I`, which topologically corresponds to the real unit interval. In a closed context, there are only two values of type `I`: the two ends of the interval, `i0` and `i1`:

```a b : I
a = i0
b = i1
```

Elements of the interval form a De Morgan algebra, with minimum (`∧`), maximum (`∨`) and negation (`~`).

```max = i ∨ j
min = i ∧ j
neg = ~ i
```

All the properties of de Morgan algebras hold definitionally. The ends of the interval `i0` and `i1` are the bottom and top elements, respectively:

```p₁ : i0 ∨ i    ≡ i
p₂ : i  ∨ i1   ≡ i1
p₃ : i  ∨ j    ≡ j ∨ i
p₄ : i  ∧ j    ≡ j ∧ i
p₅ : ~ (~ i)   ≡ i
p₆ : i0        ≡ ~ i1
p₇ : ~ (i ∨ j) ≡ ~ i ∧ ~ j
p₈ : ~ (i ∧ j) ≡ ~ i ∨ ~ j
```

## References¶

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