nLab type of finite types

Context

Universes

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 dependent type theory, the type of finite types is the type universe FinType\mathrm{FinType} which contains the finite types of the type theory, in the sense of finite set in set theory. The type of finite types is important in the field of combinatorics, as well as for defining mathematical structures like finite-dimensional vector spaces.

Definition

In dependent type theory, given a type AA, there are many different ways of defining the mere proposition isFinite(A)\mathrm{isFinite}(A) which indicates that AA is a finite type.

isFinite(A)n:.AFin(n)\mathrm{isFinite}(A) \equiv \exists n:\mathbb{N}.A \simeq \mathrm{Fin}(n)
  • Given a type of propositions Prop\mathrm{Prop}, a type AA is finite if for all subtypes S:(AProp)PropS:(A \to \mathrm{Prop}) \to \mathrm{Prop} of the power set of AA, if the empty subtype λx:A.\lambda x:A.\bot is in SS, and for all subtypes P:APropP:A \to \mathrm{Prop} and Q:APropQ:A \to \mathrm{Prop} of AA such that PP being in SS, QQ being a singleton subtype, and PP and QQ being disjoint together imply that the union PQP \cup Q is in SS, then the improper subtype λx:A.\lambda x:A.\top is in SS.
isFinite(A) S:(AProp)Prop(((λx:A.)S)× P:AProp Q:AProp(PS) ×(!x:A.xQ)×(PQ= APropλx:A.)(PQS))((λx:A.)S) \mathrm{isFinite}(A) \equiv \begin{array}{c} \prod_{S:(A \to \mathrm{Prop}) \to \mathrm{Prop}} (((\lambda x:A.\bot) \in S) \times \prod_{P:A \to \mathrm{Prop}} \prod_{Q:A \to \mathrm{Prop}} (P \in S) \\ \times (\exists!x:A.x \in Q) \times (P \cap Q =_{A \to \mathrm{Prop}} \lambda x:A.\bot) \to (P \cup Q \in S)) \to ((\lambda x:A.\top) \in S) \end{array}

The membership relation and the subtype operations used above are defined in the nLab article on subtypes.

The definitions of the various different types of finite types are agnostic regarding the definition of isFinite\mathrm{isFinite}, as they uses isFinite\mathrm{isFinite} directly rather than a particular definition.

The type of (all) finite types FinType\mathrm{FinType} in a dependent type theory could be defined in many different ways:

In addition, in dependent type theory defined using a universe hierarchy instead of a separate type judgment, a universe U iU_i having the type of all finite types as defined above is equivalent to a local resizing axiom which says that the locally U i U_i -small type P:U iisFinite(P)\sum_{P:U_i} \mathrm{isFinite}(P) is (essentially) U i U_i -small.

As Rezk completion of a strict category

The natural numbers type has a strict category structure where the objects are natural numbers and the hom-sets hom(m,n)\mathrm{hom}(m, n) are function types Fin(m)Fin(n)\mathrm{Fin}(m) \to \mathrm{Fin}(n) between the standard finite sets with mm and nn elements respectively. This strict category is not a univalent category. The type of (all) finite types is defined as the Rezk completion of the above strict category, which is a higher inductive type.

The set truncation of this univalent category results in the natural numbers again, with cardinality function λX.|X|:FinType\lambda X.\vert X \vert:\mathrm{FinType} \to \mathbb{N} from the definition of set truncation, so the Tarski universe type family X:FinTypeEl(X)X:\mathrm{FinType} \vdash \mathrm{El}(X) is defined by the standard finite type of the cardinality of the finite type

El(X)Fin(|X|)\mathrm{El}(X) \coloneqq \mathrm{Fin}(\vert X \vert)

This Tarski universe is a univalent Tarski universe of finite types by definition of Rezk completion.

As a homotopy-terminal type

A univalent family of finite types consists of a type AA and a type family (B(x)) x:A(B(x))_{x:A} such that

  • B(x)B(x) is a finite type for all x:Ax:A,

  • the transport function

    tr B(x,y):x= Ay(B(x)B(y))\mathrm{tr}^B(x, y):x =_A y \to (B(x) \simeq B(y))

    is an equivalence of types for all x:Ax:A and y:Ay:A

A morphism of univalent families of finite types between univalent families of finite types (A,B)(A, B) and (A,B)(A', B') consists of a function f A:AAf_A:A \to A' and a family of functions f B(x):B(x)B(f A(x))f_B(x):B(x) \to B'(f_A(x)).

