nLab subtype

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

In type theory, the notion of subtypes is the analog of subsets in set theory.

In the presence of a type universe Prop Prop of propositions (alternatively denoted “Ω\Omega”), the subtypes of a given A:TypeA \colon Type may be simply be identified with the function type from AA to PropProp:

Sub(A)=Prop AAPropAΩ. Sub(A) \;\; = \;\; Prop_A \;\; \equiv \;\; A \to Prop \;\; \equiv \;\; A \to \Omega \,.

In topos-semantics, PropProp is interpreted as the subobject classifier and subtypes as subobjects.

Notice that with PropProp itself being a subtype of a type universe TypeType, the subtypes of AA are thus a special case of the AA-dependent types

Type AAType, Type_A \;\; \equiv \;\; A \to Type \,,

namely those whose fiber type over a:Aa \colon A is the proposition asserting that “aa is contained in the subtype”.

This is equivalent to other definitions of subtypes, which one can make sense of also in the absence of a Prop-universe.

Notice here that in set theory, there are in fact two notions of subsets:

In dependent type theory, a similar distinction can be made between the two notions of subtypes, resulting in material subtypes and structural subtypes.

Definition

Material subtypes

We work with a Russell type of all propositions Ω\Omega.

Definition

The power set of a type AA is defined as the function type from AA to the Russell type of all propositions Ω\Omega, 𝒫(A)AΩ\mathcal{P}(A) \coloneqq A \to \Omega.

The power set of a type AA is always a set because its codomain, the Russell type of all propositions Ω\Omega, is a set due to the univalence axiom or propositional extensionality.

Definition

A material subtype on AA is an element of the power set B:𝒫(A)B:\mathcal{P}(A).

Definition

The local membership relation x ABx \in_A B between elements x:Ax:A and material subtypes B:𝒫(A)B:\mathcal{P}(A) is defined as

x ABB(x)x \in_A B \coloneqq B(x)

Theorem

Given a type AA and a subtype P:APropP:A \to \mathrm{Prop}, one can construct a subtype [P] 0:[A]Prop[P]_0:[A] \to \mathrm{Prop} of the set truncation of AA such that for all x:Ax:A, P(x)=[P] 0([x] 0)P(x) = [P]_0([x]_0).

Proof

By propositional extensionality, the type of propositions Prop\mathrm{Prop} is a set, and by the universal property of set truncations, given any type AA, set BB, and function f:ABf:A \to B, one can construct a unique function u:[A] 0Bu:[A]_0 \to B such that for all x:Ax:A, f(x)=u([x] 0)f(x) = u([x]_0). This is just the special case of the universal property of set truncations where the codomain is the set of propositions.

Structural subtypes

Definition

A structural subtype of AA is a type BB with an embedding i:BAi:B \hookrightarrow A. AA is a supertype of BB.

Comparison between material subtypes, structural subtypes, and predicates

material subtypepredicatestructural subtype
B:𝒫(A)B:\mathcal{P}(A)x:Ax ABB(x)x:A \vdash x \in_A B \coloneqq B(x) x:Ax AB\sum_{x:A} x \in_A B
λx:A.B(x):𝒫(A)\lambda x:A.B(x):\mathcal{P}(A)x:AB(x)x:Ap(x):isProp(B(x))x:A \vdash B(x) \qquad x:A \vdash p(x):\mathrm{isProp}(B(x)) x:AB(x)\sum_{x:A} B(x)
(λx:A. y:Bi(y)= Ax):𝒫(A)\left(\lambda x:A.\sum_{y:B} i(y) =_A x\right):\mathcal{P}(A)x:A y:Bi(y)= Axx:A \vdash \sum_{y:B} i(y) =_A xBi:BAB \qquad i:B \hookrightarrow A

Operations on material and structural subtypes

 Material subtypes

Definition

Given a type AA, the improper material subtype on AA is the material subtype A:𝒫(A)\Im_A:\mathcal{P}(A) such that for all elements x:Ax:A, x A Ax \in_A \Im_A is contractible.

Definition

Given a type AA, there is a binary operation ()():𝒫(A)×𝒫(A)𝒫(A)(-)\cap(-):\mathcal{P}(A) \times \mathcal{P}(A) \to \mathcal{P}(A) on the power set of AA called the binary intersection, such that for all material subtypes B:𝒫(A)B:\mathcal{P}(A) and C:𝒫(A)C:\mathcal{P}(A), BCB \cap C is defined as

(BC)(x)(x AB)(x AC)(B \cap C)(x) \coloneqq (x \in_A B) \wedge (x \in_A C)

