nLab path type

Redirected from "path space type".

Contents

 Disambiguation

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

  • The identity type x= Ayx =_A y for type AA and elements x:Ax:A and y:Ay:A, which is the type of paths between x:Ax:A and y:Ay:A;

  • The dependent sum type x:A y:Ax= Ay\sum_{x:A} \sum_{y:A} x =_A y, which is the type of all paths in AA; reflexivity is given by the diagonal function;

  • The function type 𝕀A\mathbb{I} \to A from the interval type 𝕀\mathbb{I} to type AA; reflexivity is given by the constant functions in 𝕀A\mathbb{I} \to A - this parallels the topological definition of path spaces as continuous functions out of the unit interval;

  • In cubical type theory, the cubical path type path A(x,y)\mathrm{path}_A(x, y) for type AA and elements x:Ax:A and y:Ay:A - this is notated similarly to the identity type but also behaves as function types from the predefined interval primitive in addition to the behavior of identity types.

The categorical semantics of path types in any of the above forms is the path space object.

category: disambiguation

Last revised on December 31, 2023 at 17:03:24. See the history of this page for a list of all contributions to it.