Uniqueness quantification

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.
Last modified 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

See also

Recent changes