for all x:Ax:A, where AB[A×B]A \wedge B \coloneqq [A \times B] is the disjunction of two types and [T][T] is the propositional truncation of TT.

Definition

Given a type AA and a type II, there is an function :(I𝒫(A))𝒫(A)\bigcap:(I \to \mathcal{P}(A)) \to \mathcal{P}(A) called the II-indexed intersection, such that for all families of material subtypes B:I𝒫(A)B:I \to \mathcal{P}(A), i:IB(i)\bigcap_{i:I} B(i) is defined as

( i:IB(i))(x)i:I.x AB(i)\left(\bigcap_{i:I} B(i)\right)(x) \coloneqq \forall i:I.x \in_A B(i)

for all x:Ax:A, where

x:A.B(x)[ x:AB(x)]\forall x:A.B(x) \coloneqq \left[\prod_{x:A} B(x)\right]

is the universal quantification of a type family and [T][T] is the propositional truncation of TT.

Definition

Given a type AA, the empty material subtype on AA is the material subtype A:𝒫(A)\emptyset_A:\mathcal{P}(A) such that for all elements x:Ax:A, x A Ax \in_A \emptyset_A is equivalent to the empty type.

Definition

Given a type AA, there is a binary operation ()():𝒫(A)×𝒫(A)𝒫(A)(-)\cup(-):\mathcal{P}(A) \times \mathcal{P}(A) \to \mathcal{P}(A) on the power set of AA called the binary union, such that for all material subtypes B:𝒫(A)B:\mathcal{P}(A) and C:𝒫(A)C:\mathcal{P}(A), BCB \cup C is defined as

(BC)(x)(x AB)(x AC)(B \cup C)(x) \coloneqq (x \in_A B) \vee (x \in_A C)

for all x:Ax:A, where AB[A+B]A \vee B \coloneqq [A + B] is the disjunction of two types and [T][T] is the propositional truncation of TT.

Definition

Given a type AA and a type II, there is an function :(I𝒫(A))𝒫(A)\bigcup:(I \to \mathcal{P}(A)) \to \mathcal{P}(A) called the II-indexed union, such that for all families of material subtypes B:I𝒫(A)B:I \to \mathcal{P}(A), i:IB(i)\bigcup_{i:I} B(i) is defined as

( i:IB(i))(x)i:I.x AB(i)\left(\bigcup_{i:I} B(i)\right)(x) \coloneqq \exists i:I.x \in_A B(i)

for all x:Ax:A, where

x:A.B(x)[ x:AB(x)]\exists x:A.B(x) \coloneqq \left[\sum_{x:A} B(x)\right]

is the existential quantification of a type family and [T][T] is the propositional truncation of TT.

Definition

Given a type AA, there is a binary relation B:𝒫(A),C:𝒫(A)B ACB:\mathcal{P}(A), C:\mathcal{P}(A) \vdash B \subseteq_A C on the power set of AA called the subtype inclusion relation, such that for all material subtypes B:𝒫(A)B:\mathcal{P}(A) and C:𝒫(A)C:\mathcal{P}(A), B ACB \subseteq_A C is defined as

B AC x:A(x AB)(x AC)B \subseteq_A C \coloneqq \prod_{x:A} (x \in_A B) \to (x \in_A C)

Definition

Given a type AA, there is a binary relation B:𝒫(A),C:𝒫(A)Eq A(B,C)B:\mathcal{P}(A), C:\mathcal{P}(A) \vdash \mathrm{Eq}_A(B, C) on the power set of AA called observational equality, such that for all material subtypes B:𝒫(A)B:\mathcal{P}(A) and C:𝒫(A)C:\mathcal{P}(A), Eq 𝒫(A)(B,C)\mathrm{Eq}_{\mathcal{P}(A)}(B, C) is defined as

Eq 𝒫(A)(B,C) x:A(x AB)(x AC)\mathrm{Eq}_{\mathcal{P}(A)}(B, C) \coloneqq \prod_{x:A} (x \in_A B) \simeq (x \in_A C)

Proposition

Axiom of extensionality: Given a type AA, for all subtypes B:𝒫(A)B:\mathcal{P}(A) and C:𝒫(A)C:\mathcal{P}(A), there is an equivalence of types between B= 𝒫(A)CB =_{\mathcal{P}(A)} C and Eq 𝒫(A)(B,C)\mathrm{Eq}_{\mathcal{P}(A)}(B, C).

Proof

