(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In dependent type theory, the type of finite types is the type universe 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.
In dependent type theory, given a type , there are many different ways of defining the mere proposition which indicates that is a finite type.
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 , as they uses directly rather than a particular definition.
The type of (all) finite types in a dependent type theory could be defined in many different ways:
as a positive higher inductive type representing the Rezk completion of the strict category of standard finite types, whose objects is the set of natural numbers.
as a homotopy-terminal univalent type family of finite types, suitably defined.
as a type universe, with inference rules that mimic that of the negative dependent sum type or respectively, but for all types, not just the -small types.
In addition, in dependent type theory defined using a universe hierarchy instead of a separate type judgment, a universe having the type of all finite types as defined above is equivalent to a local resizing axiom which says that the locally -small type is (essentially) -small.
The natural numbers type has a strict category structure where the objects are natural numbers and the hom-sets are function types between the standard finite sets with and 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 from the definition of set truncation, so the Tarski universe type family is defined by the standard finite type of the cardinality of the finite type
This Tarski universe is a univalent Tarski universe of finite types by definition of Rezk completion.
A univalent family of finite types consists of a type and a type family such that
is a finite type for all ,
the transport function
is an equivalence of types for all and
A morphism of univalent families of finite types between univalent families of finite types and consists of a function and a family of functions .
The type of (all) finite types is the homotopy-terminal univalent family of finite types: given any other univalent family of finite types , there exists a unique function and a unique family of functions .
The type of (all) finite types 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
a witness that 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.
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:
Introduction rules for the type of all finite types:
Elimination rules for the type of all finite types:
Computation rules for the type of all finite types:
Uniqueness rules for the type of all finite types:
Extensionality principle of the type of all finite types:
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:
Introduction rules for the type of all finite types:
Elimination rules for the type of all finite types:
Computation rules for the type of all finite types:
Uniqueness rules for the type of all finite types:
Extensionality principle of the type of all finite types:
Unlike the case for the type of all types , the type of all finite types doesn’t run into Girard's paradox, because neither nor its set truncation is itself a finite type, and so isn’t essentially -small.
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.
The natural numbers type is equivalent to the set truncation of the type of finite types:
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 could be defined as a resizing axiom similar to propositional resizing, since set truncations could be defined from the type of propositions in :
The arithmetic operations and order relations on the natural numbers type can be defined by induction on set truncation:
For all finite types and and finite families , we have
The categorical semantics of the type of finite types is the finite object classifier, the object classifier which classifies finite objects of a category.
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.