Distributivity of set truncation over finite products

module univalent-combinatorics.distributivity-of-set-truncation-over-finite-products where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functions
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-function-types
open import foundation.functoriality-set-truncation
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.set-truncations
open import foundation.sets
open import foundation.unit-type
open import foundation.universal-property-dependent-pair-types
open import foundation.universal-property-empty-type
open import foundation.universal-property-maybe
open import foundation.universe-levels

open import univalent-combinatorics.counting
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types

Theorem

trunc-Set distributes over Π indexed by Fin.

abstract
  distributive-trunc-Π-Fin-Set :
    {l : Level} (k : ) (A : Fin k  UU l) 
    is-contr
      ( Σ ( ( type-trunc-Set ((x : Fin k)  A x)) 
            ( (x : Fin k)  type-trunc-Set (A x)))
          ( λ e 
            ( map-equiv e  unit-trunc-Set) ~
            ( map-Π  x  unit-trunc-Set))))
  distributive-trunc-Π-Fin-Set zero-ℕ A =
    uniqueness-trunc-Set
      ( Π-Set empty-Set  x  trunc-Set (A x)))
      ( map-Π  x  unit-trunc-Set))
      ( λ {l} B 
        is-equiv-precomp-is-equiv
          ( map-Π  x  unit-trunc-Set))
          ( is-equiv-is-contr
            ( map-Π  x  unit-trunc-Set))
            ( dependent-universal-property-empty' A)
            ( dependent-universal-property-empty' (type-trunc-Set  A)))
          ( type-Set B))
  distributive-trunc-Π-Fin-Set (succ-ℕ k) A =
    uniqueness-trunc-Set
      ( Π-Set (Fin-Set (succ-ℕ k))  x  trunc-Set (A x)))
      ( map-Π  x  unit-trunc-Set))
      ( λ {l} B 
        is-equiv-left-factor
          ( precomp (map-Π  x  unit-trunc-Set)) (type-Set B))
          ( precomp (ev-Maybe {B = type-trunc-Set  A}) (type-Set B))
          ( is-equiv-comp
            ( precomp ev-Maybe (type-Set B))
            ( precomp
              ( map-prod (map-Π  x  unit-trunc-Set)) unit-trunc-Set)
              ( type-Set B))
            ( is-equiv-right-factor
              ( ev-pair)
              ( precomp
                ( map-prod (map-Π  x  unit-trunc-Set)) unit-trunc-Set)
                ( type-Set B))
              ( is-equiv-ev-pair)
              ( is-equiv-map-equiv
                ( ( ( pair
                      ( precomp
                        ( (map-Π  x  unit-trunc-Set)))
                        ( A (inr star)  type-Set B))
                      ( is-set-truncation-is-equiv
                        ( Π-Set (Fin-Set k)  x  trunc-Set (A (inl x))))
                        ( map-Π  x  unit-trunc-Set))
                        { map-equiv
                          ( pr1
                            ( center
                              ( distributive-trunc-Π-Fin-Set k (A  inl))))}
                        ( pr2
                          ( center (distributive-trunc-Π-Fin-Set k (A  inl))))
                        ( is-equiv-map-equiv
                          ( pr1
                            ( center
                              ( distributive-trunc-Π-Fin-Set k (A  inl)))))
                        ( Π-Set' (A (inr star))  a  B)))) ∘e
                    ( equiv-postcomp
                      ( (x : Fin k)  type-trunc-Set (A (inl x)))
                      ( equiv-universal-property-trunc-Set
                        ( A (inr star))
                        ( B)))) ∘e
                  ( equiv-ev-pair))))
            ( is-equiv-precomp-is-equiv
              ( ev-Maybe)
              ( dependent-universal-property-Maybe)
              ( type-Set B)))
          ( is-equiv-precomp-is-equiv
            ( ev-Maybe)
            ( dependent-universal-property-Maybe)
            ( type-Set B)))