For all x:Ax:A and B:𝒫(A)B:\mathcal{P}(A), since x ABx \in_A B is propositions, by the introduction rules of the Russell type of all propositions, x AB:Ωx \in_A B:\Omega. The univalence axiom for Ω\Omega states that (x AB)(x AC)(x \in_A B) \simeq (x \in_A C) is equivalent to (x AB)= Ω(x AC)(x \in_A B) =_\Omega (x \in_A C). Thus, Eq 𝒫(A)(B,C)\mathrm{Eq}_{\mathcal{P}(A)}(B, C) is equivalent to x:A(x AB)= Ω(x AC)\prod_{x:A} (x \in_A B) =_\Omega (x \in_A C). But by function extensionality, there is an equivalence of types between B= 𝒫(A)CB =_{\mathcal{P}(A)} C and x:A(x AB)= Ω(x AC)\prod_{x:A} (x \in_A B) =_\Omega (x \in_A C); hence there is an equivalence of types between B= 𝒫(A)CB =_{\mathcal{P}(A)} C and Eq 𝒫(A)(B,C)\mathrm{Eq}_{\mathcal{P}(A)}(B, C).

Definition

Given a type AA, a singleton subtype on AA is a material subtype S:𝒫(A)S:\mathcal{P}(A) such that there exists a unique x:Ax:A such that xSx \in S:

isSingleton(S)!x:A.xS\mathrm{isSingleton}(S) \coloneqq \exists!x:A.x \in S

Definition

Given a type TT, there is a binary function ()×():𝒫(T)×𝒫(T)𝒫(T×T)(-) \times (-):\mathcal{P}(T) \times \mathcal{P}(T) \to \mathcal{P}(T \times T) called the cartesian product of subtypes, defined by

(A×B)(a,b)(a TA)(b TB)(A \times B)(a, b) \coloneqq (a \in_T A) \wedge (b \in_T B)

for all elements a:Ta:T, b:Tb:T and subtypes A:𝒫(T)A:\mathcal{P}(T) and B:𝒫(T)B:\mathcal{P}(T).

Structural subtypes

Definition

Given a type TT, TT is the improper structural subtype, with embedding given by the identity function on TT.

Definition

Given a type TT and structural subtypes RR and SS with embeddings i R:RTi_R:R \hookrightarrow T and i S:STi_S:S \hookrightarrow T, the binary intersection of RR and SS is the pullback of the two embeddings into TT, or equivalently the dependent sum type

RS r:R s:Si R(r)= Ti S(s)R \cap S \coloneqq \sum_{r:R} \sum_{s:S} i_R(r) =_T i_S(s)

Definition

Given a type TT, an index type II, and a family of structural subtypes (R(i)) i:I(R(i))_{i:I} with a family of embeddings i R: i:IR(i)Ti_R:\prod_{i:I} R(i) \hookrightarrow T, the II-indexed intersection of (R(i)) i:I(R(i))_{i:I} is the dependent pullback of the embeddings into TT, or equivalently the dependent sum type

i:IR(i) t:T i:I r:R(i)i R(i,r)= Tt\bigcap_{i:I} R(i) \coloneqq \sum_{t:T} \prod_{i:I} \sum_{r:R(i)} i_R(i, r) =_T t

By definition of dependent pullback, the intersection of a family of structural subsets is a wide span, with dependent function

λj:I.λp: i:IR(i).π 1(π 2(p)(j)): j:I( i:IR(i))R(j)\lambda j:I.\lambda p:\bigcap_{i:I} R(i).\pi_1(\pi_2(p)(j)):\prod_{j:I} \left(\bigcap_{i:I} R(i)\right) \to R(j)

Definition

Given a type TT, the empty type is the empty structural subtype, with embedding given by any function from the empty type to TT.

Definition

Given a type TT and structural subtypes RR and SS with embeddings i R:RTi_R:R \hookrightarrow T and i S:STi_S:S \hookrightarrow T, the binary union of RR and SS is the pushout type

