Sets

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-02-07.
Last modified on 2024-08-21.

module foundation-core.sets where
Imports 
open import foundation.dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.truncated-types
open import foundation-core.truncation-levels

Idea

A type is a set if its identity types are propositions.

Definition

is-set : {l : Level} → UU l → UU l
is-set A = (x y : A) → is-prop (x ＝ y)

Set : (l : Level) → UU (lsuc l)
Set l = Σ (UU l) is-set

module _
  {l : Level} (X : Set l)
  where

  type-Set : UU l
  type-Set = pr1 X

  abstract
    is-set-type-Set : is-set type-Set
    is-set-type-Set = pr2 X

  Id-Prop : (x y : type-Set) → Prop l
  Id-Prop x y = (x ＝ y , is-set-type-Set x y)

Properties

A type is a set if and only if it satisfies Streicher’s axiom K

instance-axiom-K : {l : Level} → UU l → UU l
instance-axiom-K A = (x : A) (p : x ＝ x) → refl ＝ p

axiom-K-Level : (l : Level) → UU (lsuc l)
axiom-K-Level l = (A : UU l) → instance-axiom-K A

axiom-K : UUω
axiom-K = {l : Level} → axiom-K-Level l

module _
  {l : Level} {A : UU l}
  where

  abstract
    is-set-axiom-K' :
      instance-axiom-K A → (x y : A) → all-elements-equal (x ＝ y)
    is-set-axiom-K' K x .x refl q with K x q
    ... | refl = refl

  abstract
    is-set-axiom-K : instance-axiom-K A → is-set A
    is-set-axiom-K H x y = is-prop-all-elements-equal (is-set-axiom-K' H x y)

  abstract
    axiom-K-is-set : is-set A → instance-axiom-K A
    axiom-K-is-set H x p =
      ( inv (contraction (is-proof-irrelevant-is-prop (H x x) refl) refl)) ∙
      ( contraction (is-proof-irrelevant-is-prop (H x x) refl) p)

A type is a set if and only if it satisfies uniqueness of identity proofs

A type A is said to satisfy uniqueness of identity proofs if for all elements x y : A all equality proofs x ＝ y are equal.

has-uip : {l : Level} → UU l → UU l
has-uip A = (x y : A) → all-elements-equal (x ＝ y)

module _
  {l : Level} {A : UU l}
  where

  is-set-has-uip : is-set A → has-uip A
  is-set-has-uip is-set-A x y = eq-is-prop' (is-set-A x y)

  has-uip-is-set : has-uip A → is-set A
  has-uip-is-set uip-A x y = is-prop-all-elements-equal (uip-A x y)

If a reflexive binary relation maps into the identity type of A, then A is a set

module _
  {l1 l2 : Level} {A : UU l1} (R : A → A → UU l2)
  (p : (x y : A) → is-prop (R x y)) (ρ : (x : A) → R x x)
  (i : (x y : A) → R x y → x ＝ y)
  where

  abstract
    is-equiv-prop-in-id : (x y : A) → is-equiv (i x y)
    is-equiv-prop-in-id x =
      fundamental-theorem-id-retraction x (i x)
        ( λ y →
          pair
            ( ind-Id x (λ z p → R x z) (ρ x) y)
            ( λ r → eq-is-prop (p x y)))

  abstract
    is-set-prop-in-id : is-set A
    is-set-prop-in-id x y = is-prop-is-equiv' (is-equiv-prop-in-id x y) (p x y)

Any proposition is a set

abstract
  is-set-is-prop :
    {l : Level} {P : UU l} → is-prop P → is-set P
  is-set-is-prop = is-trunc-succ-is-trunc neg-one-𝕋

set-Prop :
  {l : Level} → Prop l → Set l
set-Prop P = truncated-type-succ-Truncated-Type neg-one-𝕋 P

Sets are closed under equivalences

abstract
  is-set-is-equiv :
    {l1 l2 : Level} {A : UU l1} (B : UU l2) (f : A → B) → is-equiv f →
    is-set B → is-set A
  is-set-is-equiv = is-trunc-is-equiv zero-𝕋

abstract
  is-set-equiv :
    {l1 l2 : Level} {A : UU l1} (B : UU l2) (e : A ≃ B) →
    is-set B → is-set A
  is-set-equiv = is-trunc-equiv zero-𝕋

abstract
  is-set-is-equiv' :
    {l1 l2 : Level} (A : UU l1) {B : UU l2} (f : A → B) → is-equiv f →
    is-set A → is-set B
  is-set-is-equiv' = is-trunc-is-equiv' zero-𝕋

abstract
  is-set-equiv' :
    {l1 l2 : Level} (A : UU l1) {B : UU l2} (e : A ≃ B) →
    is-set A → is-set B
  is-set-equiv' = is-trunc-equiv' zero-𝕋

abstract
  is-set-equiv-is-set :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    is-set A → is-set B → is-set (A ≃ B)
  is-set-equiv-is-set = is-trunc-equiv-is-trunc zero-𝕋

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

  equiv-Set : UU (l1 ⊔ l2)
  equiv-Set = type-Set A ≃ type-Set B

  equiv-set-Set : Set (l1 ⊔ l2)
  pr1 equiv-set-Set = equiv-Set
  pr2 equiv-set-Set =
    is-set-equiv-is-set (is-set-type-Set A) (is-set-type-Set B)

If a type injects into a set, then it is a set

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

  abstract
    is-set-is-injective :
      {f : A → B} → is-set B → is-injective f → is-set A
    is-set-is-injective {f} H I =
      is-set-prop-in-id
        ( λ x y → f x ＝ f y)
        ( λ x y → H (f x) (f y))
        ( λ x → refl)
        ( λ x y → I)

Recent changes