In first order logic with equality, given a predicate $P$ on a type $T$ with equality, the **uniqueness quantifier** of $P$, denoted $\exists!\, x\colon T, P(x)$, is defined in terms of the universal and existential quantifiers as

$\exists!\, x\colon T, P(x) \;\equiv\; \exists\, x\colon T, P(x) \wedge \forall\, y\colon T, P(y) \Rightarrow (x = y) .$

The intended interpretation is that $\exists!\, x\colon T, P(x)$ is true iff $P(a)$ is true for *exactly* one element $a$ of $T$.

Sometimes, we want to use a weaker notion of equivalence than strict equality, such as isomorphism $x \cong y$. The **uniqueness up to isomorphism quantifier** of $P$, denoted $\exists!_\cong\, x\colon T, P(x)$, is defined in terms of the universal and existential quantifiers as

$\exists!_\cong\, x\colon T, P(x) \;\equiv\; \exists\, x\colon T, P(x) \wedge \forall\, y\colon T, P(y) \Rightarrow (x \cong y).$

The intended interpretation is that $\exists!_\cong\, x\colon T, P(x)$ is true iff $P(a)$ is true for *exactly* one element $a$ of $T$ 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, given a type $T$ and a type family $x:T \vdash P(x)$, the uniqueness quantifier is a type defined as

$\exists!\, x\colon T. P(x) \coloneqq \mathrm{isContr}\left(\sum_{x:T} P(x)\right)$

which indicates that the dependent sum type $\sum_{x:T} P(x)$ 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 $x:T$ up to identity, the type $P(x)$ is inhabited.

In dependent type theory, given two mere propositions $P$ and $Q$, by descent or large elimination? of the boolean domain, one can construct a boolean-indexed family of propositions

$x:\mathrm{bool} \vdash \mathrm{rec}_\mathrm{bool}^{P, Q}(x)$

$\beta_\mathrm{bool}^{P, Q}(0):\mathrm{rec}_\mathrm{bool}^{P, Q}(0) \simeq P \quad \beta_\mathrm{bool}^{P, Q}(1):\mathrm{rec}_\mathrm{bool}^{P, Q}(1) \simeq Q$

in the case for descent for booleans, or with judgmental equality of types

$\mathrm{rec}_\mathrm{bool}^{P, Q}(0) \equiv P \quad \mathrm{rec}_\mathrm{bool}^{P, Q}(1) \equiv P$

in the case for large elimination for booleans.

The uniqueness quantifier of the above family of propositions is the exclusive disjunction of $P$ and $Q$:

$P \underline{\vee} Q \coloneqq \exists!x:\mathbb{2}.\mathrm{rec}_\mathrm{bool}^{P, Q}(x)$

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 $f:A \to B$ to be a bijection or equivalence if for all $y:B$ the there is a unique $x:A$ such that $f(x) =_B y$

$\mathrm{isEquiv}(f) \coloneqq \forall y:B.\exists! x:A.f(x) =_B y$

In dependent type theory, this is the same as defining a family of elements $x:A \vdash f(x):B$ to be an equivalence if it comes with a family of elements

$y:B \vdash \epsilon(f)(y):\exists! x:A.f(x) =_B y$

The inverse of an equivalence is given by the family of elements $y:B \vdash \epsilon_A(\epsilon(f)(y)):A$, where $\epsilon_A$ is defined in the elimination rules for uniqueness quantifiers in dependent type theory.

Similarly, uniqueness quantifications is used in the definition of an anafunction, where one defines a relation or correspondence $x:A, y:B \vdash R(x, y)$ to be an anafunction if for all $x:A$ there is a unique $y:B$ such that $R(x, y)$

$\mathrm{isAnafunc}(R) \coloneqq \forall x:A.\exists! y:B.R(x, y)$

Uniqueness quantifiers are also used to define univalent universes. A Russell universe $U$ is a univalent universe if for all elements $A:U$ there is a unique $B:U$ such that $A \simeq B$:

$\mathrm{isUnivalent}(U) \coloneqq \forall A:U.\exists! B:U.A \simeq B$

Similarly, a Tarski universe $(U, T)$ is a univalent universe if for all elements $A:U$ there is a unique $B:U$ such that $T(A) \simeq T(B)$:

$\mathrm{isUnivalent}(U, T) \coloneqq \forall A:U.\exists! B:U.T(A) \simeq T(B)$

Last revised on September 6, 2024 at 19:10:14. See the history of this page for a list of all contributions to it.