Subfinite types

Content created by Fredrik Bakke.

Created on 2025-08-14.
Last modified on 2025-08-14.

module univalent-combinatorics.subfinite-types where

Imports

open import elementary-number-theory.natural-numbers

open import foundation.decidable-equality
open import foundation.dependent-pair-types
open import foundation.discrete-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.injective-maps
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import univalent-combinatorics.dedekind-finite-types
open import univalent-combinatorics.equality-standard-finite-types
open import univalent-combinatorics.standard-finite-types
open import univalent-combinatorics.subcounting

Idea

A type X is subfinite^¶ if there exists an embedding into a standard finite type.

Definitions

The predicate of being subfinite

is-subfinite-Prop : {l : Level} → UU l → Prop l
is-subfinite-Prop X = trunc-Prop (subcount X)

is-subfinite : {l : Level} → UU l → UU l
is-subfinite X = type-Prop (is-subfinite-Prop X)

is-prop-is-subfinite : {l : Level} {X : UU l} → is-prop (is-subfinite X)
is-prop-is-subfinite {X = X} = is-prop-type-Prop (is-subfinite-Prop X)

The subuniverse of subfinite types

Subfinite-Type : (l : Level) → UU (lsuc l)
Subfinite-Type l = Σ (UU l) (is-subfinite)

module _
  {l : Level} (X : Subfinite-Type l)
  where

  type-Subfinite-Type : UU l
  type-Subfinite-Type = pr1 X

  is-subfinite-type-Subfinite-Type : is-subfinite type-Subfinite-Type
  is-subfinite-type-Subfinite-Type = pr2 X

Properties

The standard finite types are subfinite

Fin-Subfinite-Type : (n : ℕ) → Subfinite-Type lzero
Fin-Subfinite-Type n = (Fin n , unit-trunc-Prop (subcount-Fin n))

Subfinite types are discrete

module _
  {l : Level} (X : Subfinite-Type l)
  where

  has-decidable-equality-type-Subfinite-Type :
    has-decidable-equality (type-Subfinite-Type X)
  has-decidable-equality-type-Subfinite-Type =
    rec-trunc-Prop
      ( has-decidable-equality-Prop (type-Subfinite-Type X))
      ( λ (k , f) → has-decidable-equality-emb f (has-decidable-equality-Fin k))
      ( is-subfinite-type-Subfinite-Type X)

  discrete-type-Subfinite-Type : Discrete-Type l
  discrete-type-Subfinite-Type =
    ( type-Subfinite-Type X , has-decidable-equality-type-Subfinite-Type)

Subfinite types are sets

module _
  {l : Level} (X : Subfinite-Type l)
  where

  is-set-type-Subfinite-Type : is-set (type-Subfinite-Type X)
  is-set-type-Subfinite-Type =
    is-set-has-decidable-equality (has-decidable-equality-type-Subfinite-Type X)

  set-Subfinite-Type : Set l
  set-Subfinite-Type = (type-Subfinite-Type X , is-set-type-Subfinite-Type)

Subfinite types are Dedekind finite

We reproduce a proof given by Gro-Tsen in this MathOverflow answer: https://mathoverflow.net/a/433318.

Proof. Let $X$ be a subfinite type witnessed by $ι : X ↪ F inn$ , and let $f : X ↪ X$ be an arbitrary self-embedding. It suffices to prove $f$ is surjective, so assume given an $x : X$ where we want to show there exists $z : X$ such that $f (z) ＝ x$ . The mapping $i \mapsto f^{i} (x)$ defines an $N$ -indexed sequence of elements of $X$ . Since the standard pigeonhole principle applies to $Fin n$ there has to be $i < j$ in $Fin n$ such that $ι (f^{i} (x)) = ι (f^{j} (x))$ . Since $ι$ is an embedding we in particular have $f^{i} (x) = f^{j} (x)$ . By injectivity of $f$ we can cancel $i$ applications on both sides of the equation to obtain $x = f (f^{j - i - 1} (x))$ , and so $f^{j - i - 1} (x)$ is our desired preimage of $x$ . ∎

module _
  {l : Level} (X : Subfinite-Type l)
  where

  is-dedekind-finite-type-Subfinite-Type' :
    (f : type-Subfinite-Type X → type-Subfinite-Type X) →
    is-injective f → is-equiv f
  is-dedekind-finite-type-Subfinite-Type' f is-injective-f =
    rec-trunc-Prop
      ( is-equiv-Prop f)
      ( λ j → is-dedekind-finite-subcount' j f is-injective-f)
      ( is-subfinite-type-Subfinite-Type X)

  is-dedekind-finite-type-Subfinite-Type :
    is-dedekind-finite (type-Subfinite-Type X)
  is-dedekind-finite-type-Subfinite-Type f is-emb-f =
    is-dedekind-finite-type-Subfinite-Type' f (is-injective-is-emb is-emb-f)

  dedekind-finite-type-Subfinite-Type : Dedekind-Finite-Type l
  dedekind-finite-type-Subfinite-Type =
    ( type-Subfinite-Type X , is-dedekind-finite-type-Subfinite-Type)

The Cantor–Schröder–Bernstein theorem for subfinite types

If two subfinite types X and Y mutually embed, X ↪ Y and Y ↪ X, then X ≃ Y.

module _
  {l1 l2 : Level} (X : Subfinite-Type l1) (Y : Subfinite-Type l2)
  where

  Cantor-Schröder-Bernstein-Subfinite-Type :
    (type-Subfinite-Type X ↪ type-Subfinite-Type Y) →
    (type-Subfinite-Type Y ↪ type-Subfinite-Type X) →
    type-Subfinite-Type X ≃ type-Subfinite-Type Y
  Cantor-Schröder-Bernstein-Subfinite-Type =
    Cantor-Schröder-Bernstein-Dedekind-Finite-Type
      ( dedekind-finite-type-Subfinite-Type X)
      ( dedekind-finite-type-Subfinite-Type Y)

External links

Finiteness in Sheaf Topoi, blog post by Chris Grossack
Fin.Kuratowski at TypeTopology
finite set at $n$ Lab
finite object at $n$ Lab
Finite set at Wikipedia

Recent changes

2025-08-14. Fredrik Bakke. Dedekind finiteness of various notions of finite type (#1422).