n-truncation modality

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

- homotopy hypothesis-theorem
- delooping hypothesis-theorem
- periodic table
- stabilization hypothesis-theorem
- exactness hypothesis
- holographic principle

- (n,r)-category
- Theta-space
- ∞-category/∞-category
- (∞,n)-category
- (∞,2)-category
- (∞,1)-category
- (∞,0)-category/∞-groupoid
- n-category = (n,n)-category
- 2-category, (2,1)-category
- 1-category
- 0-category
- (?1)-category?
- (?2)-category?

- n-poset = (n-1,n)-category
- n-groupoid = (n,0)-category

- categorification/decategorification
- geometric definition of higher category
- algebraic definition of higher category
- stable homotopy theory

For all $n \in \{-2, -1, 0,1,2,3, \cdots\}$, n-truncation is a modality (in homotopy type theory).

$(-2)$-truncation is the unit type modality (constant on the unit type).

$(-1)$-truncation is given by forming *bracket types*, turning types into genuine propositions.

Classically, this is the same as the double negation modality; in general, the bracket type ${\|A\|_{-1}}$ only entails the double negation $\neg(\neg{A})$:

there is a canonical function

${\|A\|_{-1}} \longrightarrow \neg(\neg{A})$

and this is a 1-epimorphism precisely if the law of excluded middle holds.

(…)

The $(-1)$-truncation in the context is forming the bracket type hProp. $n$-truncation is given by a higher inductive type.

homotopy level | n-truncation | homotopy theory | higher category theory | higher topos theory | homotopy type theory |
---|---|---|---|---|---|

h-level 0 | (-2)-truncated | contractible space | (-2)-groupoid | true/unit type/contractible type | |

h-level 1 | (-1)-truncated | contractible-if-inhabited | (-1)-groupoid/truth value | (0,1)-sheaf/ideal | mere proposition/h-proposition |

h-level 2 | 0-truncated | homotopy 0-type | 0-groupoid/set | sheaf | h-set |

h-level 3 | 1-truncated | homotopy 1-type | 1-groupoid/groupoid | (2,1)-sheaf/stack | h-groupoid |

h-level 4 | 2-truncated | homotopy 2-type | 2-groupoid | (3,1)-sheaf/2-stack | h-2-groupoid |

h-level 5 | 3-truncated | homotopy 3-type | 3-groupoid | (4,1)-sheaf/3-stack | h-3-groupoid |

h-level $n+2$ | $n$-truncated | homotopy n-type | n-groupoid | (n+1,1)-sheaf/n-stack | h-$n$-groupoid |

h-level $\infty$ | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h-$\infty$-groupoid |

- Mike Shulman,
*Higher modalities*, talk at UF-IAS-2012, October 2012 (pdf)

Last revised on January 5, 2015 at 10:15:18. See the history of this page for a list of all contributions to it.