nLab heterogeneous path type

Disambiguation

There are a few different types which can be called heterogeneous path types or dependent path types in dependent type theory:

• The heterogeneous identity type $u =_{B(-)}^{p} v$ for type family $B(x)$ indexed by $x:A$, and elements $x:A$, $y:A$, $u:B(x)$, $v:B(y)$, and identification $p:x =_A y$, which is the type of paths between $u:B(x)$ and $v:B(y)$ across $p:x =_A y$;

• The dependent sum type $\sum_{u:B(x)} \sum_{v:B(y)} u =_{B(-)}^{p} v$, which is the type of all heterogeneous paths in the type family $B(x)$ across the identification $p:x =_A y$;

• The dependent function type $\prod_{i:\mathbb{I}} B(x)$ from the interval type $\mathbb{I}$ to the type family $B(x)$.

• In cubical type theory, the cubical path type $\mathrm{path}_{i.A}(x, y)$ for a line of types $A(i)$ indexed by interval variable $i:\mathbb{I}$, given interval terms $i:\mathbb{I}$ and $j:\mathbb{I}$ and elements $x:A(i)$ and $y:A(j)$.

See also path type for the homogeneous version of path types.

category: disambiguation