nLab uniqueness quantifier

Contents

Definition

In first order logic with equality

Uniqueness up to equality

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

!x:T,P(x)x:T,P(x)y:T,P(y)(x=y). \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 !x:T,P(x)\exists!\, x\colon T, P(x) is true iff P(a)P(a) is true for exactly one element aa of TT.

Uniqueness up to isomorphism

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

! x:T,P(x)x:T,P(x)y:T,P(y)(xy). \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 ! x:T,P(x)\exists!_\cong\, x\colon T, P(x) is true iff P(a)P(a) is true for exactly one element aa of TT 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 TT and a type family x:TP(x)x:T \vdash P(x), the uniqueness quantifier is a type defined as

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

which indicates that the dependent sum type x:TP(x)\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:Tx:T up to identity, the type P(x)P(x) 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:

ΓAtypeΓ,x:AB(x)typeΓ!x:A.B(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \exists!x:A.B(x) \; \mathrm{type}}

Introduction rules for uniqueness quantifier types:

ΓAtypeΓ,x:AB(x)typeΓa:AΓb:B(a)Γ,x:A,y:B(x)τ A(x,y):a= AxΓ,x:A,y:B(x)τ B(x,y):b= B τ A(x,y)yΓw(a,b,τ A,τ B):!x:A.B(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a) \quad \Gamma, x:A, y:B(x) \vdash \tau_A(x, y):a =_A x \quad \Gamma, x:A, y:B(x) \vdash \tau_B(x, y):b =_B^{\tau_A(x, y)} y}{\Gamma \vdash w(a, b, \tau_A, \tau_B):\exists!x:A.B(x)}

Elimination rules for uniqueness quantifier types:

ΓAtypeΓ,x:AB(x)typeΓp:!x:A.B(x)Γϵ A(p):A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash p:\exists!x:A.B(x)}{\Gamma \vdash \epsilon_A(p):A}
ΓAtypeΓ,x:AB(x)typeΓp:!x:A.B(x)Γϵ B(p):B(ϵ A(p))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash p:\exists!x:A.B(x)}{\Gamma \vdash \epsilon_B(p):B(\epsilon_A(p))}
ΓAtypeΓ,x:AB(x)typeΓp:!x:A.B(x)Γ,x:A,y:B(x)c A(p,x,y):ϵ A(p)= Ax\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash p:\exists!x:A.B(x)}{\Gamma, x:A, y:B(x) \vdash c_A(p, x, y):\epsilon_A(p) =_A x}
ΓAtypeΓ,x:AB(x)typeΓp:!x:A.B(x)Γ,x:A,y:B(x)c B(p,x,y):ϵ B(p)= B c A(p,x,y)y\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash p:\exists!x:A.B(x)}{\Gamma, x:A, y:B(x) \vdash c_B(p, x, y):\epsilon_B(p) =_B^{c_A(p, x, y)} y}

Computation rules for uniqueness quantifier types:

ΓAtypeΓ,x:AB(x)typeΓa:AΓb:B(a)Γ,x:A,y:B(x)τ A(x,y):a= AxΓ,x:A,y:B(x)τ B(x,y):b= B τ A(x,y)yΓβ !x:A.B(x) ϵ A(a,b):ϵ A(w(a,b,τ A,τ B))= Aa\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a) \quad \Gamma, x:A, y:B(x) \vdash \tau_A(x, y):a =_A x \quad \Gamma, x:A, y:B(x) \vdash \tau_B(x, y):b =_B^{\tau_A(x, y)} y}{\Gamma \vdash \beta_{\exists!x:A.B(x)}^{\epsilon_A}(a, b):\epsilon_A(w(a, b, \tau_A, \tau_B)) =_A a}
ΓAtypeΓ,x:AB(x)typeΓa:AΓb:B(a)Γ,x:A,y:B(x)τ A(x,y):a= AxΓ,x:A,y:B(x)τ B(x,y):b= B τ A(x,y)yΓβ !x:A.B(x) ϵ B(a,b):ϵ B(w(a,b,τ A,τ B)))= B β !x:A.B(x) ϵ A(a,b)b\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a) \quad \Gamma, x:A, y:B(x) \vdash \tau_A(x, y):a =_A x \quad \Gamma, x:A, y:B(x) \vdash \tau_B(x, y):b =_B^{\tau_A(x, y)} y}{\Gamma \vdash \beta_{\exists!x:A.B(x)}^{\epsilon_B}(a, b):\epsilon_B(w(a, b, \tau_A, \tau_B))) =_B^{\beta_{\exists!x:A.B(x)}^{\epsilon_A}(a, b)} b}
ΓAtypeΓ,x:AB(x)typeΓa:AΓb:B(a)Γ,x:A,y:B(x)τ A(x,y):a= AxΓ,x:A,y:B(x)τ B(x,y):b= B τ A(x,y)yΓ,x:A,y:B(x)β !x:A.B(x) c A(a,b,x,y):c A(w(a,b,τ A,τ B),x,y)= ()= Ax β !x:A.B(x) ϵ Aτ A(x,y)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a) \quad \Gamma, x:A, y:B(x) \vdash \tau_A(x, y):a =_A x \quad \Gamma, x:A, y:B(x) \vdash \tau_B(x, y):b =_B^{\tau_A(x, y)} y}{\Gamma, x:A, y:B(x) \vdash \beta_{\exists!x:A.B(x)}^{c_A}(a, b, x, y):c_A(w(a, b, \tau_A, \tau_B), x, y) =_{(-) =_A x}^{\beta_{\exists!x:A.B(x)}^{\epsilon_A}} \tau_A(x, y)}
ΓAtypeΓ,x:AB(x)typeΓa:AΓb:B(a)Γ,x:A,y:B(x)τ A(x,y):a= AxΓ,x:A,y:B(x)τ B(x,y):b= B τ A(x,y)yΓ,x:A,y:B(x)β !x:A.B(x) c B(a,b,x,y):c B(w(a,b,τ A,τ B),x,y)= ()= B β !x:A.B(x) c A(a,b,x,y)y β !x:A.B(x) ϵ Bτ B(x,y)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a) \quad \Gamma, x:A, y:B(x) \vdash \tau_A(x, y):a =_A x \quad \Gamma, x:A, y:B(x) \vdash \tau_B(x, y):b =_B^{\tau_A(x, y)} y}{\Gamma, x:A, y:B(x) \vdash \beta_{\exists!x:A.B(x)}^{c_B}(a, b, x, y):c_B(w(a, b, \tau_A, \tau_B), x, y) =_{(-) =_B^{\beta_{\exists!x:A.B(x)}^{c_A}(a, b, x, y)} y}^{\beta_{\exists!x:A.B(x)}^{\epsilon_B}} \tau_B(x, y)}

Uniqueness rules for uniqueness quantifier types:

ΓAtypeΓ,x:AB(x)typeΓp:!x:A.B(x)Γη !x:A.B(x)(p):w(ϵ A(p),ϵ B(p),c A(p),c B(p))= !x:A.B(x)p\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash p:\exists!x:A.B(x)}{\Gamma \vdash \eta_{\exists!x:A.B(x)}(p):w(\epsilon_A(p), \epsilon_B(p), c_A(p), c_B(p)) =_{\exists!x:A.B(x)} p}

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

isEquiv(f)y:B.!x:A.f(x)= By\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:Af(x):Bx:A \vdash f(x):B to be an equivalence if it comes with a family of elements

y:Bϵ(f)(y):!x:A.f(x)= Byy: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ϵ A(ϵ(f)(y)):Ay:B \vdash \epsilon_A(\epsilon(f)(y)):A, where ϵ A\epsilon_A 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 x:A,y:BR(x,y)x:A, y:B \vdash R(x, y) to be an anafunction if for all x:Ax:A there is a unique y:By:B such that R(x,y)R(x, y)

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

Univalent universes

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

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

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

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

See also

Last revised on January 13, 2023 at 06:21:25. See the history of this page for a list of all contributions to it.