Contents

# Contents

## Idea

Cubical path types are a form of path types in dependent type theory used in cubical type theories.

A major difference between cubical path types and Martin-Löf identity types is the behaviour of the J rule. In Martin-Löf identity types the J rule holds up to definitional equality, but for cubical path types, the J rule only holds up to a path.

Another difference is that transport generally behaves better with cubical path types. Certain rules for the computation of transports in concrete type families hold up to definitional equality for cubical path types, but only up to an identification for Martin-Löf identity types.

## Rules

The rules for (dependent) cubical path types are as follows

• Formation
$\frac{\Gamma, i:I \vdash A \; \mathrm{type} \quad \Gamma \vdash a:[0/i]A \quad \Gamma \vdash b:[1/i]A}{\Gamma \vdash \mathrm{path}_{i.A}(a,b) \; \mathrm{type}}$
• Introduction
$\frac{\Gamma, i:I \vdash a:A}{\Gamma \vdash \lambda i.a:\mathrm{path}_{i.A}([0/i]a,[1/i]a)}$
• Elimination
$\frac{\Gamma \vdash p:\mathrm{path}_{i.A}(a,b) \quad \Gamma \vdash r:I}{\Gamma \vdash p(r):[r/i]A [\partial(r) \to [r \equiv 0 \to a \vert r \equiv 1 \to b]]}$
• Computation
$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash (\lambda i.a)(r) \equiv [r/i]a:[r/i]A}$
• Uniqueness (optional)
$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash p \equiv \lambda i.p(i) : \mathrm{path}_{i.A}(a,b)}$

In addition, there are coercion and composition operations which make the path type behave like an identity type:

• Coercion:
$\frac{\Gamma, i:I \vdash A \; \mathrm{type} \quad \Gamma \vdash a:[r/i]A}{\Gamma \vdash \mathrm{coe}^{r \rightsquigarrow r'}_{i.A} a:[r'/i]A \; [r' \equiv r \to a]}$
• Composition:

## Regularity

In general, cubical path types in cubical type theory do not satisfy the J rule definitionally. However one could force the J rule to hold definitionally by appending a coercion regularity rule:

$\frac{\Gamma, i:I, j:I \vdash A \equiv [j/i]A \; \mathrm{type}}{\Gamma \vdash \mathrm{coe}^{r \rightsquigarrow r'}_{i.A} a \equiv a:[r'/i]A}$

to the type theory.