# Uniqueness quantification

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.

module foundation.uniqueness-quantification where

Imports
open import foundation.dependent-pair-types
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.propositions


## Idea

Given a predicate P : A → Prop we say there uniquely exists an x : A satisfying P, if the subtype Σ (x : A), (P x) is contractible.

More generally, given a structure B : A → 𝒰 we say there uniquely exists an x : A and a y : B x, if the total type Σ (x : A), (B x) is contractible.

Note that the unique existence of structure is defined in the exact same way as the concept of torsorial type families. Whether to use the concept of unique existence of a structure or the concept of torsorial type family is dependent on the context. Torsoriality is used often to emphasize the relation of the type family to the identity type, whereas uniqueness of structure is used to emphasize the uniqueness of elements equipped with further structure. For example, we tend to use unique existence in combination with universal properties, in order to conclude that a certain map equipped with some homotopies exists uniquely.

As a special case of uniqueness quantification, we recover exclusive disjunction when the indexing type is a 2-element type. Concretely, we have the equivalence

  ∃! (t : bool), (P t) ≐ is-contr (Σ (t : bool), (P t))
≃ is-contr ((P false) + (P true))
≐ P false ⊻ P true.


## Definitions

### Unique existence of structure

module _
{l1 l2 : Level} (A : UU l1) (B : A → UU l2)
where

uniquely-exists-structure-Prop : Prop (l1 ⊔ l2)
uniquely-exists-structure-Prop = is-torsorial-Prop B

uniquely-exists-structure : UU (l1 ⊔ l2)
uniquely-exists-structure = type-Prop uniquely-exists-structure-Prop

is-prop-uniquely-exists-structure : is-prop uniquely-exists-structure
is-prop-uniquely-exists-structure =
is-prop-type-Prop uniquely-exists-structure-Prop


### Unique existence in a subtype

module _
{l1 l2 : Level} (A : UU l1) (P : A → Prop l2)
where

uniquely-exists-Prop : Prop (l1 ⊔ l2)
uniquely-exists-Prop = uniquely-exists-structure-Prop A (type-Prop ∘ P)

uniquely-exists : UU (l1 ⊔ l2)
uniquely-exists = type-Prop uniquely-exists-Prop

is-prop-uniquely-exists : is-prop uniquely-exists
is-prop-uniquely-exists = is-prop-type-Prop uniquely-exists-Prop

∃! : Prop (l1 ⊔ l2)
∃! = uniquely-exists-Prop


### Components of unique existence

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
where

pair-uniquely-exists : uniquely-exists-structure A B → Σ A B
pair-uniquely-exists = center

pr1-uniquely-exists : uniquely-exists-structure A B → A
pr1-uniquely-exists = pr1 ∘ pair-uniquely-exists

pr2-uniquely-exists :
(p : uniquely-exists-structure A B) → B (pr1-uniquely-exists p)
pr2-uniquely-exists = pr2 ∘ pair-uniquely-exists

contraction-uniquely-exists :
(p : uniquely-exists-structure A B) →
(q : Σ A B) → pair-uniquely-exists p ＝ q
contraction-uniquely-exists = contraction