nLab
homotopy level

Context

Type theory

natural deduction metalanguage, practical foundations

judgement
hypothetical judgement, sequent
- antecedents $\vdash$ consequent, succedents

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

calculus of constructions

syntax object language

theory, axiom
proposition/type (propositions as types)
definition/proof/program (proofs as programs)
theorem

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

logic	category theory	type theory
true	terminal object/(-2)-truncated object	h-level 0-type/unit type

false initial object empty type

proposition (-1)-truncated object h-proposition, mere proposition

proof generalized element program

cut rule composition of classifying morphisms / pullback of display maps substitution

cut elimination for implication counit for hom-tensor adjunctionbeta reduction

introduction rule for implication unit for hom-tensor adjunctioneta conversion

logical conjunction product product type

disjunction coproduct ((-1)-truncation of)sum type (bracket type of)

implication internal hom function type

negation internal hom into initial object function type into empty type

universal quantification dependent product dependent product type

existential quantification dependent sum ((-1)-truncation of)dependent sum type (bracket type of)

equivalence path space object identity type

equivalence class quotient quotient type

induction colimit inductive type, W-type, M-type

higher induction higher colimit higher inductive type

completely presented set discrete object/0-truncated object h-level 2-type/preset/h-set

set internal 0-groupoid Bishop set/setoid

universe object classifier type of types

modality closure operator, (idemponent) monad modal type theory, monad (in computer science)

linear logic(symmetric, closed) monoidal category linear type theory/quantum computation

proof net string diagram quantum circuit

(absence of) contraction rule(absence of) diagonal no-cloning theorem

synthetic mathematics domain specific embedded programming language

</table>

homotopy levels

Edit this sidebar

Homotopy theory

Contents

Idea
Related concepts

Idea

The term homotopy level (or h-level), originating in homotopy type theory, is another name for the notion of truncation (particularly in (∞,1)-categories and their internal language of homotopy type theory) in which the numbering is offset by 2:

a homotopy n-type is a type of homotopy level $n+2$ .

This offset in counting enables it to “start” at 0 rather than (-2), which is convenient when defining it by induction over the natural numbers in type theory. Thus, the correspondence between the various terminologies is indicated in the following table.

Related concepts

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

Last revised on March 9, 2014 at 23:28:22. See the history of this page for a list of all contributions to it.