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))