nLab bracket type

Contents

Context

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

semantics

Contents

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

Definition

As a higher inductive type

In dependent type theory, the propositional truncation of a type AA is defined as the higher inductive type generated by the two constructors

isinhab:A[A]\mathrm{isinhab} \colon A \to [A]
supp: x:A y:Aisinhab(x)= [A]isinhab(y)\mathrm{supp} \colon \prod_{x:A} \prod_{y:A} \mathrm{isinhab}(x) =_{[A]} \mathrm{isinhab}(y)

In any dependent type theory with identity types, given type AA, 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.

The induction principle states that if we have a family of mere propositions B(x)B(x) indexed by x:Ax:A and we have f: x:AB(isinhab(x))f:\prod_{x:A} B(isinhab(x)), then there is an induced g: z:supp(A)B(z)g:\prod_{z:supp(A)} B(z) such that g(isinhab(a))f(a)g(isinhab(a)) \equiv f(a) for all a:Aa:A.

Inference rules

The inference rules for bracket types are as follows:

  • Formation rules for bracket types:
ΓAtypeΓ[A]type\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash [A] \; \mathrm{type}}
  • Introduction rules for bracket types:
ΓAtypeΓ,x:A[x]:[A]type\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A \vdash [x]:[A] \; \mathrm{type}}
ΓAtypeΓ,x:A,y:Atrunc A(x,y):[x]= [A][y]type\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A \vdash \mathrm{trunc}_A(x, y):[x] =_{[A]} [y] \; \mathrm{type}}
  • Elimination rules for bracket types:
ΓAtypeΓ,x:AB(x)typeΓp: x:A y:B(x) z:B(x)y= B(x)zΓf: x:AB([x])Γ,x:[A]ind [A] B()(p,f,x):B(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash p:\prod_{x:A} \prod_{y:B(x)} \prod_{z:B(x)} y =_{B(x)} z \quad \Gamma \vdash f:\prod_{x:A} B([x])}{\Gamma, x:[A] \vdash \mathrm{ind}_{[A]}^{B(-)}(p, f, x):B(x)}
  • Computation rules for bracket types
ΓAtypeΓ,x:AB(x)typeΓp: x:A y:B(x) z:B(x)y= B(x)zΓf: x:AB([x])Γa:AΓind [A] B()(p,f,[a])f(a):B([a])\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash p:\prod_{x:A} \prod_{y:B(x)} \prod_{z:B(x)} y =_{B(x)} z \quad \Gamma \vdash f:\prod_{x:A} B([x]) \quad \Gamma \vdash a:A}{\Gamma \vdash \mathrm{ind}_{[A]}^{B(-)}(p, f, [a]) \equiv f(a):B([a])}

With a type of all propositions

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

