Kőnig’s theorem

Content created by Fredrik Bakke.

Created on 2026-09-09.
Last modified on 2026-09-09.

module set-theory.konigs-theorem where
Imports 
open import foundation.binary-transport
open import foundation.complements-images
open import foundation.dependent-pair-types
open import foundation.dependent-products-propositions
open import foundation.function-extensionality
open import foundation.function-extensionality-axiom
open import foundation.function-types
open import foundation.functoriality-propositional-truncation
open import foundation.identity-types
open import foundation.nonsurjective-maps
open import foundation.projective-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import set-theory.cardinality-projective-sets
open import set-theory.cardinals
open import set-theory.dependent-products-cardinals
open import set-theory.dependent-sums-cardinals
open import set-theory.strict-indexed-inequality-cardinals

Idea

Kőnig’s theorem states that for any pair of families of cardinals and over , if for all then we have that .

In constructive mathematics we have to be more mindful of our statements than classically. Here is any projective set, and by we mean that is inhabited and that for every map there exists an element of that does not hit.

Lemma

Given a projective type and a pair of families of types and over such that for every every function from to misses an element, then every function from to misses an element.

module _
  {l1 l2 l3 : Level}
  {I : UU l1} (is-projective-I : is-projective-Level (l2 ⊔ l3) I)
  {A : I → UU l2} {B : I → UU l3}
  where

  is-nonsurjective-map-Σ-Π-is-projective-base :
    (H : (i : I) (f : A i → B i) → is-nonsurjective f)
    (g : Σ I A → ((i : I) → B i)) → is-nonsurjective g
  is-nonsurjective-map-Σ-Π-is-projective-base H g =
    map-trunc-Prop
      ( λ h → (pr1 ∘ h , (λ ((i , a) , r) → pr2 (h i) (a , htpy-eq r i))))
      ( is-projective-I
        ( λ i → nonim (λ a → g (i , a) i)) (λ i → H i (λ a → g (i , a) i)))

Theorem

module _
  {l1 l2 : Level}
  (I : Set l1)
  (is-projective-I : is-projective-Level l2 (type-Set I))
  where

  le-indexed-cardinality-Σ-Π' :
    (A B : type-Set I → Set l2) →
    ((i : type-Set I) → le-indexed-cardinality' (A i) (B i)) →
    le-indexed-cardinality' (Σ-Set I A) (Π-Set I B)
  le-indexed-cardinality-Σ-Π' A B p =
    ( is-projective-I (type-Set ∘ B) (pr1 ∘ p) ,
      is-nonsurjective-map-Σ-Π-is-projective-base is-projective-I (pr2 ∘ p))

  le-indexed-cardinality-Σ-Π :
    (A B : type-Set I → Set l2) →
    ((i : type-Set I) → le-indexed-cardinality (A i) (B i)) →
    le-indexed-cardinality (Σ-Set I A) (Π-Set I B)
  le-indexed-cardinality-Σ-Π A B p =
    unit-le-indexed-cardinality
      ( Σ-Set I A)
      ( Π-Set I B)
      ( le-indexed-cardinality-Σ-Π' A B
        ( λ i → inv-unit-le-indexed-cardinality (A i) (B i) (p i)))

module _
  {l1 l2 : Level}
  (I : Projective-Set l1 (lsuc l2))
  (let set-I = set-Projective-Set I)
  (let type-I = type-Projective-Set I)
  (let I' = cardinality-projective-set-Projective-Set I)
  where

  le-indexed-Σ-Π-Cardinal :
    (A B : type-I → Cardinal l2) →
    ((i : type-I) → le-indexed-Cardinal (A i) (B i)) →
    le-indexed-Cardinal (Σ-Cardinal I' A) (Π-Cardinal I' B)
  le-indexed-Σ-Π-Cardinal =
    apply-twice-ind-Cardinality-Projective-Set I'
      ( λ A B →
        set-Prop
          ( function-Prop
            ( (i : type-I) → le-indexed-Cardinal (A i) (B i))
            ( le-indexed-prop-Cardinal
              ( Σ-Cardinal I' A)
              ( Π-Cardinal I' B))))
      ( λ A B p →
        binary-tr
          ( le-indexed-Cardinal)
          ( inv (compute-Σ-Cardinal I' A))
          ( inv (compute-Π-Cardinal I' B))
          ( le-indexed-cardinality-Σ-Π
            ( set-I)
            ( is-projective-is-projective-lsuc-Level l2
              ( is-projective-Projective-Set I))
            ( A)
            ( B)
            ( p)))

Recent changes