Contents
Definition
In first order logic with equality
Uniqueness up to equality
In first order logic with equality, given a predicate on a type with equality, the uniqueness quantifier of , denoted , is defined in terms of the universal and existential quantifiers as
The intended interpretation is that is true iff is true for exactly one element of .
Uniqueness up to isomorphism
Sometimes, we want to use a weaker notion of equivalence than strict equality, such as isomorphism . The uniqueness up to isomorphism quantifier of , denoted , is defined in terms of the universal and existential quantifiers as
The intended interpretation is that is true iff is true for exactly one element of up to isomorphism.
Uniqueness up to isomorphism quantifiers are important in category theory, where the relevant notion of sameness is isomorphism rather than strict equality. It is also important in foundational set theories where the type of sets does not have equality, such as some presentations of SEAR and ETCS.
In dependent type theory
In dependent type theory, given a type and a type family , the uniqueness quantifier is a type defined as
which indicates that the dependent sum type is a contractible type, which is only the case for a family of type if every dependent type is a mere proposition and, for exactly one element up to identity, the type is inhabited.
Rules for uniqueness quantifiers
If the dependent type theory has identity types and dependent identity types, but does not have general dependent function types (such as in strongly predicative mathematics), one could directly form the uniqueness quantifier via its natural deduction rules:
Formation rules for uniqueness quantifier types:
Introduction rules for uniqueness quantifier types:
Elimination rules for uniqueness quantifier types:
Computation rules for uniqueness quantifier types:
Uniqueness rules for uniqueness quantifier types:
Usages
Bijections and equivalences
The uniqueness quantifier is used in the definition of a bijection in set theory and an equivalence in type theory, where one defines a function to be a bijection or equivalence if for all the there is a unique such that
In dependent type theory, this is the same as defining a family of elements to be an equivalence if it comes with a family of elements
The inverse of an equivalence is given by the family of elements , where is defined in the elimination rules for uniqueness quantifiers in dependent type theory.
Anafunctions
Similarly, uniqueness quantifications is used in the definition of an anafunction, where one defines a relation or correspondence to be an anafunction if for all there is a unique such that
Univalent universes
Uniqueness quantifiers are also used to define univalent universes. A Russell universe is a univalent universe if for all elements there is a unique such that :
Similarly, a Tarski universe is a univalent universe if for all elements there is a unique such that :
See also