# Distributivity of set truncation over finite products

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-02-17.

module univalent-combinatorics.distributivity-of-set-truncation-over-finite-products where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.dependent-universal-property-equivalences
open import foundation.empty-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
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.postcomposition-functions
open import foundation.precomposition-dependent-functions
open import foundation.precomposition-functions
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-equivalences
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-product (map-Π (λ x → unit-trunc-Set)) unit-trunc-Set)
( type-Set B))
( is-equiv-right-factor
( ev-pair)
( precomp
( map-product (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))
( 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 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-Π-equiv-family
( λ 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)