Dedekind finite sets

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

Created on 2022-04-06.
Last modified on 2025-02-11.

module univalent-combinatorics.dedekind-finite-sets where
Imports 
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

Idea

Dedekind finite sets are sets X with the property that every embedding X ↪ X is an equivalence.

Definition

is-dedekind-finite-set-Prop : {l : Level} → Set l → Prop l
is-dedekind-finite-set-Prop X =
  Π-Prop
    ( type-Set X → type-Set X)
    ( λ f → function-Prop (is-emb f) (is-equiv-Prop f))

is-dedekind-finite-set : {l : Level} → Set l → UU l
is-dedekind-finite-set X = type-Prop (is-dedekind-finite-set-Prop X)

Dedekind-Finite-Set : (l : Level) → UU (lsuc l)
Dedekind-Finite-Set l = Σ (Set l) is-dedekind-finite-set

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

  set-Dedekind-Finite-Set : Set l
  set-Dedekind-Finite-Set = pr1 X

  type-Dedekind-Finite-Set : UU l
  type-Dedekind-Finite-Set = type-Set set-Dedekind-Finite-Set

  is-set-type-Dedekind-Finite-Set : is-set type-Dedekind-Finite-Set
  is-set-type-Dedekind-Finite-Set = is-set-type-Set set-Dedekind-Finite-Set

  is-dedekind-finite-set-Dedekind-Finite-Set :
    is-dedekind-finite-set set-Dedekind-Finite-Set
  is-dedekind-finite-set-Dedekind-Finite-Set = pr2 X

See also

References

[Sto87]
Lawrence Neff Stout. Dedekind finiteness in topoi. Journal of Pure and Applied Algebra, 49(1):219–225, 1987. doi:10.1016/0022-4049(87)90130-7.

Recent changes