module _
  {l : Level} (k : ) (A : Fin k  UU l)
  where

  equiv-distributive-trunc-Π-Fin-Set :
    type-trunc-Set ((x : Fin k)  A x)  ((x : Fin k)  type-trunc-Set (A x))
  equiv-distributive-trunc-Π-Fin-Set =
    pr1 (center (distributive-trunc-Π-Fin-Set k A))

  map-equiv-distributive-trunc-Π-Fin-Set :
    type-trunc-Set ((x : Fin k)  A x)  ((x : Fin k)  type-trunc-Set (A x))
  map-equiv-distributive-trunc-Π-Fin-Set =
    map-equiv equiv-distributive-trunc-Π-Fin-Set

  triangle-distributive-trunc-Π-Fin-Set :
    ( map-equiv-distributive-trunc-Π-Fin-Set  unit-trunc-Set) ~
    ( map-Π  x  unit-trunc-Set))
  triangle-distributive-trunc-Π-Fin-Set =
    pr2 (center (distributive-trunc-Π-Fin-Set k A))

module _
  {l1 l2 : Level} {A : UU l1} (B : A  UU l2)
  where

  abstract
    distributive-trunc-Π-count-Set :
      count A 
      is-contr
        ( Σ ( ( type-trunc-Set ((x : A)  B x)) 
              ( (x : A)  type-trunc-Set (B x)))
            ( λ e 
              ( map-equiv e  unit-trunc-Set) ~
              ( map-Π  x  unit-trunc-Set))))
    distributive-trunc-Π-count-Set (pair k e) =
      is-contr-equiv
        ( Σ ( ( type-trunc-Set ((x : A)  B x)) 
              ( (x : Fin k)  type-trunc-Set (B (map-equiv e x))))
            ( λ f 
              ( map-equiv f  unit-trunc-Set) ~
              ( map-Π  x  unit-trunc-Set)  precomp-Π (map-equiv e) B)))
        ( equiv-Σ
          ( λ f 
            ( map-equiv f  unit-trunc-Set) ~
            ( map-Π  x  unit-trunc-Set)  precomp-Π (map-equiv e) B))
          ( equiv-postcomp-equiv
            ( equiv-precomp-Π e (type-trunc-Set  B))
            ( type-trunc-Set ((x : A)  B x)))
          ( λ f 
            equiv-map-Π
              ( λ h 
                ( ( inv-equiv equiv-funext) ∘e
                  ( equiv-precomp-Π e
                    ( λ x  Id ((map-equiv f  unit-trunc-Set) h x)
                    ( map-Π  y  unit-trunc-Set) h x)))) ∘e
                ( equiv-funext))))
        ( is-contr-equiv'
          ( Σ ( ( type-trunc-Set ((x : Fin k)  B (map-equiv e x))) 
                ( (x : Fin k)  type-trunc-Set (B (map-equiv e x))))
              ( λ f 
                ( map-equiv f  unit-trunc-Set) ~
                ( map-Π  x  unit-trunc-Set))))
          ( equiv-Σ
            ( λ f 
              ( map-equiv f  unit-trunc-Set) ~
              ( map-Π  x  unit-trunc-Set)  precomp-Π (map-equiv e) B))
            ( equiv-precomp-equiv
              ( equiv-trunc-Set (equiv-precomp-Π e B))
              ( (x : Fin k)  type-trunc-Set (B (map-equiv e x))))
            ( λ f 
              equiv-Π
                ( λ h 
                  Id ( map-equiv f
                       ( map-equiv
                         ( equiv-trunc-Set (equiv-precomp-Π e B))
                         ( unit-trunc-Set h)))
                     ( map-Π  x  unit-trunc-Set)  x  h (map-equiv e x))))
                ( equiv-Π B e  x  id-equiv))
                ( λ h 
                  ( ( inv-equiv equiv-funext) ∘e
                    ( equiv-Π
                      ( λ x 
                        Id ( map-equiv f
                             ( map-equiv-trunc-Set
                               ( equiv-precomp-Π e B)
                               ( unit-trunc-Set
                                 ( map-equiv-Π B e  x  id-equiv) h)))
                             ( x))
                           ( unit-trunc-Set
                             ( map-equiv-Π B e
                               ( λ z  id-equiv)
                               ( h)
                               ( map-equiv e x))))
                      ( id-equiv)
                      ( λ x 
                        ( equiv-concat
                          ( ap
                            ( λ t  map-equiv f t x)
                            ( ( naturality-unit-trunc-Set
                                ( precomp-Π (map-equiv e) B)
                                ( map-equiv-Π B e  _  id-equiv) h)) 
                              ( ap
                                ( unit-trunc-Set)
                                ( eq-htpy
                                  ( compute-map-equiv-Π B e
                                    ( λ _  id-equiv)
                                    ( h))))))
                          ( unit-trunc-Set
                            ( map-equiv-Π B e
                              ( λ _  id-equiv)
                              ( h)
                              ( map-equiv e x)))) ∘e
                        ( equiv-concat'
                          ( map-equiv f (unit-trunc-Set h) x)
                          ( ap unit-trunc-Set
                            ( inv
                              ( compute-map-equiv-Π B e
                                ( λ _  id-equiv)
                                ( h)
                                ( x)))))))) ∘e
                  ( equiv-funext))))
          ( distributive-trunc-Π-Fin-Set k (B  map-equiv e)))

