Counting the elements of dependent function types

module univalent-combinatorics.dependent-function-types where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-dependent-function-types
open import foundation.homotopies
open import foundation.propositional-truncations
open import foundation.unit-type
open import foundation.universal-property-coproduct-types
open import foundation.universal-property-empty-type
open import foundation.universal-property-unit-type
open import foundation.universe-levels

open import univalent-combinatorics.cartesian-product-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.finite-choice
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types

Idea

Dependent products of finite types indexed by a finite type are finite.

Properties

Counting dependent products indexed by standard finite types

If the elements of A can be counted and if for each x : A the elements of B x can be counted, then the elements of Π A B can be counted.

count-Π-Fin :
  {l1 : Level} (k : ) {B : Fin k  UU l1} 
  ((x : Fin k)  count (B x))  count ((x : Fin k)  B x)
count-Π-Fin {l1} zero-ℕ {B} e =
  count-is-contr (dependent-universal-property-empty' B)
count-Π-Fin {l1} (succ-ℕ k) {B} e =
  count-equiv'
    ( equiv-dependent-universal-property-coprod B)
    ( count-prod
      ( count-Π-Fin k  x  e (inl x)))
      ( count-equiv'
        ( equiv-dependent-universal-property-unit (B  inr))
        ( e (inr star))))

Counting on dependent function types

count-Π :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
  count A  ((x : A)  count (B x))  count ((x : A)  B x)
count-Π {l1} {l2} {A} {B} e f =
  count-equiv'
    ( equiv-precomp-Π (equiv-count e) B)
    ( count-Π-Fin (number-of-elements-count e)  x  f (map-equiv-count e x)))

Finiteness of dependent function types

abstract
  is-finite-Π :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    is-finite A  ((x : A)  is-finite (B x))  is-finite ((x : A)  B x)
  is-finite-Π {l1} {l2} {A} {B} f g =
    apply-universal-property-trunc-Prop f
      ( is-finite-Prop ((x : A)  B x))
      ( λ e 
        apply-universal-property-trunc-Prop
          ( finite-choice f g)
          ( is-finite-Prop ((x : A)  B x))
          ( λ h  unit-trunc-Prop (count-Π e h)))

  is-finite-Π' :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    is-finite A  ((x : A)  is-finite (B x))  is-finite ({x : A}  B x)
  is-finite-Π' {l1} {l2} {A} {B} f g =
    is-finite-equiv
      (( pair
        ( λ f {x}  f x)
        ( is-equiv-has-inverse
          ( λ g x  g {x})
          ( refl-htpy)
          ( refl-htpy))))
      (is-finite-Π f g)

Π-𝔽 : {l1 l2 : Level} (A : 𝔽 l1) (B : type-𝔽 A  𝔽 l2)  𝔽 (l1  l2)
pr1 (Π-𝔽 A B) = (x : type-𝔽 A)  type-𝔽 (B x)
pr2 (Π-𝔽 A B) = is-finite-Π (is-finite-type-𝔽 A)  x  is-finite-type-𝔽 (B x))

Π-𝔽' : {l1 l2 : Level} (A : 𝔽 l1) (B : type-𝔽 A  𝔽 l2)  𝔽 (l1  l2)
pr1 (Π-𝔽' A B) = {x : type-𝔽 A}  type-𝔽 (B x)
pr2 (Π-𝔽' A B) =
  is-finite-Π' (is-finite-type-𝔽 A)  x  is-finite-type-𝔽 (B x))