Sets

module foundation.sets where
Imports
open import foundation-core.sets public

open import foundation.contractible-types
open import foundation.subuniverses
open import foundation.truncated-types

open import foundation-core.1-types
open import foundation-core.cartesian-product-types
open import foundation-core.dependent-pair-types
open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.functions
open import foundation-core.identity-types
open import foundation-core.propositional-maps
open import foundation-core.propositions
open import foundation-core.truncation-levels
open import foundation-core.universe-levels

Properties

The type of all sets in a universe is a 1-type

is-1-type-Set : {l : Level}  is-1-type (Set l)
is-1-type-Set = is-trunc-Truncated-Type zero-𝕋

Set-1-Type : (l : Level)  1-Type (lsuc l)
pr1 (Set-1-Type l) = Set l
pr2 (Set-1-Type l) = is-1-type-Set

Any contractible type is a set

abstract
  is-set-is-contr :
    {l : Level} {A : UU l}  is-contr A  is-set A
  is-set-is-contr = is-trunc-is-contr zero-𝕋

Sets are closed under dependent pair types

abstract
  is-set-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    is-set A  ((x : A)  is-set (B x))  is-set (Σ A B)
  is-set-Σ = is-trunc-Σ {k = zero-𝕋}

Σ-Set :
  {l1 l2 : Level} (A : Set l1) (B : pr1 A  Set l2)  Set (l1  l2)
pr1 (Σ-Set A B) = Σ (type-Set A)  x  (type-Set (B x)))
pr2 (Σ-Set A B) = is-set-Σ (is-set-type-Set A)  x  is-set-type-Set (B x))

Sets are closed under cartesian product types

abstract
  is-set-prod :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} 
    is-set A  is-set B  is-set (A × B)
  is-set-prod = is-trunc-prod zero-𝕋

prod-Set :
  {l1 l2 : Level} (A : Set l1) (B : Set l2)  Set (l1  l2)
prod-Set A B = Σ-Set A  x  B)

Being a set is a property

abstract
  is-prop-is-set :
    {l : Level} (A : UU l)  is-prop (is-set A)
  is-prop-is-set = is-prop-is-trunc zero-𝕋

is-set-Prop : {l : Level}  UU l  Prop l
pr1 (is-set-Prop A) = is-set A
pr2 (is-set-Prop A) = is-prop-is-set A

The inclusion of sets into the universe is an embedding

emb-type-Set : (l : Level)  Set l  UU l
emb-type-Set l = emb-type-Truncated-Type l zero-𝕋

Products of families of sets are sets

abstract
  is-set-Π :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    ((x : A)  is-set (B x))  is-set ((x : A)  (B x))
  is-set-Π = is-trunc-Π zero-𝕋

type-Π-Set' :
  {l1 l2 : Level} (A : UU l1) (B : A  Set l2)  UU (l1  l2)
type-Π-Set' A B = (x : A)  type-Set (B x)

is-set-type-Π-Set' :
  {l1 l2 : Level} (A : UU l1) (B : A  Set l2)  is-set (type-Π-Set' A B)
is-set-type-Π-Set' A B =
  is-set-Π  x  is-set-type-Set (B x))

Π-Set' :
  {l1 l2 : Level} (A : UU l1) (B : A  Set l2)  Set (l1  l2)
pr1 (Π-Set' A B) = type-Π-Set' A B
pr2 (Π-Set' A B) = is-set-type-Π-Set' A B

function-Set :
  {l1 l2 : Level} (A : UU l1) (B : Set l2)  Set (l1  l2)
function-Set A B = Π-Set' A  x  B)

type-Π-Set :
  {l1 l2 : Level} (A : Set l1) (B : type-Set A  Set l2)  UU (l1  l2)
type-Π-Set A B = type-Π-Set' (type-Set A) B

is-set-type-Π-Set :
  {l1 l2 : Level} (A : Set l1) (B : type-Set A  Set l2) 
  is-set (type-Π-Set A B)
is-set-type-Π-Set A B =
  is-set-type-Π-Set' (type-Set A) B

Π-Set :
  {l1 l2 : Level} (A : Set l1) 
  (type-Set A  Set l2)  Set (l1  l2)
pr1 (Π-Set A B) = type-Π-Set A B
pr2 (Π-Set A B) = is-set-type-Π-Set A B

The type of functions into a set is a set

abstract
  is-set-function-type :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} 
    is-set B  is-set (A  B)
  is-set-function-type = is-trunc-function-type zero-𝕋

type-hom-Set :
  {l1 l2 : Level}  Set l1  Set l2  UU (l1  l2)
type-hom-Set A B = type-Set A  type-Set B

is-set-type-hom-Set :
  {l1 l2 : Level} (A : Set l1) (B : Set l2) 
  is-set (type-hom-Set A B)
is-set-type-hom-Set A B = is-set-function-type (is-set-type-Set B)

hom-Set :
  {l1 l2 : Level}  Set l1  Set l2  Set (l1  l2)
pr1 (hom-Set A B) = type-hom-Set A B
pr2 (hom-Set A B) = is-set-type-hom-Set A B

precomp-Set :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B) (C : Set l3) 
  (B  type-Set C)  (A  type-Set C)
precomp-Set f C = precomp f (type-Set C)

The type of equivalences between sets is a set

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

  is-set-equiv-is-set : 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

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

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

Extensionality of sets

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

  equiv-eq-Set : (Y : Set l)  X  Y  type-equiv-Set X Y
  equiv-eq-Set = equiv-eq-subuniverse is-set-Prop X

  abstract
    is-contr-total-equiv-Set : is-contr (Σ (Set l) (type-equiv-Set X))
    is-contr-total-equiv-Set =
      is-contr-total-equiv-subuniverse is-set-Prop X

  abstract
    is-equiv-equiv-eq-Set : (Y : Set l)  is-equiv (equiv-eq-Set Y)
    is-equiv-equiv-eq-Set = is-equiv-equiv-eq-subuniverse is-set-Prop X

  eq-equiv-Set : (Y : Set l)  type-equiv-Set X Y  X  Y
  eq-equiv-Set Y = eq-equiv-subuniverse is-set-Prop

  extensionality-Set : (Y : Set l)  (X  Y)  type-equiv-Set X Y
  pr1 (extensionality-Set Y) = equiv-eq-Set Y
  pr2 (extensionality-Set Y) = is-equiv-equiv-eq-Set Y

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

abstract
  is-set-is-emb :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
    is-emb f  is-set B  is-set A
  is-set-is-emb = is-trunc-is-emb neg-one-𝕋

abstract
  is-set-emb :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B)  is-set B  is-set A
  is-set-emb = is-trunc-emb neg-one-𝕋

Any function from a proposition into a set is an embedding

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

  is-emb-is-prop-is-set : is-prop A  is-set B  {f : A  B}  is-emb f
  is-emb-is-prop-is-set is-prop-A is-set-B {f} =
    is-emb-is-prop-map  b  is-prop-Σ is-prop-A  a  is-set-B (f a) b))