# 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

Imports
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


## Idea

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.

## Definitions

### The predicate of being a singleton subtype

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

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)
where

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)
where

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 =
subtype-standard-singleton-subtype
pr2 inhabited-subtype-standard-singleton-subtype =
unit-trunc-Prop (pair x refl)


## Properties

### 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)
where

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)
where

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)
where

inclusion-is-singleton-subtype :
is-singleton-subtype P → P ⊆ Q
inclusion-is-singleton-subtype s =
backward-implication
( 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)
where

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)
where

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)
where

abstract
is-singleton-im-singleton-subtype :
is-singleton-subtype
( im-subtype f (subtype-standard-singleton-subtype X x))
is-singleton-im-singleton-subtype =
is-contr-equiv
( Σ (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 :
has-same-elements-subtype
( subtype-standard-singleton-subtype Y (f x))
( im-subtype f (subtype-standard-singleton-subtype X x))
compute-im-singleton-subtype =
has-same-elements-is-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)