Kuratowski finite sets

Content created by Fredrik Bakke.

Created on 2024-08-22.
Last modified on 2024-09-23.

module univalent-combinatorics.kuratowski-finite-sets where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.decidable-equality
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.surjective-maps
open import foundation.universe-levels

open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.image-of-maps
open import univalent-combinatorics.standard-finite-types

Idea

A Kuratowski finite set is a set X for which there exists a surjection into X from a standard finite type. In other words, the Kuratowski finite set are the set-quotient of a standard finite type.

Definition

is-kuratowski-finite-set-Prop : {l : Level} → Set l → Prop l
is-kuratowski-finite-set-Prop X =
  exists-structure-Prop ℕ (λ n → Fin n ↠ type-Set X)

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

𝔽-Kuratowski : (l : Level) → UU (lsuc l)
𝔽-Kuratowski l = Σ (Set l) is-kuratowski-finite-set

module _
  {l : Level} (X : 𝔽-Kuratowski l)
  where

  set-𝔽-Kuratowski : Set l
  set-𝔽-Kuratowski = pr1 X

  type-𝔽-Kuratowski : UU l
  type-𝔽-Kuratowski = type-Set set-𝔽-Kuratowski

  is-set-type-𝔽-Kuratowski : is-set type-𝔽-Kuratowski
  is-set-type-𝔽-Kuratowski = is-set-type-Set set-𝔽-Kuratowski

  is-kuratowski-finite-set-𝔽-Kuratowski :
    is-kuratowski-finite-set set-𝔽-Kuratowski
  is-kuratowski-finite-set-𝔽-Kuratowski = pr2 X

Properties

A Kuratowski finite set is finite if and only if it has decidable equality

is-finite-has-decidable-equality-type-𝔽-Kuratowski :
  {l : Level} (X : 𝔽-Kuratowski l) →
  has-decidable-equality (type-𝔽-Kuratowski X) →
  is-finite (type-𝔽-Kuratowski X)
is-finite-has-decidable-equality-type-𝔽-Kuratowski X H =
  apply-universal-property-trunc-Prop
    ( is-kuratowski-finite-set-𝔽-Kuratowski X)
    ( is-finite-Prop (type-𝔽-Kuratowski X))
    ( λ (n , f , s) → is-finite-codomain (is-finite-Fin n) s H)

has-decidable-equality-is-finite-type-𝔽-Kuratowski :
  {l : Level} (X : 𝔽-Kuratowski l) →
  is-finite (type-𝔽-Kuratowski X) →
  has-decidable-equality (type-𝔽-Kuratowski X)
has-decidable-equality-is-finite-type-𝔽-Kuratowski X =
  has-decidable-equality-is-finite

See also

Recent changes