bracket type


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

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

syntax object language

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

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




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][A]); in homotopy type theory it can be identified with the higher inductive type isInhabisInhab.


In type theory


In homotopy type theory

We discuss the definition in homotopy type theory.

For AA a type, the support of AA denoted supp(A)supp(A) or isInhab(A)isInhab(A) or τ 1A\tau_{-1} A or A 1\| A \|_{-1} or A\| A \| or, lastly, [A][A], is the higher inductive type defined by the two constructors

a:Aisinhab(a):supp(A) a \colon A \;\vdash \; isinhab(a) \colon supp(A)
x:supp(A),y:supp(A)inpath(x,y):(x=y), 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)supp(A) is the type which is universal with the property that the terms of AA map to it and that any two term of AA become equivalent in supp(A)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)supp(A) says that if BB is a mere proposition and we have f:ABf: A \to B, then there is an induced g:supp(A)Bg : supp(A) \to B such that g(isinhab(a))f(a)g(isinhab(a)) \equiv f(a) for all a:Aa:A. In other words, any mere proposition which follows from (the inhabitedness of) AA already follows from supp(A)supp(A). Thus, supp(A)supp(A), as a mere proposition, contains no more information than the inhabitedness of AA.

For more see at n-truncation modality.


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 CC is as follows.

A dependent type (a type in context XX)

x:XA(x):Typex\colon X \vdash A(x) \colon Type

is interpreted in CC as an arbitrary morphism

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

The corresponding bracket type

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

is interpreted then as the image-factorization

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

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

homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/​unit type/​contractible type
h-level 1(-1)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-\infty-groupoid


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

Exposition in the context of homotopy type theory is in

Formalization in the context of homotopy type theory is in

Discussion of this in the more general context of truncations is in

Revised on September 26, 2017 04:21:09 by David Corfield (