RSR π 1;π 1π 2 RSSR \cup S \coloneqq R \sqcup^{R \cap S}_{\pi_1 ; \pi_1' \circ \pi_2} S

where π 1\pi_1 and π 2\pi_2 are the first and second projection functions for the first dependent sum type and π 1\pi_1' is the first projection function for the second dependent sum type for the intersection as defined above ( r:R s:Si R(r)= Ti S(s)\sum_{r:R} \sum_{s:S} i_R(r) =_T i_S(s))

Definition

Given a type TT, an index type II, and a family of structural subtypes (R(i)) i:I(R(i))_{i:I} with a family of embeddings i R: i:IR(i)Ti_R:\prod_{i:I} R(i) \hookrightarrow T, the II-indexed union of (R(i)) i:I(R(i))_{i:I} is the dependent pushout of the dependent pullback

λj.λp.π 1(π 2(p)(j)): j:I( i:IR(i))R(j)\lambda j.\lambda p.\pi_1(\pi_2(p)(j)):\prod_{j:I} \left(\bigcap_{i:I} R(i)\right) \to R(j)

of the embeddings into TT,

i:IR(i) i:I i:IR(i),λj.λp.π 1(π 2(p)(j))R(i)\bigcup_{i:I} R(i) \coloneqq \bigsqcup_{i:I}^{\bigcap_{i:I} R(i), \lambda j.\lambda p.\pi_1(\pi_2(p)(j))} R(i)

Definition

Given a type TT, a singleton subtype of TT is a contractible type SS with an embedding i:STi:S \hookrightarrow T.

Definition

Given a type TT and structural subtypes RR and SS with embeddings i R:RTi_R:R \hookrightarrow T and i S:STi_S:S \hookrightarrow T, the cartesian product of RR and SS is simply the product R×SR \times S. The associated embedding i R×S:(R×S)(T×T)i_{R \times S}:(R \times S) \hookrightarrow (T \times T) is defined by

i R×S(a)(i R(π 1(a)),i S(π 2(a)))i_{R \times S}(a) \coloneqq (i_R(\pi_1(a)), i_S(\pi_2(a)))

for all a:R×Sa:R \times S, where π 1\pi_1 and π 2\pi_2 are the first and second product projection functions defined in the inference rules of the negative product type R×SR \times S.

Decidable subtypes

Given a Russell type of propositions, a subtype P:APropP:A \to \mathrm{Prop} is a decidable subtype if for all x:Ax:A, P(x)P(x) satisfies the law of excluded middle

isDecidable(P) x:AP(x)¬P(x)\mathrm{isDecidable}(P) \equiv \prod_{x:A} P(x) \vee \neg P(x)

Similarly, given a Tarski type of propositions, a subtype P:APropP:A \to \mathrm{Prop} is a decidable subtype if for all x:Ax:A, P(x)P(x) satisfies the law of excluded middle

isDecidable(P) x:AEl(P(x)¬P(x))\mathrm{isDecidable}(P) \equiv \prod_{x:A} \mathrm{El}(P(x) \vee \neg P(x))

For all types AA, there exists an equivalence between the type of decidable subtypes of AA and the type of boolean-valued functions of AA

toDecidSub:(ABool)( P:APropisDecidable(P))\mathrm{toDecidSub}:\left(A \to \mathrm{Bool}\right) \simeq \left(\sum_{P:A \to \mathrm{Prop}} \mathrm{isDecidable}(P)\right)

The membership relation of decidable subsets is defined by whether the boolean-valued function evaluations is true

xPtoDecidSub 1(P)(x)= truex \in P \coloneqq \mathrm{toDecidSub}^{-1}(P)(x) =_\mathrm{true}

Decidable subtypes are closed under the empty subtype, the improper subtype, and unions with a disjoint singleton subtype:

The empty subtype and improper subtype are given by

AtoDecidSub(λx:A.false)im AtoDecidSub(λx:A.true)\emptyset_A \coloneqq \mathrm{toDecidSub}(\lambda x:A.\mathrm{false}) \qquad \im_A \coloneqq \mathrm{toDecidSub}(\lambda x:A.\mathrm{true})

Singleton subtypes correspond to boolean-valued functions for which there exists a unique x:Ax:A such that f(x)f(x) is true, and is given by

f:Abool!x:A.f(x)= booltrue\sum_{f:A \to \mathrm{bool}} \exists!x:A.f(x) =_\mathrm{bool} \mathrm{true}

Unions of decidable subtypes correspond to lambda abstraction of the disjunction of boolean-valued function evaluations

PQtoDecidSub(λx:A.toDecidSub 1(P)(x)toDecidSub 1(Q)(x))P \cup Q \coloneqq \mathrm{toDecidSub}(\lambda x:A.\mathrm{toDecidSub}^{-1}(P)(x) \vee \mathrm{toDecidSub}^{-1}(Q)(x))

and intersections of decidable subtypes correspond to lambda abstraction of the conjunction of boolean-valued function evaluations

PQtoDecidSub(λx:A.toDecidSub 1(P)(x)toDecidSub 1(Q)(x))P \cap Q \coloneqq \mathrm{toDecidSub}(\lambda x:A.\mathrm{toDecidSub}^{-1}(P)(x) \wedge \mathrm{toDecidSub}^{-1}(Q)(x))

Two decidable subtypes are disjoint if their intersection is the empty subtype.

See also

References

In Agda:

In Lean:

Last revised on February 11, 2024 at 18:22:14. See the history of this page for a list of all contributions to it.