Counting the elements of dependent pair types

module univalent-combinatorics.counting-dependent-pair-types where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.sums-of-natural-numbers

open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.decidable-equality
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.functions
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.sections
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universe-levels

open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.decidable-propositions
open import univalent-combinatorics.double-counting
open import univalent-combinatorics.standard-finite-types

Idea

Consider a type family B over A, and consider the following statements

  1. The elements of A can be counted.
  2. For each x : A, the elements of B x can be counted
  3. The elements of Σ A B can be counted.

If 1 holds, then 2 holds if and only if 3 holds. Furthermore if 2 and 3 hold, then 1 holds if and only if the elements of Σ A (¬ ∘ B) can be counted, i.e., if the elements in the complement of B can be counted.

Proofs

Σ A B can be counted if A can be counted and if each B x can be counted

count-Σ' :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
  (k : ) (e : Fin k  A)  ((x : A)  count (B x))  count (Σ A B)
count-Σ' zero-ℕ e f =
  count-is-empty
    ( λ x 
      is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl (pr1 x))
count-Σ' {l1} {l2} {A} {B} (succ-ℕ k) e f =
  count-equiv
    ( ( equiv-Σ-equiv-base B e) ∘e
      ( ( inv-equiv
          ( right-distributive-Σ-coprod (Fin k) unit (B  map-equiv e))) ∘e
        ( equiv-coprod
          ( id-equiv)
          ( inv-equiv
            ( left-unit-law-Σ (B  (map-equiv e  inr)))))))
    ( count-coprod
      ( count-Σ' k id-equiv  x  f (map-equiv e (inl x))))
      ( f (map-equiv e (inr star))))

abstract
  equiv-count-Σ' :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    (k : ) (e : Fin k  A) (f : (x : A)  count (B x)) 
    Fin (number-of-elements-count (count-Σ' k e f))  Σ A B
  equiv-count-Σ' k e f = pr2 (count-Σ' k e f)

count-Σ :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
  count A  ((x : A)  count (B x))  count (Σ A B)
pr1 (count-Σ (pair k e) f) = number-of-elements-count (count-Σ' k e f)
pr2 (count-Σ (pair k e) f) = equiv-count-Σ' k e f

We compute the number of elements of a Σ-type

abstract
  number-of-elements-count-Σ' :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (k : ) (e : Fin k  A) 
    (f : (x : A)  count (B x)) 
    Id ( number-of-elements-count (count-Σ' k e f))
      ( sum-Fin-ℕ k  x  number-of-elements-count (f (map-equiv e x))))
  number-of-elements-count-Σ' zero-ℕ e f = refl
  number-of-elements-count-Σ' (succ-ℕ k) e f =
    ( number-of-elements-count-coprod
      ( count-Σ' k id-equiv  x  f (map-equiv e (inl x))))
      ( f (map-equiv e (inr star)))) 
    ( ap
      ( _+ℕ (number-of-elements-count (f (map-equiv e (inr star)))))
      ( number-of-elements-count-Σ' k id-equiv  x  f (map-equiv e (inl x)))))

abstract
  number-of-elements-count-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (e : count A)
    (f : (x : A)  count (B x)) 
    Id ( number-of-elements-count (count-Σ e f))
      ( sum-count-ℕ e  x  number-of-elements-count (f x)))
  number-of-elements-count-Σ (pair k e) f = number-of-elements-count-Σ' k e f

If A and Σ A B can be counted, then each B x can be counted

count-fiber-count-Σ :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
  has-decidable-equality A  count (Σ A B)  (x : A)  count (B x)
count-fiber-count-Σ {B = B} d f x =
  count-equiv
    ( equiv-fib-pr1 B x)
    ( count-Σ f
      ( λ z  count-eq d (pr1 z) x))

count-fiber-count-Σ-count-base :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
  count A  count (Σ A B)  (x : A)  count (B x)
count-fiber-count-Σ-count-base e f x =
  count-fiber-count-Σ (has-decidable-equality-count e) f x

If Σ A B and each B x can be counted, and if B has a section, then A can be counted

count-fib-map-section :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (b : (x : A)  B x) 
  count (Σ A B)  ((x : A)  count (B x)) 
  (t : Σ A B)  count (fib (map-section b) t)
count-fib-map-section {l1} {l2} {A} {B} b e f (pair y z) =
  count-equiv'
    ( ( ( left-unit-law-Σ-is-contr
            ( is-contr-total-path' y)
            ( pair y refl)) ∘e
        ( inv-associative-Σ A
          ( λ x  Id x y)
          ( λ t  Id (tr B (pr2 t) (b (pr1 t))) z))) ∘e
      ( equiv-tot  x  equiv-pair-eq-Σ (pair x (b x)) (pair y z))))
    ( count-eq (has-decidable-equality-count (f y)) (b y) z)

count-base-count-Σ :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (b : (x : A)  B x) 
  count (Σ A B)  ((x : A)  count (B x))  count A
count-base-count-Σ b e f =
  count-equiv
    ( equiv-total-fib-map-section b)
    ( count-Σ e (count-fib-map-section b e f))

More generally, if Σ A B and each B x can be counted, then A can be counted if and only if the type Σ A (¬ ∘ B) can be counted. However, to avoid having to invoke function extensionality, we show that if Σ A B and each B x can be counted, then A can be counted if and only if

   count (Σ A (λ x → is-zero-ℕ (number-of-elements-count (f x)))),

where f : (x : A) → count (B x). Thus, we have a precise characterization of when the elements of A can be counted, if it is given that Σ A B and each B x can be counted.

section-count-base-count-Σ' :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2}  count (Σ A B) 
  (f : (x : A)  count (B x)) 
  count (Σ A  x  is-zero-ℕ (number-of-elements-count (f x)))) 
  (x : A)  (B x) + (is-zero-ℕ (number-of-elements-count (f x)))
section-count-base-count-Σ' e f g x with
  is-decidable-is-zero-ℕ (number-of-elements-count (f x))
... | inl p = inr p
... | inr H with is-successor-is-nonzero-ℕ H
... | (pair k p) = inl (map-equiv-count (f x) (tr Fin (inv p) (zero-Fin k)))

count-base-count-Σ' :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2}  count (Σ A B) 
  (f : (x : A)  count (B x)) 
  count (Σ A  x  is-zero-ℕ (number-of-elements-count (f x))))  count A
count-base-count-Σ' {l1} {l2} {A} {B} e f g =
  count-base-count-Σ
    ( section-count-base-count-Σ' e f g)
    ( count-equiv'
      ( left-distributive-Σ-coprod A B
        ( λ x  is-zero-ℕ (number-of-elements-count (f x))))
      ( count-coprod e g))
    ( λ x 
      count-coprod
        ( f x)
        ( count-eq has-decidable-equality-ℕ
          ( number-of-elements-count (f x))
          ( zero-ℕ)))

If A can be counted and Σ A P can be counted for a subtype of A, then P is decidable

is-decidable-count-Σ :
  {l1 l2 : Level} {X : UU l1} {P : X  UU l2} 
  count X  count (Σ X P)  (x : X)  is-decidable (P x)
is-decidable-count-Σ e f x =
  is-decidable-count (count-fiber-count-Σ-count-base e f x)
abstract
  double-counting-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (count-A : count A)
    (count-B : (x : A)  count (B x)) (count-C : count (Σ A B)) 
    Id ( number-of-elements-count count-C)
       ( sum-count-ℕ count-A  x  number-of-elements-count (count-B x)))
  double-counting-Σ count-A count-B count-C =
    ( double-counting count-C (count-Σ count-A count-B)) 
    ( number-of-elements-count-Σ count-A count-B)

abstract
  sum-number-of-elements-count-fiber-count-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (e : count A)
    (f : count (Σ A B)) 
    Id ( sum-count-ℕ e
         ( λ x  number-of-elements-count
           (count-fiber-count-Σ-count-base e f x)))
       ( number-of-elements-count f)
  sum-number-of-elements-count-fiber-count-Σ e f =
    ( inv
      ( number-of-elements-count-Σ e (count-fiber-count-Σ-count-base e f))) 
    ( double-counting (count-Σ e (count-fiber-count-Σ-count-base e f)) f)

abstract
  double-counting-fiber-count-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (count-A : count A)
    (count-B : (x : A)  count (B x)) (count-C : count (Σ A B)) (x : A) 
    Id ( number-of-elements-count (count-B x))
       ( number-of-elements-count
         ( count-fiber-count-Σ-count-base count-A count-C x))
  double-counting-fiber-count-Σ count-A count-B count-C x =
    double-counting
      ( count-B x)
      ( count-fiber-count-Σ-count-base count-A count-C x)

abstract
  sum-number-of-elements-count-base-count-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (b : (x : A)  B x) 
    (count-ΣAB : count (Σ A B)) (count-B : (x : A)  count (B x)) 
    Id ( sum-count-ℕ
         ( count-base-count-Σ b count-ΣAB count-B)
         ( λ x  number-of-elements-count (count-B x)))
       ( number-of-elements-count count-ΣAB)
  sum-number-of-elements-count-base-count-Σ b count-ΣAB count-B =
    ( inv
      ( number-of-elements-count-Σ
        ( count-base-count-Σ b count-ΣAB count-B)
        ( count-B))) 
    ( double-counting
      ( count-Σ (count-base-count-Σ b count-ΣAB count-B) count-B)
      ( count-ΣAB))

abstract
  double-counting-base-count-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (b : (x : A)  B x) 
    (count-A : count A) (count-B : (x : A)  count (B x))
    (count-ΣAB : count (Σ A B)) 
    Id ( number-of-elements-count (count-base-count-Σ b count-ΣAB count-B))
       ( number-of-elements-count count-A)
  double-counting-base-count-Σ b count-A count-B count-ΣAB =
    double-counting (count-base-count-Σ b count-ΣAB count-B) count-A

abstract
  sum-number-of-elements-count-base-count-Σ' :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (count-ΣAB : count (Σ A B)) 
    ( count-B : (x : A)  count (B x)) 
    ( count-nB :
      count (Σ A  x  is-zero-ℕ (number-of-elements-count (count-B x))))) 
    Id ( sum-count-ℕ
         ( count-base-count-Σ' count-ΣAB count-B count-nB)
         ( λ x  number-of-elements-count (count-B x)))
       ( number-of-elements-count count-ΣAB)
  sum-number-of-elements-count-base-count-Σ' count-ΣAB count-B count-nB =
    ( inv
      ( number-of-elements-count-Σ
        ( count-base-count-Σ' count-ΣAB count-B count-nB)
        ( count-B))) 
    ( double-counting
      ( count-Σ
        ( count-base-count-Σ' count-ΣAB count-B count-nB)
        ( count-B))
      ( count-ΣAB))

abstract
  double-counting-base-count-Σ' :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (count-A : count A)
    ( count-B : (x : A)  count (B x)) (count-ΣAB : count (Σ A B)) 
    ( count-nB :
      count (Σ A  x  is-zero-ℕ (number-of-elements-count (count-B x))))) 
    Id ( number-of-elements-count
         ( count-base-count-Σ' count-ΣAB count-B count-nB))
       ( number-of-elements-count count-A)
  double-counting-base-count-Σ' count-A count-B count-ΣAB count-nB =
    double-counting (count-base-count-Σ' count-ΣAB count-B count-nB) count-A