[A] P:Prop(AEl(P))El(P)[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 boolean domain. The bracket type of a type AA is the localization of AA at the unique function 𝟚𝟙\mathbb{2} \to \mathbb{1}.

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

By definition, the type of functions (𝟙[A])(𝟚[A])(\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)(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.

As a sequential colimit

Let A*BA * B denote the join type of AA and BB, and let A *(n)A^{*(n)} be the iterated join type, inductively defined on the natural numbers by A *(0)A^{*(0)} \coloneqq \emptyset and A *(n+1)A *(n)*AA^{*(n + 1)} \coloneqq A^{*(n)} * A.

Then the propositional truncation of AA is the sequential colimit of the sequence of functions

A *(0)inrA *(1)inrA *(2)inrA^{*(0)} \overset{\mathrm{inr}}\to A^{*(1)} \overset{\mathrm{inr}}\to A^{*(2)} \overset{\mathrm{inr}}\to \ldots

As a quotient set

Let AA be a type and R(x,y)R(x, y) be a binary family of contractible types indexed by x:Ax:A and y:Ay:A, so that the product projection function for the dependent sum type

p 1:( z:A×AR(π 1(z),π 2(z)))(A×A)p_1:\left(\sum_{z:A \times A} R(\pi_1(z), \pi_2(z))\right) \to (A \times A)

is an equivalence of types. Then the propositional truncation of AA is the quotient set A/RA / R. (The quotient set in dependent type theory can be defined using inference rules without propositional truncations.)

Using functions from the boolean domain

There is another definition of the bracket type as a higher inductive type using functions from the boolean domain. The bracket type is generated by the two constructors

isinhab:A[A]\mathrm{isinhab} \colon A \to [A]
supp: f:bool[A]f(false)= [A]f(true)\mathrm{supp} \colon \prod_{f:\mathrm{bool} \to [A]} f(\mathrm{false}) =_{[A]} f(\mathrm{true})

The induction principle states that if we have a family of mere propositions B(x)B(x) indexed by x:Ax:A and we have f: x:AB(isinhab(x))f:\prod_{x:A} B(\mathrm{isinhab}(x)), then there is an induced g: z:supp(A)B(z)g:\prod_{z:\mathrm{supp}(A)} B(z) such that g(isinhab(a))f(a)g(\mathrm{isinhab}(a)) \equiv f(a) for all a:Aa:A. Here, a mere proposition is defined as a type AA for which every function from the boolean domain is a weakly constant function, or equivalently, that f:boolAf:\mathrm{bool} \to A satisfies f(false)= Af(true)f(\mathrm{false}) =_A f(\mathrm{true}).

isProp(A) f:boolAf(false)= Af(true)\mathrm{isProp}(A) \coloneqq \prod_{f:\mathrm{bool} \to A} f(\mathrm{false}) =_A f(\mathrm{true})

Using hubs and spokes

In section 7.3 of the HoTT Book UFP13, the authors give another definition of the propositional truncation using the hubs and spokes construction developed in section 6.7. Since the boolean domain is the zero-dimensional sphere, the propositional truncation of AA is a higher inductive type generated by

  • A function []:A[A][-]:A \to [A]

  • For each function r:boolAr:\mathrm{bool} \to A, a hub point h(r):Ah(r):A

  • For each function r:boolAr:\mathrm{bool} \to A and each boolean x:boolx:\mathrm{bool}, a spoke path s r(x):r(x)= Ah(r)s_r(x):r(x) =_A h(r)

Properties

Weakly constant functions

In dependent type theory, a weakly constant function from type AA to BB is a function f:ABf:A \to B with a dependent function p: x:A y:Af(x)= Bf(y)p:\prod_{x:A} \prod_{y:A} f(x) =_B f(y).

Given a weakly constant function f:ABf:A \to B with p: x:A y:Af(x)= Bf(y)p:\prod_{x:A} \prod_{y:A} f(x) =_B f(y), by the recursion principle of bracket types, one has

rec [A] B(f,p):[A]B\mathrm{rec}_{[A]}^B(f, p):[A] \to B

such that

rec [A] B(f,p)(isinhab(x))f(x):B\mathrm{rec}_{[A]}^B(f, p)(\mathrm{isinhab}(x)) \equiv f(x):B
ap rec [A] B(f,p)(supp(x,y))p(x,y):f(x)= Bf(y)\mathrm{ap}_{\mathrm{rec}_{[A]}^B(f, p)}(\mathrm{supp}(x, y)) \equiv p(x, y):f(x) =_B f(y)

In particular, by the judgmental congruence rule for the introduction rule of function types, every weakly constant function f:ABf:A \to B with p: x:A y:Af(x)= Bf(y)p:\prod_{x:A} \prod_{y:A} f(x) =_B f(y) factors through [A][A] by

frec [A] B(f,p)isinhabf \equiv \mathrm{rec}_{[A]}^B(f, p) \circ \mathrm{isinhab}

Weakly constant functions can also be regarded directly as functions [A]B[A] \to B, similar to how paths in AA can be regarded as functions 𝕀A\mathbb{I} \to A from the the interval type rather than the application of said function along the path generator of the interval type.

Functions from the interval type

Given a type AA, there exists a function AA𝕀[A]A \to A \to \mathbb{I} \to [A] defined by

λx:A.λy:A.rec 𝕀([x],[y],supp(x,y)):AA𝕀[A]\lambda x:A.\lambda y:A.\mathrm{rec}_{\mathbb{I}}([x], [y], \mathrm{supp}(x, y)):A \to A \to \mathbb{I} \to [A]

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 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

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

Discussion in the context of homotopy type theory:

Exposition:

Formalization:

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

More on the universal property of propositional truncation:

For propositional truncations as sequential colimits, see section 26.5 of

as well as section 16.2 of the lecture notes:

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

That propositional truncations with judgmental computation rules along with the boolean domain imply function extensionality:

Last revised on July 6, 2024 at 11:37:49. See the history of this page for a list of all contributions to it.