nLab bracket type

Idea

There are various different paradigms for the interpretation of predicate logic in type theory. In “logic-enriched type theory”, there is a separate class of “propositions” from the class of “types”. But we can also identify propositions with particular types. In the propositions as types-paradigm, every proposition is a type, and also every type is identified with a proposition (the proposition that it is an inhabited type).

By contrast, in the paradigm that may be called propositions as some types, every proposition is a type, but not every type is a proposition. The types which are propositions are generally those which “have at most one inhabitant” — in homotopy type theory this is called being of h-level 1 or being a (-1)-type. This paradigm is often used in the categorical semantics of type theory, such as the internal logic of various kinds of categories.

Under “propositions as types”, all type-theoretic operations represent corresponding logical operations (dependent sum is the existential quantifier, dependent product the universal quantifier, and so on). However, under “propositions as some types”, not every such operation preserves the class of propositions; this is particularly the case for dependent sum and disjunction(or). Thus, in order to obtain the correct logical operations, we need to reflect these constructions back into propositions somehow, finding the “underlying proposition”, corresponding to the (-1)-truncation/h-level 1-projection. This operation in type theory is called the bracket type (when denoted $[A]$); in homotopy type theory it can be identified with the higher inductive type $isInhab$.

Definition

In homotopy type theory

In homotopy type theory, the propositional truncation of a type $A$ is defined as the higher inductive type generated by the two constructors

$$isinhab\colon A \to [A]$$

$$proptrunc \colon \prod_{x:A} \prod_{y:A} isinhab(x) =_{[A]} isinhab(y)$$

More generally

In any dependent type theory with identity types, given type $A$, the support of $A$ denoted $supp(A)$ or $isInhab(A)$ or $\tau_{-1} A$ or $\| A \|_{-1}$ or $\| A \|$ or, lastly, $[A]$, is the higher inductive type defined by the two constructors

$$a \colon A \;\vdash \; isinhab(a) \colon supp(A)$$

$$x \colon supp(A) \;,\; y \colon supp(A) \;\vdash \; inpath(x,y) \colon (x = y) \,,$$

where in the last sequent on the right we have the identity type. (Voevodsky, HoTTLibrary)

This says that $supp(A)$ is the type which is universal with the property that the terms of $A$ map to it and that any two term of $A$ become equivalent in $supp(A)$.

In Agda syntax this is

data isinhab {i : Level} (A : Set i) : Set i where
  inhab : A → isinhab A
  inhab-path : (x y : isinhab A) → x ≡ y

The recursion principle for $supp(A)$ says that if $B$ is a mere proposition and we have $f: A \to B$, then there is an induced $g : supp(A) \to B$ such that $g(isinhab(a)) \equiv f(a)$ for all $a:A$. In other words, any mere proposition which follows from (the inhabitedness of) $A$ already follows from $supp(A)$. Thus, $supp(A)$, as a mere proposition, contains no more information than the inhabitedness of $A$.

With a type of all propositions

Suppose the dependent type theory has a univalent type of all propositions $(\mathrm{Prop}, \mathrm{El})$. Then the bracket type of $A$ could be defined as the type

$$[A] \coloneqq \prod_{P:\mathrm{Prop}} (A \to \mathrm{El}(P)) \to \mathrm{El}(P)$$

As localization

Let $\mathbb{1}$ be the unit type and let $\mathbb{2}$ be the two-valued type. The bracket type of a type $A$ is the localization of $A$ at the unique function $\mathbb{2} \to \mathbb{1}$.

$$\left[A\right] \coloneqq L_\mathbb{2}(A)$$

By definition, the type of functions $(\mathbb{1} \to \left[A\right]) \to (\mathbb{2} \to \left[A\right])$ is an equivalence of types.

This is the special case of the n-truncation modality as the n-truncation modality is localization at the unique map from the $(n + 1)$-dimensional sphere type to the unit type, and $\mathbb{2}$ is the zero-dimensional sphere type.

For more see at n-truncation modality.

Semantics

One presentation of the internal type theory of regular categories consists of dependent type theory with the unit type, strong extensional equality types?, strong dependent sums, and bracket types. (The internal logic of a regular category can alternatively be presented as a logic-enriched type theory?.)

The semantics of bracket types in a regular category $C$ is as follows.

A dependent type (a type in context $X$)

$$x\colon X \vdash A(x) \colon Type$$

is interpreted in $C$ as an arbitrary morphism

$$\array{ A \\ \downarrow \\ X } \,.$$

The corresponding bracket type

$$x\colon X \vdash [A(x)] \colon Type$$

is interpreted then as the image-factorization

$$\array{ A &&\to&& [A] & := im(A \to X) \\ & \searrow && \swarrow \\ && X \,. }$$

Therefore $[A] \to X$ is a monomorphism, and hence the interpretation of a proposition about the elements of $X$.

Related concepts

• image, inhabited type

• n-truncation modality

• propositional truncation object

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

References

The original articles are

• M.E. Maietti, The Type Theory of Categorical Universes PhD thesis, Università Degli Studi di Padova, 1998

(which speaks of “mono types”) and

• Frank Pfenning, Intensionality, extensionality, and proof irrelevance in modal type theory, In Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS’01), June 2001.

• Steve Awodey, Andrej Bauer, Propositions as $[$Types$]$, Journal of Logic and Computation, 14 (2004) 447-471 [doi:10.1093/logcom/14.4.447, pdf]

Discussion in the context of homotopy type theory:

• Univalent Foundations Project, §3.7 Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

Exposition:

• Mike Shulman, Minicourse on homotopy type theory (2012) (web)

Formalization:

• Vladimir Voevodsky, The hProp version of the “inhabited” construction. (web)

• CoqHoTT library, IsInhab.v

Discussion in the more general context of $n$-truncations:

• Guillaume Brunerie, Truncations and truncated higher inductive types (web)

More on the universal property of propositional truncation:

• Nicolai Kraus, The General Universal Property of the Propositional Truncation, in TYPES 2014 Leibniz International Proceedings in Informatics (LIPIcs) 39 (2015) [arXiv:1411.2682, doi:10.4230/LIPIcs.TYPES.2014.111]

For n-truncations as localizations at sphere types, see:

• David Jaz Myers, Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory (arXiv:2205.15887)