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 inhabited).

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 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 $\mathrm{isInhab}$.

Properties

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?.)

Semantics

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

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

$$x:X⊢A(x):\mathrm{Type}$$x\colon X \vdash A(x) \colon Type

is interpreted in $C$ as an arbitrary morphism

$$\begin{array}{c}A\\ \downarrow \\ X\end{array}.$$\array{ A \\ \downarrow \\ X } \,.

The corresponding bracket type

$$x:X⊢[A(x)]:\mathrm{Type}$$x\colon X \vdash [A(x)] \colon Type

is interpreted then as the image-factorization

$$\begin{array}{cccccc}A& & \to & & [A]& :=\mathrm{im}(A\to X)\\ & \searrow & & \swarrow \\ & & X.\end{array}$$\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$.

References

The original articles are

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

(which speaks of “mono types”),

• F. 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. Volume 14, Issue 4, August 2004, pp. 447-471 (pdf)