Singleton subtypes

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Vojtěch Štěpančík.

Created on 2022-09-12.
Last modified on 2024-03-14.

module foundation.singleton-subtypes where
open import foundation.connected-components
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.images-subtypes
open import foundation.inhabited-subtypes
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.singleton-induction
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.propositions


A singleton subtype of a type X is a subtype P of X of which the underlying type is contractible. In informal writing, we will write {x} for the standard singleton subtype of a set X containing the element x.

Note: If a subtype containing an element x is a singleton subtype, then it is also the least subtype containing x. However, the reverse implication does not necessarily hold. The condition that a subtype is the least subtype containing an element x is only equivalent to the condition that its underlying type is 0-connected, which is a weaker condition than being a singleton subtype.


The predicate of being a singleton subtype

module _
  {l1 l2 : Level} {X : UU l1} (P : subtype l2 X)

  is-singleton-subtype-Prop : Prop (l1  l2)
  is-singleton-subtype-Prop = is-contr-Prop (type-subtype P)

  is-singleton-subtype : UU (l1  l2)
  is-singleton-subtype = type-Prop is-singleton-subtype-Prop

  is-prop-is-singleton-subtype :
    is-prop is-singleton-subtype
  is-prop-is-singleton-subtype = is-prop-type-Prop is-singleton-subtype-Prop

The type of singleton subtypes

singleton-subtype :
  {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
singleton-subtype l2 X = type-subtype (is-singleton-subtype-Prop {l2 = l2} {X})

module _
  {l1 l2 : Level} {X : UU l1} (P : singleton-subtype l2 X)

  subtype-singleton-subtype : subtype l2 X
  subtype-singleton-subtype = pr1 P

  is-singleton-subtype-singleton-subtype :
    is-singleton-subtype subtype-singleton-subtype
  is-singleton-subtype-singleton-subtype = pr2 P

Standard singleton subtypes

module _
  {l : Level} (X : Set l) (x : type-Set X)

  subtype-standard-singleton-subtype : subtype l (type-Set X)
  subtype-standard-singleton-subtype y = Id-Prop X x y

  type-standard-singleton-subtype : UU l
  type-standard-singleton-subtype =
    type-subtype subtype-standard-singleton-subtype

  inclusion-standard-singleton-subtype :
    type-standard-singleton-subtype  type-Set X
  inclusion-standard-singleton-subtype =
    inclusion-subtype subtype-standard-singleton-subtype

  standard-singleton-subtype : singleton-subtype l (type-Set X)
  pr1 standard-singleton-subtype = subtype-standard-singleton-subtype
  pr2 standard-singleton-subtype = is-torsorial-Id x

  inhabited-subtype-standard-singleton-subtype :
    inhabited-subtype l (type-Set X)
  pr1 inhabited-subtype-standard-singleton-subtype =
  pr2 inhabited-subtype-standard-singleton-subtype =
    unit-trunc-Prop (pair x refl)


If a subtype is a singleton subtype containing x, then it is the least subtype containing x

module _
  {l1 l2 : Level} {X : UU l1} {x : X} (P : subtype l2 X) (p : is-in-subtype P x)

  is-least-subtype-containing-element-is-singleton-subtype :
    is-singleton-subtype P  is-least-subtype-containing-element x P
  pr1 (is-least-subtype-containing-element-is-singleton-subtype H Q) L = L x p
  pr2 (is-least-subtype-containing-element-is-singleton-subtype H Q) q y r =
    ind-singleton (x , p) H (is-in-subtype Q  pr1) q (y , r)

If the identity type y ↦ x = y is a subtype, then a subtype containing x is a singleton subtype if and only if it is the least subtype containing x

Proof: We already showed the forward direction. For the converse, suppose that the identity type y ↦ x = y is a subtype and that P is the least subtype containing the element x. To show that Σ X P is contractible, we use the element (x , p) as the center of contraction, where p : P x is assumed. Then it remains to construct the contraction. Recall that for any element (y , q) : Σ X P we have a function

  eq-type-subtype P : (x = y) → ((x , p) = (y , q)).

Therefore it suffices to show that x = y. This is a proposition. By the assumption that P is the least subtype containing x we have a function P u → x = u for all u, so x = y follows.

module _
  {l1 l2 : Level} {X : UU l1} {x : X} (P : subtype l2 X) (p : is-in-subtype P x)

  is-singleton-subtype-is-least-subtype-containing-element :
    (H : (y : X)  is-prop (x  y)) 
    is-least-subtype-containing-element x P  is-singleton-subtype P
  pr1 (is-singleton-subtype-is-least-subtype-containing-element H L) = (x , p)
  pr2 (is-singleton-subtype-is-least-subtype-containing-element H L) (y , q) =
    eq-type-subtype P (backward-implication (L  y  x  y , H y)) refl y q)

