[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents \section{Cubical MLTT} MLTT with a cubical flavour \subsection{Interval type and path types} The **interval type** is a type $\mathbb{I}$ which contains elements $0:\mathbb{I}$ and $1:\mathbb{I}$. $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{I} \; \mathrm{type}}$$ $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{I}} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{I}}$$ \begin{definition} A **path** in a type $A$ is a function $p:\mathbb{I} \to A$ from the interval type to $A$, and the **path type** of a type $A$ is the type of functions $\mathbb{I} \to A$ from the interval type to $A$. \end{definition} \begin{definition} A **line of types** is a type family $A(i)$ indexed by the interval type $i:\mathbb{I}$. \end{definition} \begin{definition} A **heterogeneous path** in a line of types $A(i)$ indexed by $i:\mathbb{I}$ is a dependent function $p:\prod_{i:\mathbb{I}} A(i)$ from the interval type to the line of types $A(i)$, and the **heterogeneous path type** of a type $A$ is the type of dependent functions $\prod_{i:\mathbb{I}} A(i)$ from the interval type to the line of types $A(i)$. \end{definition} \begin{definition} The **identity path** in the interval type is given by the identity function $\mathrm{id}_\mathbb{I} \equiv \lambda i:\mathbb{I}.i:\mathbb{I} \to \mathbb{I}$. \end{definition} \begin{definition} The **constant path** for element $x:A$ is given by the constant function $\lambda i:\mathbb{I}.x:\mathbb{I} \to A$. \end{definition} \begin{theorem} Function application to paths: Given types $A$ and $B$, a function $f:A \to B$, and a path $p:\mathbb{I} \to A$, one could construct a path $\mathrm{ap}_f(p):\mathbb{I} \to B$ \end{theorem} This is defined by $$\mathrm{ap}_f(p) \equiv \lambda i:\mathbb{I}.f(p(i)):\mathbb{I} \to B$$ \begin{theorem} Application of paths to the identity path: Given a type $A$, and a path $p:\mathbb{I} \to A$, $\mathrm{ap}_p(\mathrm{id}_\mathbb{I}) \equiv p$. \end{theorem} By definition of function application to paths, identity path and the uniqueness rule of identity types, one has the following reduction $$\mathrm{ap}_p(\mathrm{id}_\mathbb{I}) \equiv \lambda i:\mathbb{I}.p(\mathrm{id}_\mathbb{I}(i)) \equiv \lambda i:\mathbb{I}.p(i) \equiv p$$ \begin{theorem} Dependent function application to paths: Given a type $A$ and a type family $B(x)$ indexed by $x:A$, a dependent function $f:\prod_{x:A} B(x)$, and a path $p:\mathbb{I} \to A$, one could construct a dependent path $\mathrm{apd}_f(p):\prod_{x:\mathbb{I}} B(x)$ \end{theorem} This is defined by $$\mathrm{apd}_f(p) \equiv \lambda i:\mathbb{I}.f(p(i)):\prod_{x:\mathbb{I}} B(x)$$ \begin{definition} Given a type $A$ and a type family $B(x)$ indexed by $x:A$, a **path homotopy** is a dependent function $H:\prod_{x:A} \mathbb{I} \to B(x)$, a family of paths in $B(x)$. \end{definition} \begin{theorem} Dependent function extensionality for paths: Given a path homotopy $H:\prod_{x:A} \mathbb{I} \to B(x)$, we have a path $$\mathrm{funext}(H):\mathbb{I} \to \prod_{x:A} B(x)$$ \end{theorem} This is defined by $$\mathrm{funext}(H) \equiv \lambda i:\mathbb{I}.\lambda x:A.H(x)(i)$$ \subsection{Path induction} The key difference between cubical Martin-Löf type theory and other cubical type theories, which require additional Kan operations on types, is that the path types in cubical Martin-Löf type theory are characterised directly by an induction principle, called **path induction**: Path induction says that given any type $A$, and any type family $C(p)$ indexed by paths $p:\mathbb{I} \to A$ in $A$, and given any dependent function $t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)$ which says that for all elements $x:A$, there is an element of the type defined by substituting the constant path of $x:A$ into $C$, $C(\lambda i:\mathbb{I}.x)$, one could construct a dependent function $\mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{z:\mathbb{I} \to A} C(z)$ such that for all $x:A$, $\mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t(x)$. $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, p:\mathbb{I} \to A \vdash C(p) \; \mathrm{type} \quad t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)}{\Gamma \vdash \mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{p:\mathbb{I} \to A} C(p)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, p:\mathbb{I} \to A \vdash C(p) \; \mathrm{type} \quad t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)}{\Gamma, x:A \vdash \mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t(x):C(\lambda i:\mathbb{I}.x)}$$ \subsection{Identity types} * The formation rule of identity types state that given a type $A$ and elements $x:A$ and $y:A$, one could form the identity type $x =_A y$. $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A \vdash x =_A y \; \mathrm{type}}$$ * The introduction rule of identity types state that given a type $A$ and a path $p:\mathbb{I} \to A$, one could construct an identification $\mathrm{toeq}_A(f):f(0) =_A f(1)$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash f:\mathbb{I} \to A}{\Gamma \vdash \mathrm{toeq}_A(f):f(0) =_A f(1)}$$ * The elimination rule of identity types state that given a type $A$, elements $x:A$ and $y:A$, and identification $p:x =_A y$, one could construct a path $\mathrm{topath}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A}$$ * The three computation rules of identity types state that given a type $A$, elements $x:A$ and $y:A$, and identification $p:x =_A y$, $$\mathrm{topath}_\mathbb{I}^A(x, y, p)(0) \equiv x \quad \mathrm{topath}_\mathbb{I}^A(x, y, p)(1) \equiv y \quad \mathrm{toeq}_{A}(\mathrm{topath}_\mathbb{I}^A(x, y, p)) \equiv p$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(x, y, p)(0) \equiv x:A}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(x, y, p)(1) \equiv y:A}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{toeq}_{A}(\mathrm{topath}_\mathbb{I}^A(x, y, p)) \equiv p:x =_A y}$$ * The uniqueness rule of identity types state that given a type $A$ and a path $p:\mathbb{I} \to A$, $$\mathrm{topath}_\mathbb{I}^A(p(0), p(1), \mathrm{toeq}_A(p)) \equiv p$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash f:\mathbb{I} \to A}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(f(0), f(1), \mathrm{toeq}_A(f)) \equiv f:\mathbb{I} \to A}$$ \begin{theorem} The elements $0:\mathbb{I}$ and $1:\mathbb{I}$ are equal to each other. \end{theorem} This is defined by sending the identity path in the interval type to its corresponding identification $$\mathrm{toeq}_\mathbb{I}(\mathrm{id}_\mathbb{I}):0 =_\mathbb{I} 1$$ since by the computation rules of the function type, one has $$\mathrm{id}_\mathbb{I}(0) \equiv 0 \quad \mathrm{id}_\mathbb{I}(1) \equiv 1$$ \begin{theorem} Function application of identifications: Given types $A$ and $B$, a a function $f:A \to B$, elements $x:A$ and $y:A$ and an identification $p:x =_A y$, one can construct the identification $\mathrm{ap}_f^{=}(x, y, p):f(x) =_B f(y)$. \end{theorem} This is defined through the inference rules for identity types and function application of paths: $$\mathrm{ap}_f^{=}(x, y, p) \equiv \mathrm{toeq}_B(\mathrm{ap}_f(\mathrm{rec}_\mathbb{I}^A(x, y, p))):f(x) =_B f(y)$$ \begin{theorem} The recursion principle of the interval type: Given a type $A$, elements $x:A$ and $y:A$ and identification $p:x =_{A} y$, one can construct a function $\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p):\mathbb{I} \to A$ such that $$\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(0) \equiv x \quad \mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(1) \equiv y \quad \mathrm{ap}_{\mathrm{rec}_\mathbb{I}^{A}(x, y, p)}^{=}(0, 1, \mathrm{toeq}_\mathbb{I}(\mathrm{id}_\mathbb{I})) \equiv p$$ \end{theorem} We define $$\mathrm{rec}_{\mathbb{I}}^{A(-)}(x, y, p) \equiv \mathrm{topath}_{\mathbb{I}}^{A(-)}(x, y, p)$$ That $\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(0) \equiv x$ is given by the first computation rule of identity types and that $\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(1) \equiv y$ is given by the second computation rules of identity types. Finally, by definition of function application to identifications and the uniqueness rule of identity types, one has the following reduction: $$\mathrm{ap}_{\mathrm{rec}_\mathbb{I}^{A}(x, y, p)}^{=}(0, 1, \mathrm{toeq}_A(\mathrm{id}_\mathbb{I})) \equiv \mathrm{toeq}_A(\mathrm{ap}_{\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)}(\mathrm{rec}_\mathbb{I}^\mathbb{I}(0, 1, \mathrm{toeq}_\mathbb{I}(\mathrm{id}_\mathbb{I})))) \equiv \mathrm{toeq}_A(\mathrm{ap}_{\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)}(\mathrm{id}_\mathbb{I}))$$ and by function application to the identity path and the third computation rule of identity types, one has the following reduction $$\mathrm{toeq}_A(\mathrm{ap}_{\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)}(\mathrm{id}_\mathbb{I})) \equiv \mathrm{toeq}_A(\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)) \equiv p$$ \begin{theorem} Identity types are reflexive: Given an element $x:A$, one could construct an identification $\mathrm{refl}_A(x):x =_A x$. \end{theorem} This is defined by sending the constant path of $x:A$ to its identification $$\mathrm{refl}_A(x) \equiv \mathrm{toeq}_{A}(\lambda i:\mathbb{I}.x):x =_A x$$ \begin{theorem} Given a type $A$ and given a type family $C(x, y, p)$ indexed by $x:A$, $y:A$, and $p:x =_A y$, and a dependent function $t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x))$, one could construct a dependent function $$\mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{f:\mathbb{I} \to A} C(f(0), f(1), \mathrm{toeq}_A(f))$$ such that $\mathrm{ind}_{\mathbb{I} \to A}(t,\lambda i:\mathbb{I}.x) \equiv t(x)$ \end{theorem} This follows by path induction on the type family $C(f(0), f(1), \mathrm{toeq}_A(f))$ indexed by $f:\mathbb{I} \to A$, since by definition of constant function and reflexivity, one has $$(\lambda i:\mathbb{I}.x)(0) \equiv x \quad (\lambda i:\mathbb{I}.x)(1) \equiv x \quad \mathrm{toeq}_A(\lambda i:\mathbb{I}.x) \equiv \mathrm{refl}_A(x)$$ \begin{theorem} J-rule: Given a type $A$ and given a type family $C(x, y, p)$ indexed by $x:A$, $y:A$, and $p:x =_A y$, and a dependent function $t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x))$, one could construct a dependent function $$J(t):\prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} C(x, y, p)$$ such that $J(t, x, x, \mathrm{refl}_A(x)) \equiv t(x)$ \end{theorem} We define $$J(t, x, y, p) \equiv \mathrm{ind}_{\mathbb{I} \to A}(t, \mathrm{rec}_\mathbb{I}^A(x, y, p))$$ since by interval recursion one has a path $\mathrm{rec}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A$ such that $$\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(0) \equiv x \quad \mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(1) \equiv y \quad \mathrm{ap}_{\mathrm{rec}_\mathbb{I}^{A}(x, y, p)}^{=}(0, 1, \mathrm{toeq}_A(\mathrm{id}_\mathbb{I})) \equiv p$$ Thus, one could do everything here that one could do in Martin-Löf type theory with an interval higher inductive type. \subsection{Kan operations} \begin{theorem} The fillers of identifications: Given paths $f:\mathbb{I} \to A$ and $g:\mathbb{I} \to A$, one could construct a function $\mathrm{filleq}_A(f, g):(f(0) =_A g(0)) \to (f(1) =_A g(1))$. \end{theorem} This is defined by double path induction by sending the constant path of $x$ in each parameter to its filler of identifications, which is just the identity function on $x =_A x$ $$x:A \vdash \mathrm{filleq}_A(\lambda i:\mathbb{I}.x, \lambda i:\mathbb{I}.x) \equiv \mathrm{id}_{x =_A x}:(x =_A x) \to (x =_A x)$$ \begin{theorem} Identity types are symmetric: Given elements $x:A$, $y:A$ and identification $p:x =_A y$, one could construct an identification $\mathrm{sym}_A(x, y, p):(y =_A x)$. \end{theorem} By interval recursion, there are paths $\mathrm{rec}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A$. By evaluating the fillers of the recursively defined path and the identity path on $x$ at reflexivity of $x$, one gets the needed identity: $$\mathrm{sym}_A(x, y, p) \equiv \mathrm{filleq}_A(\mathrm{rec}_\mathbb{I}^A(x, y, p), \lambda i:\mathbb{I}.x, \mathrm{refl}_A(y)):(y =_A x)$$ $$ \begin{array}{ccccc} & x & \overset{\mathrm{refl}_A(x)}= & x & \\ p & \Vert & & \Vert & \mathrm{refl}_A(x) \\ & y & \underset{\mathrm{sym}_A(x, y, p)}= & x & \\ \end{array} $$ \begin{theorem} Identity types are transitive: Given elements $x:A$, $y:A$, $z:A$ and identifications $p:x =_A y$ and $q:y =_A z$, one could construct an identification $\mathrm{trans}_A(x, y, z, p, q):(x =_A z)$. \end{theorem} By interval recursion, there is a path $\mathrm{rec}_\mathbb{I}^A(y, z, q):\mathbb{I} \to A$. By evaluating the fillers of the constant path of $x$ and the path of $q$ at $p$, one gets the needed identity: $$\mathrm{trans}_A(x, y, z, p, q) \equiv \mathrm{filleq}_A(\lambda i:\mathbb{I}.x, \mathrm{rec}_\mathbb{I}^A(y, z, q), p):(x =_A z)$$ $$ \begin{array}{ccccc} & x & \overset{p}= & y & \\ \mathrm{refl}_A(x) & \Vert & & \Vert & q \\ & x & \underset{\mathrm{trans}_A(x, y, z, p, q)}= & z & \\ \end{array} $$ \begin{theorem} The filler of squares: In addition, one has a dependent function $$\mathrm{fillsq}_A(f, g):\prod_{p:f(0) =_A g(0)} \mathrm{trans}_A(f(0), f(1), g(1), \mathrm{toeq}_A(f), \mathrm{filleq}_A(f, g, p)) =_{f(0) =_A g(0)} \mathrm{trans}_A(f(0), g(0), g(1), p, \mathrm{toeq}_A(g))$$ \end{theorem} This is inductively defined by $$\mathrm{fillsq}_A(\lambda i:\mathbb{I}.x, \lambda i:\mathbb{I}.x) \equiv \lambda p:x =_A x.\mathrm{refl}_{x =_A x}(p):\prod_{p:x =_A x} p =_{x =_A x} p$$ since $$\mathrm{trans}_A((\lambda i:\mathbb{I}.x)(0), (\lambda i:\mathbb{I}.x)(1), (\lambda i:\mathbb{I}.x)(0), \mathrm{toeq}_A(\lambda i:\mathbb{I}.x), \mathrm{filleq}_A(\lambda i:\mathbb{I}.x, \lambda i:\mathbb{I}.x, p)) \equiv p$$ $$\mathrm{trans}_A((\lambda i:\mathbb{I}.x)(0), (\lambda i:\mathbb{I}.x)(1), (\lambda i:\mathbb{I}.x)(0), p, \mathrm{toeq}_A(\lambda i:\mathbb{I}.x)) \equiv p$$ This completes the following commutative square: $$ \begin{array}{ccccc} & f(0) & \overset{p}= & g(0) & \\ \mathrm{toeq}_A(f) & \Vert & \overset{\mathrm{fillsq}_A(f, g, p)}= & \Vert & \mathrm{toeq}_A(g) \\ & f(1) & \underset{\mathrm{filleq}_A(f, g, p)}= & g(1) & \\ \end{array} $$ category: redirected to nlab