Dual Dedekind finite types

Content created by Fredrik Bakke.

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

module univalent-combinatorics.dual-dedekind-finite-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-propositional-truncation
open import foundation.homotopies
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.split-surjective-maps
open import foundation.surjective-maps
open import foundation.universe-levels

open import synthetic-homotopy-theory.acyclic-maps

Idea

Dual Dedekind finite types are types X with the property that every acyclic endomap X ↠ X is an equivalence.

Recall that a Dedekind finite type is a type such that every self-embedding is an equivalence. The dual Dedekind finiteness condition is formally dual to the Dedekind finiteness condition, since acyclic maps are precisely the epimorphisms in the ∞-category of types, while embeddings are precisely the monomorphisms.

Definitions

The predicate of being a dual Dedekind finite type

is-dual-dedekind-finite-Prop : {l : Level} → UU l → Prop l
is-dual-dedekind-finite-Prop X =
  Π-Prop
    ( X → X)
    ( λ f → function-Prop (is-acyclic-map f) (is-equiv-Prop f))

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

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

The subuniverse of dual Dedekind finite types

Dual-Dedekind-Finite-Type : (l : Level) → UU (lsuc l)
Dual-Dedekind-Finite-Type l = Σ (UU l) is-dual-dedekind-finite

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

  type-Dual-Dedekind-Finite-Type : UU l
  type-Dual-Dedekind-Finite-Type = pr1 X

  is-dual-dedekind-finite-Dual-Dedekind-Finite-Type :
    is-dual-dedekind-finite type-Dual-Dedekind-Finite-Type
  is-dual-dedekind-finite-Dual-Dedekind-Finite-Type = pr2 X

Properties

If two dual Dedekind finite types mutually project, they are equivalent

This can be understood as a constructive dual Cantor–Schröder–Bernstein theorem for dual Dedekind finite types.

Proof. Given epimorphisms f : X ↠ Y and g : Y ↠ X, we have a commuting diagram

       g ∘ f
    X ------> X
    |       ∧ |
  f |   g /   | f
    |   /     |
    ∨ /       ∨
    Y ------> Y.
       f ∘ g

The top and bottom rows are equivalences by dual Dedekind finiteness, so by the 6-for-2 property of equivalences every edge in this diagram is an equivalence. ∎

module _
  {l1 l2 : Level}
  (X : Dual-Dedekind-Finite-Type l1)
  (Y : Dual-Dedekind-Finite-Type l2)
  (f :
    acyclic-map
      ( type-Dual-Dedekind-Finite-Type X)
      ( type-Dual-Dedekind-Finite-Type Y))
  (g :
    acyclic-map
      ( type-Dual-Dedekind-Finite-Type Y)
      ( type-Dual-Dedekind-Finite-Type X))
  where

  is-equiv-map-Cantor-Schröder-Bernstein-Dual-Dedekind-Finite-Type :
    is-equiv (map-acyclic-map f)
  is-equiv-map-Cantor-Schröder-Bernstein-Dual-Dedekind-Finite-Type =
    is-equiv-left-is-equiv-top-is-equiv-bottom-square
      ( map-acyclic-map f)
      ( map-acyclic-map f)
      ( map-acyclic-map g)
      ( refl-htpy)
      ( refl-htpy)
      ( is-dual-dedekind-finite-Dual-Dedekind-Finite-Type X
        ( map-acyclic-map g ∘ map-acyclic-map f)
        ( is-acyclic-map-comp-acyclic-map g f))
      ( is-dual-dedekind-finite-Dual-Dedekind-Finite-Type Y
        ( map-acyclic-map f ∘ map-acyclic-map g)
        ( is-acyclic-map-comp-acyclic-map f g))

  Cantor-Schröder-Bernstein-Dual-Dedekind-Finite-Type :
    type-Dual-Dedekind-Finite-Type X ≃ type-Dual-Dedekind-Finite-Type Y
  Cantor-Schröder-Bernstein-Dual-Dedekind-Finite-Type =
    ( map-acyclic-map f ,
      is-equiv-map-Cantor-Schröder-Bernstein-Dual-Dedekind-Finite-Type)

See also

Recent changes