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 set theory, there are 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

Let (Ω,El Ω)(\Omega, \mathrm{El}_\Omega) denote the type of all propositions and its type reflector type family. Let TT be a type.

Definition

The power set of a type AA is defined as the function type from AA to the 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 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 ABEl Ω(B(x))x \in_A B \coloneqq \mathrm{El}_\Omega(B(x))

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

In the inference rules for the type of all propositions, one has an operation () Ω(-)_\Omega which takes a proposition PP and turns it into an element of the type of all propositions P Ω:ΩP_\Omega:\Omega.

material subtypepredicatestructural subtype
B:𝒫(A)B:\mathcal{P}(A)x:Ax ABEl Ω(B(x))x:A \vdash x \in_A B \coloneqq \mathrm{El}_\Omega(B(x)) x:Ax AB\sum_{x:A} x \in_A B
λx:A.(B(x)) Ω:𝒫(A)\lambda x:A.(B(x))_\Omega:\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)\lambda x:A.\left(\sum_{y:B} i(y) =_A x\right)_\Omega:\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 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) \times (x \in_A C))_\Omega

for all x:Ax:A.

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:Ix AB(i)) Ω\left(\bigcap_{i:I} B(i)\right)(x) \coloneqq \left(\prod_{i:I} x \in_A B(i)\right)_\Omega

for all x:Ax:A.

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 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))_\Omega

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))_\Omega

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.

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 intersection of RR and SS is 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, 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 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))

See also

Last revised on May 25, 2023 at 14:55:25. See the history of this page for a list of all contributions to it.