module _
  {l1 l2 : Level} {A : UU l1} (B : A  UU l2) (c : count A)
  where

  equiv-distributive-trunc-Π-count-Set :
    ( type-trunc-Set ((x : A)  B x))  ((x : A)  type-trunc-Set (B x))
  equiv-distributive-trunc-Π-count-Set =
    pr1 (center (distributive-trunc-Π-count-Set B c))

  map-equiv-distributive-trunc-Π-count-Set :
    ( type-trunc-Set ((x : A)  B x))  ((x : A)  type-trunc-Set (B x))
  map-equiv-distributive-trunc-Π-count-Set =
    map-equiv equiv-distributive-trunc-Π-count-Set

  triangle-distributive-trunc-Π-count-Set :
    ( map-equiv-distributive-trunc-Π-count-Set  unit-trunc-Set) ~
    ( map-Π  x  unit-trunc-Set))
  triangle-distributive-trunc-Π-count-Set =
    pr2 (center (distributive-trunc-Π-count-Set B c))

module _
  {l1 l2 : Level} {A : UU l1} (B : A  UU l2) (H : is-finite A)
  where

  abstract
    distributive-trunc-Π-is-finite-Set :
      is-contr
        ( Σ ( ( type-trunc-Set ((x : A)  B x)) 
              ( (x : A)  type-trunc-Set (B x)))
            ( λ e 
              ( map-equiv e  unit-trunc-Set) ~
              ( map-Π  x  unit-trunc-Set))))
    distributive-trunc-Π-is-finite-Set =
      apply-universal-property-trunc-Prop H
        ( is-contr-Prop _)
        ( distributive-trunc-Π-count-Set B)

  equiv-distributive-trunc-Π-is-finite-Set :
    ( type-trunc-Set ((x : A)  B x))  ((x : A)  type-trunc-Set (B x))
  equiv-distributive-trunc-Π-is-finite-Set =
    pr1 (center distributive-trunc-Π-is-finite-Set)

  map-equiv-distributive-trunc-Π-is-finite-Set :
    ( type-trunc-Set ((x : A)  B x))  ((x : A)  type-trunc-Set (B x))
  map-equiv-distributive-trunc-Π-is-finite-Set =
    map-equiv equiv-distributive-trunc-Π-is-finite-Set

  triangle-distributive-trunc-Π-is-finite-Set :
    ( map-equiv-distributive-trunc-Π-is-finite-Set  unit-trunc-Set) ~
    ( map-Π  x  unit-trunc-Set))
  triangle-distributive-trunc-Π-is-finite-Set =
    pr2 (center distributive-trunc-Π-is-finite-Set)