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)