The type of (all) finite types (FinType,El)(\mathrm{FinType}, \mathrm{El}) is the homotopy-terminal univalent family of finite types: given any other univalent family of finite types (A,B)(A, B), there exists a unique function u A:AFinTypeu_A:A \to \mathrm{FinType} and a unique family of functions u B(x):B(x)El(u A(x))u_B(x):B(x) \to \mathrm{El}(u_A(x)).

As a type universe

The type of (all) finite types FinType\mathrm{FinType} is a type universe of finite types. It behaves as a record type where one of the fields is a type, consisting of

  • a type AtypeA \; \mathrm{type}

  • a witness p:isFinite(A)p:\mathrm{isFinite}(A) that AA is a finite type.

Similar to other type universes and record types with type fields, the type of all finite types can be presented a la Tarski or a la Russell.

A la Tarski

The type of all finite types a la Tarski is given by the following natural deduction inference rules:

Formation rules for the type of all finite types:

ΓctxΓFinTypetype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{FinType} \; \mathrm{type}}

Introduction rules for the type of all finite types:

ΓAtypeΓtoElem A:isFinite(A)FinType\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toElem}_A:\mathrm{isFinite}(A) \to \mathrm{FinType}}

Elimination rules for the type of all finite types:

ΓA:FinTypeΓEl(A)typeΓA:FinTypeΓfinWitn(A):isFinite(El(A))\frac{\Gamma \vdash A:\mathrm{FinType}}{\Gamma \vdash \mathrm{El}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{FinType}}{\Gamma \vdash \mathrm{finWitn}(A):\mathrm{isFinite}(\mathrm{El}(A))}

Computation rules for the type of all finite types:

ΓAtypeΓp:isFinite(A)ΓEl(toElem A(p))Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isFinite}(A)}{\Gamma \vdash \mathrm{El}(\mathrm{toElem}_A(p)) \equiv A \; \mathrm{type}}
ΓAtypeΓp:isFinite(A)ΓfinWitn(toElem A(p))p:isFinite(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isFinite}(A)}{\Gamma \vdash \mathrm{finWitn}(\mathrm{toElem}_A(p)) \equiv p:\mathrm{isFinite}(A)}

Uniqueness rules for the type of all finite types:

ΓA:FinTypeΓtoElem El(A)(finWitn(A))A:FinType\frac{\Gamma \vdash A:\mathrm{FinType}}{\Gamma \vdash \mathrm{toElem}_{\mathrm{El}(A)}(\mathrm{finWitn}(A)) \equiv A:\mathrm{FinType}}

Extensionality principle of the type of all finite types:

ΓA:FinTypeΓB:FinTypeΓext FinType(A,B):isEquiv(transport El(A,B))\frac{\Gamma \vdash A:\mathrm{FinType} \quad \Gamma \vdash B:\mathrm{FinType}} {\Gamma \vdash \mathrm{ext}_\mathrm{FinType}(A, B):\mathrm{isEquiv}(\mathrm{transport}^\mathrm{El}(A, B))}

A la Russell

The type of all propositions a la Russell is given by the following natural deduction inference rules:

Formation rules for the type of all finite types:

ΓctxΓFinTypetype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{FinType} \; \mathrm{type}}

Introduction rules for the type of all finite types:

ΓAtypeΓtoElem A:isFinite(A)FinType\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toElem}_A:\mathrm{isFinite}(A) \to \mathrm{FinType}}

Elimination rules for the type of all finite types:

ΓA:FinTypeΓAtypeΓA:FinTypeΓfinWitn(A):isFinite(A)\frac{\Gamma \vdash A:\mathrm{FinType}}{\Gamma \vdash A \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{FinType}}{\Gamma \vdash \mathrm{finWitn}(A):\mathrm{isFinite}(A)}

Computation rules for the type of all finite types:

ΓAtypeΓp:isFinite(A)ΓtoElem A(p)Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isFinite}(A)}{\Gamma \vdash \mathrm{toElem}_A(p) \equiv A \; \mathrm{type}}
ΓAtypeΓp:isFinite(A)ΓfinWitn(toElem A(p))p:isFinite(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isFinite}(A)}{\Gamma \vdash \mathrm{finWitn}(\mathrm{toElem}_A(p)) \equiv p:\mathrm{isFinite}(A)}

