Cubical¶
The Cubical mode extends Agda with a variety of features from Cubical Type Theory. In particular, it adds computational univalence and higher inductive types, hence giving 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. There is also a research paper specifically about Cubical Agda at https://www.doi.org/10.1017/S0956796821000034.
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 are two major libraries for Cubical Agda:
agda/cubical
: originally intended as a standard 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.1lab
: A formalised and cross linked reference resource for cubical methods in Homotopy Type Theory which can be found at https://1lab.dev/. Much better documented than theagda/cubical
library and hence more accessible to newcomers. The sources can be found at https://github.com/plt-amy/1lab.
In this documentation we will rely on the agda/cubical
library and
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
Follow the instructions at https://github.com/agda/cubical to install the library.
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.
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
i1 ∨ i = 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, typed lambdas cannot be used to form paths, they are reserved for functions:
not-refl : ∀ {ℓ} {A : Set ℓ} {x : A} → (i : I) → A
not-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 let us prove new things are not provable in standard Agda. For example, function extensionality, stating that 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 do not 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.
As a remedy, 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 variablei
, on whichA
may depend as well, thenA
only needs to be a constant function when substitutingi1
fori
.If
r
isi0
then there is no restrition onA
, since the side condition is vacuously true.If
r
isi1
thenA
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
.
The idea is that Partial φ A
is the type of cubes in A
that are only defined when IsOne φ
holds.
Partial φ A
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
yet the two elements will still be considered the same.
There is also a dependent version of Partial φ A
called PartialP φ A
which requires A
only to be defined 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 = λ where
(i = i0) → true
(i = i1) → false
When the cases overlap they must agree:
partialBool'' : ∀ i j → Partial (~ i ∨ i ∨ (i ∧ j)) Bool
partialBool'' i j = λ where
(i = i1) → true
(i = i1) (j = i1) → true
(i = i0) → false
Note that the order of the cases does not have to match the interval formula exactly.
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
These coercions 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
; j (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
; j (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).
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 the files of Glue
types and univalence in the agda/cubical
library or the 1lab
.
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 the
agda/cubical
library or the 1lab
.
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 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
; 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