is-singleton-subtype-is-least-subtype-containing-element-Set :
  {l1 l2 : Level} (X : Set l1) {x : type-Set X} (P : subtype l2 (type-Set X))
  (p : is-in-subtype P x) 
  is-least-subtype-containing-element x P  is-singleton-subtype P
is-singleton-subtype-is-least-subtype-containing-element-Set X P p =
  is-singleton-subtype-is-least-subtype-containing-element P p
    ( is-set-type-Set X _)

Any two singleton subtypes containing a given element x have the same elements

module _
  {l1 l2 l3 : Level} {X : UU l1} {x : X} (P : subtype l2 X) (Q : subtype l3 X)
  (p : is-in-subtype P x) (q : is-in-subtype Q x)

  inclusion-is-singleton-subtype :
    is-singleton-subtype P  P  Q
  inclusion-is-singleton-subtype s =
      ( is-least-subtype-containing-element-is-singleton-subtype P p s Q)
      ( q)

module _
  {l1 l2 l3 : Level} {X : UU l1} {x : X} (P : subtype l2 X) (Q : subtype l3 X)
  (p : is-in-subtype P x) (q : is-in-subtype Q x)

  has-same-elements-is-singleton-subtype :
    is-singleton-subtype P  is-singleton-subtype Q 
    has-same-elements-subtype P Q
  pr1 (has-same-elements-is-singleton-subtype s t y) =
    inclusion-is-singleton-subtype P Q p q s y
  pr2 (has-same-elements-is-singleton-subtype s t y) =
    inclusion-is-singleton-subtype Q P q p t y

The standard singleton subtype {x} of a set is the least subtype containing x

module _
  {l1 : Level} (X : Set l1) (x : type-Set X)

  is-least-subtype-containing-element-Set :
    is-least-subtype-containing-element x
      ( subtype-standard-singleton-subtype X x)
  pr1 (is-least-subtype-containing-element-Set A) H = H x refl
  pr2 (is-least-subtype-containing-element-Set A) H .x refl = H

The image of the standard singleton subtype {x} under a map f : X → Y is the standard singleton subtype {f(x)}

Proof: Our goal is to show that the type

  Σ Y (λ y → ∥ Σ (Σ X (λ u → x = u)) (λ v → f (inclusion v) = y) ∥ )

Since the type Σ X (λ u → x = u) is contractible, the above type is equivalent to

  Σ Y (λ y → ∥ f x = y ∥ )

Note that the identity type f x = y of a set is a proposition, so this type is equivalent to the type Σ Y (λ y → f x = y), which is of course contractible.

module _
  {l1 l2 : Level} (X : Set l1) (Y : Set l2) (f : hom-Set X Y) (x : type-Set X)

    is-singleton-im-singleton-subtype :
        ( im-subtype f (subtype-standard-singleton-subtype X x))
    is-singleton-im-singleton-subtype =
        ( Σ (type-Set Y)  y  f x  y))
        ( equiv-tot
            ( λ y 
              ( inv-equiv (equiv-unit-trunc-Prop (Id-Prop Y (f x) y))) ∘e
              ( equiv-trunc-Prop
                ( left-unit-law-Σ-is-contr (is-torsorial-Id x) (x , refl)))))
        ( is-torsorial-Id (f x))

  compute-im-singleton-subtype :
      ( subtype-standard-singleton-subtype Y (f x))
      ( im-subtype f (subtype-standard-singleton-subtype X x))
  compute-im-singleton-subtype =
      ( subtype-standard-singleton-subtype Y (f x))
      ( im-subtype f (subtype-standard-singleton-subtype X x))
      ( refl)
      ( unit-trunc-Prop ((x , refl) , refl))
      ( is-torsorial-Id (f x))
      ( is-singleton-im-singleton-subtype)

See also

Recent changes