Uniqueness rules for the type of all finite types:

ΓA:FinTypeΓtoElem A(finWitn(A))A:FinType\frac{\Gamma \vdash A:\mathrm{FinType}}{\Gamma \vdash \mathrm{toElem}_{A}(\mathrm{finWitn}(A)) \equiv A:\mathrm{FinType}}

Extensionality principle of the type of all finite types:

ΓA:FinTypeΓB:FinTypeΓext FinType(A,B):isEquiv(idToEquiv(A,B))\frac{\Gamma \vdash A:\mathrm{FinType} \quad \Gamma \vdash B:\mathrm{FinType}} {\Gamma \vdash \mathrm{ext}_\mathrm{FinType}(A, B):\mathrm{isEquiv}(\mathrm{idToEquiv}(A, B))}

Properties

Unlike the case for the type of all types Type\mathrm{Type}, the type of all finite types FinType\mathrm{FinType} doesn’t run into Girard's paradox, because neither FinType\mathrm{FinType} nor its set truncation is itself a finite type, and so isn’t essentially FinType\mathrm{FinType}-small.

Closure under type formers

The type of finite types is closed under the empty type, the unit type, function types, dependent product types, product types, dependent sum types, and sum types.

Relation to the natural numbers type

The natural numbers type is equivalent to the set truncation of the type of finite types:

[FinType] 0\mathbb{N} \simeq [\mathrm{FinType}]_0

This is the type theoretic analogue of the decategorification of the permutation category resulting in the set of natural numbers.

This also means that the axiom of infinity for a type universe UU could be defined as a resizing axiom similar to propositional resizing, since set truncations could be defined from Prop U\mathrm{Prop}_U the type of propositions in UU:

axinf U: :U[ A:UisFinite(A)] 0\mathrm{axinf}_U:\sum_{\mathbb{N}:U} \mathbb{N} \simeq \left[\sum_{A:U} \mathrm{isFinite}(A)\right]_0
axinf U: :UT()[ A:UisFinite(T(A))] 0\mathrm{axinf}_U:\sum_{\mathbb{N}:U} T(\mathbb{N}) \simeq \left[\sum_{A:U} \mathrm{isFinite}(T(A))\right]_0

The arithmetic operations and order relations on the natural numbers type can be defined by induction on set truncation:

For all finite types A:FinTypeA:\mathrm{FinType} and B:FinTypeB:\mathrm{FinType} and finite families C:AFinTypeC:A \to \mathrm{FinType}, we have

0= [] 01= [𝟙] 00 =_\mathbb{N} [\emptyset]_0 \quad 1 =_\mathbb{N} [\mathbb{1}]_0
[A] 0+[B] 0= [A+B] 0[A]_0 + [B]_0 =_\mathbb{N} [A + B]_0
x=1 [A] 0[C] 0(x)= [ x:AC(x)] 0\sum_{x = 1}^{[A]_0} [C]_0(x) =_\mathbb{N} \left[\sum_{x:A} C(x)\right]_0
[A] 0[B] 0= [A×B] 0[A]_0 \cdot [B]_0 =_\mathbb{N} [A \times B]_0
x=1 [A] 0[C] 0(x)= [ x:AC(x)] 0\prod_{x = 1}^{[A]_0} [C]_0(x) =_\mathbb{N} \left[\prod_{x:A} C(x)\right]_0
[B] 0 [A] 0= [AB] 0[B]_0^{[A]_0} =_\mathbb{N} [A \to B]_0
[A] 0= [B] 0[AB] (1)or[A= FinTypeB] (1)[A]_0 =_\mathbb{N} [B]_0 \coloneqq [A \simeq B]_{(-1)} \; \mathrm{or} \; [A =_\mathrm{FinType} B]_{(-1)}
[A] 0[B] 0[AB] (1)[A]_0 \leq [B]_0 \coloneqq [A \hookrightarrow B]_{(-1)}

Categorical semantics

The categorical semantics of the type of finite types is the finite object classifier, the object classifier which classifies finite objects of a category.

References

For the fact that binary sum types, finite dependent sum types, and binary product types of finite types are finite types, see section 16.3 of:

For the fact that function types between finite types are finite types, see Exercise 16.1 of the above reference. These imply that the type of finite types are closed under binary sum types, finite dependent sum types, binary product types, and function types.

Last revised on May 16, 2025 at 06:19:32. See the history of this page for a list of all contributions to it.