Dependent pair types of finite types

module univalent-combinatorics.dependent-pair-types where

Imports

open import foundation.dependent-pair-types public

open import foundation.complements
open import foundation.contractible-types
open import foundation.decidable-types
open import foundation.empty-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sections
open import foundation.sets
open import foundation.subtypes
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.counting-dependent-pair-types
open import univalent-combinatorics.decidable-propositions
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-choice
open import univalent-combinatorics.finite-types

Idea

In this file we study finiteness in relation to dependent pair types.

Properties

A dependent sum of finite types indexed by a finite type is finite

abstract
  is-finite-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    is-finite A → ((a : A) → is-finite (B a)) → is-finite (Σ A B)
  is-finite-Σ {A = A} {B} H K =
    apply-universal-property-trunc-Prop H
      ( is-finite-Prop (Σ A B))
      ( λ (e : count A) →
        apply-universal-property-trunc-Prop
          ( finite-choice H K)
          ( is-finite-Prop (Σ A B))
          ( is-finite-count ∘ (count-Σ e)))

Σ-𝔽 : {l1 l2 : Level} (A : 𝔽 l1) (B : type-𝔽 A → 𝔽 l2) → 𝔽 (l1 ⊔ l2)
pr1 (Σ-𝔽 A B) = Σ (type-𝔽 A) (λ a → type-𝔽 (B a))
pr2 (Σ-𝔽 A B) =
  is-finite-Σ
    ( is-finite-type-𝔽 A)
    ( λ a → is-finite-type-𝔽 (B a))

If `A` and `Σ A B` are finite, then eacy `B a` is finite

abstract
  is-finite-fiber-is-finite-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    is-finite A → is-finite (Σ A B) → (a : A) → is-finite (B a)
  is-finite-fiber-is-finite-Σ {l1} {l2} {A} {B} f g a =
    apply-universal-property-trunc-Prop f
      ( is-finite-Prop (B a))
      ( λ e → map-trunc-Prop (λ h → count-fiber-count-Σ-count-base e h a) g)

If `B` is a family of finite types over `A` equipped with a (mere) section and `Σ A B` is finite, then `A` is finite

abstract
  is-finite-base-is-finite-Σ-section :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (b : (a : A) → B a) →
    is-finite (Σ A B) → ((a : A) → is-finite (B a)) → is-finite A
  is-finite-base-is-finite-Σ-section {l1} {l2} {A} {B} b f g =
    apply-universal-property-trunc-Prop f
      ( is-finite-Prop A)
      ( λ e →
        is-finite-count
          ( count-equiv
            ( ( equiv-total-fib-map-section b) ∘e
              ( equiv-tot
                ( λ t →
                  ( equiv-tot (λ x → equiv-eq-pair-Σ (map-section b x) t)) ∘e
                  ( ( associative-Σ A
                      ( λ (x : A) → Id x (pr1 t))
                      ( λ s → Id (tr B (pr2 s) (b (pr1 s))) (pr2 t))) ∘e
                    ( inv-left-unit-law-Σ-is-contr
                      ( is-contr-total-path' (pr1 t))
                      ( pair (pr1 t) refl))))))
            ( count-Σ e
              ( λ t →
                count-eq
                  ( has-decidable-equality-is-finite (g (pr1 t)))
                  ( b (pr1 t))
                  ( pr2 t)))))

abstract
  is-finite-base-is-finite-Σ-mere-section :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    type-trunc-Prop ((a : A) → B a) →
    is-finite (Σ A B) → ((a : A) → is-finite (B a)) → is-finite A
  is-finite-base-is-finite-Σ-mere-section {l1} {l2} {A} {B} H f g =
    apply-universal-property-trunc-Prop H
      ( is-finite-Prop A)
      ( λ b → is-finite-base-is-finite-Σ-section b f g)

If `B` is a family of finite inhabited types over a set `A` and `Σ A B` is finite, then `A` is finite

abstract
  is-finite-base-is-finite-Σ-merely-inhabited :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    is-set A → (b : (a : A) → type-trunc-Prop (B a)) →
    is-finite (Σ A B) → ((a : A) → is-finite (B a)) → is-finite A
  is-finite-base-is-finite-Σ-merely-inhabited {l1} {l2} {A} {B} K b f g =
    is-finite-base-is-finite-Σ-mere-section
      ( choice-is-finite-Σ-is-finite-fiber K f g b)
      ( f)
      ( g)

If `B` is a family of finite types over `A` with finite complement, and if `Σ A B` is finite, then `A` is finite

abstract
  is-finite-base-is-finite-complement :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → is-set A →
    is-finite (Σ A B) → (g : (a : A) → is-finite (B a)) →
    is-finite (complement B) → is-finite A
  is-finite-base-is-finite-complement {l1} {l2} {A} {B} K f g h =
    is-finite-equiv
      ( ( right-unit-law-Σ-is-contr
          ( λ x →
            is-proof-irrelevant-is-prop
              ( is-prop-is-inhabited-or-empty (B x))
              ( is-inhabited-or-empty-is-finite (g x)))) ∘e
        ( inv-equiv
          ( left-distributive-Σ-coprod A
            ( λ x → type-trunc-Prop (B x))
            ( λ x → is-empty (B x)))))
      ( is-finite-coprod
        ( is-finite-base-is-finite-Σ-merely-inhabited
          ( is-set-type-subtype (λ x → trunc-Prop _) K)
          ( λ t → pr2 t)
          ( is-finite-equiv
            ( equiv-right-swap-Σ)
            ( is-finite-Σ
              ( f)
              ( λ x → is-finite-type-trunc-Prop (g (pr1 x)))))
          ( λ x → g (pr1 x)))
        ( h))