# Contents

## Idea

A modal dependent type theory with the sharp modality $\sharp$ and the flat modality $\flat$. Spatial type theory which is also a homotopy type theory is called spatial homotopy type theory.

## Presentation

In this presentation of spatial type theory, we assume a dependent type theory with crisp term judgments $a::A$ in addition to the usual (cohesive) type and term judgments $A \; \mathrm{type}$ and $a:A$, as well as context judgments $\Xi \vert \Gamma \; \mathrm{ctx}$ where $\Xi$ is a list of crisp term judgments, and $\Gamma$ is a list of cohesive term judgments. A crisp type is a type in the context $\Xi \vert ()$, where $()$ is the empty list of cohesive term judgments.

### Identity types

In addition, we also assume the dependent type theory has typal equality:

• Formation rule for identity types:

$\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma \vdash a:A \quad \Xi \vert \Gamma \vdash b:A}{\Xi \vert \Gamma \vdash a =_A b \; \mathrm{type}}$
• Introduction rule for identity types:

$\frac{\Xi \vert \Gamma \vdash A \; \mathrm{type} \quad \Xi \vert \Gamma \vdash a:A}{\Xi \vert \Gamma \vdash \mathrm{refl}_A(a) : a =_A a}$
• Elimination rule for identity types:

$\frac{\Xi \vert \Gamma, x:A, y:A, p:a =_A b \vdash C \; \mathrm{type} \quad \Xi \vert \Gamma, z:A \vdash t:C[z/a, z/b, \mathrm{refl}_A(z)/p] \quad \Xi \vert \Gamma \vdash a:A \quad \Xi \vert \Gamma \vdash b:A \quad \Xi \vert \Gamma \vdash q:a =_A b}{\Xi \vert \Gamma \vdash \mathrm{ind}_{=_A}^{x,y,p.C}(z.t, a, b, q):C[a, b, q/x, y, p]}$
• Computation rules for identity types:

$\frac{\Xi \vert \Gamma, x:A, y:A, p:a =_A b \vdash C \; \mathrm{type} \quad \Xi \vert \Gamma, z:A \vdash t:C[z/a, z/b, \mathrm{refl}_A(z)/p] \quad \Xi \vert \Gamma \vdash a:A}{\Xi \vert \Gamma \vdash \beta_{=_A}^{x,y,p.C}(a):\mathrm{ind}_{=_A}^{x,y,p.C}(z.t, a, a, \mathrm{refl}(a)) =_{C[a, a, \mathrm{refl}_A(a)/x, y, p]} t}$

### Sharp modality

The sharp modality is given by the following rules:

• Formation rule for sharp types:
$\frac{\Xi, \Gamma \vert () \vdash A \; \mathrm{type}}{\Xi \vert \Gamma \vdash \sharp A \; \mathrm{type}}\sharp-\mathrm{form}$
• Introduction rule for sharp types:
$\frac{\Xi, \Gamma \vert () \vdash a:A}{\Xi \vert \Gamma \vdash a^\sharp:\sharp A}\sharp-\mathrm{intro}$
• Elimination rule for sharp types:
$\frac{\Xi \vert () \vdash a:\sharp A}{\Xi \vert \Gamma \vdash a_\sharp:A}\sharp-\mathrm{elim}$
• Computation rule for sharp types:
$\frac{\Xi \vert () \vdash a:A}{\Xi \vert \Gamma \vdash \beta_{\sharp A}(a):(a^\sharp)_\sharp =_A a}\sharp-\mathrm{comp}$
• Uniqueness rule for sharp types:
$\frac{\Xi \vert () \vdash a:\sharp A}{\Xi \vert \Gamma \vdash \eta_{\sharp A}(a):(a_\sharp)^\sharp =_{\sharp A} a}\sharp-\mathrm{uniq}$

### Flat modality

The flat modality is given by the following rules:

• Formation rule for flat types:
$\frac{\Xi, \Gamma \vert () \vdash A \; \mathrm{type}}{\Xi \vert \Gamma \vdash \flat A \; \mathrm{type}}\flat-\mathrm{form}$
• Introduction rule for flat types:
$\frac{\Xi, \Gamma \vert () \vdash a:A}{\Xi \vert \Gamma \vdash a^\flat:\flat A}\flat-\mathrm{intro}$
• Elimination rule for flat types:
$\frac{\Xi \vert \Gamma, x:\flat A \vdash C \; \mathrm{type} \quad \Xi \vert \Gamma \vdash M:\flat A \quad \Xi, u::A \vert \Gamma \vdash N : C[u^\flat/x]}{\Xi \vert \Gamma \vdash (\mathrm{let}\; u^\flat \coloneqq M \;\mathrm{in}\; n):C[M/x]}\flat-\mathrm{elim}$
• Computation rule for flat types:
$\frac{\Xi \vert \Gamma, x:\flat A \vdash C \; \mathrm{type} \quad \Xi \vert () \vdash M:\flat A \quad \Xi, u::A \vert \Gamma \vdash N : C[u^\flat/x]}{\Xi \vert \Gamma \vdash \beta_{\flat}(M, N):(\mathrm{let}\; u^\flat \coloneqq M \;\mathrm{in}\; N) =_{C[M^\flat/x]} N[M/u]}\flat-\mathrm{comp}$

## Examples

A cohesive homotopy type theory is a spatial homotopy type theory which additionally has an axiom of cohesion and a shape modality. Examples of this include