The universal property of truncations
module foundation.universal-property-truncation where
Imports
open import foundation-core.universal-property-truncation public open import foundation.contractible-types open import foundation.function-extensionality open import foundation.identity-types open import foundation.propositional-truncations open import foundation.surjective-maps open import foundation.type-arithmetic-dependent-function-types open import foundation.type-theoretic-principle-of-choice open import foundation.universal-property-dependent-pair-types open import foundation.universal-property-identity-types open import foundation-core.contractible-maps open import foundation-core.dependent-pair-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.functoriality-dependent-function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.truncated-types open import foundation-core.truncation-levels open import foundation-core.universe-levels
Properties
A map f : A → B is a k+1-truncation if and only if it is surjective and ap f : (x ＝ y) → (f x ＝ f y) is a k-truncation for all x y : A
module _ {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 (succ-𝕋 k)) {f : A → type-Truncated-Type B} (H : is-surjective f) ( K : {l : Level} (x y : A) → is-truncation l (Id-Truncated-Type B (f x) (f y)) (ap f {x} {y})) where unique-extension-fib-is-truncation-is-truncation-ap : {l : Level} (C : Truncated-Type l (succ-𝕋 k)) (g : A → type-Truncated-Type C) (y : type-Truncated-Type B) → is-contr ( Σ ( type-Truncated-Type C) ( λ z → (t : fib f y) → Id (g (pr1 t)) z)) unique-extension-fib-is-truncation-is-truncation-ap C g = apply-dependent-universal-property-surj-is-surjective f H ( λ y → is-contr-Prop _) ( λ x → is-contr-equiv ( Σ (type-Truncated-Type C) (λ z → g x ＝ z)) ( equiv-tot ( λ z → ( ( equiv-ev-refl' x) ∘e ( equiv-map-Π ( λ x' → equiv-is-truncation ( Id-Truncated-Type B (f x') (f x)) ( ap f) ( K x' x) ( Id-Truncated-Type C (g x') z)))) ∘e ( equiv-ev-pair))) ( is-contr-total-path (g x))) is-truncation-is-truncation-ap : {l : Level} → is-truncation l B f is-truncation-is-truncation-ap C = is-equiv-is-contr-map ( λ g → is-contr-equiv' ( (y : type-Truncated-Type B) → Σ ( type-Truncated-Type C) ( λ z → (t : fib f y) → (g (pr1 t) ＝ z))) ( ( equiv-tot ( λ h → ( ( ( inv-equiv (equiv-funext)) ∘e ( equiv-map-Π ( λ x → equiv-inv (g x) (h (f x)) ∘e equiv-ev-refl (f x)))) ∘e ( equiv-swap-Π)) ∘e ( equiv-map-Π (λ x → equiv-ev-pair)))) ∘e ( distributive-Π-Σ)) ( is-contr-Π ( unique-extension-fib-is-truncation-is-truncation-ap C g))) module _ {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 (succ-𝕋 k)) {f : A → type-Truncated-Type B} where is-surjective-is-truncation : ({l : Level} → is-truncation l B f) → is-surjective f is-surjective-is-truncation H = map-inv-is-equiv ( dependent-universal-property-truncation-is-truncation B f H ( λ y → truncated-type-trunc-Prop k (fib f y))) ( λ x → unit-trunc-Prop (pair x refl))
Corollary 18.5.4
{- reflecting-map-mere-eq-unit-trunc-Set : {l : Level} (A : UU l) → reflecting-map-Eq-Rel (mere-eq-Eq-Rel A) (type-trunc-Set A) reflecting-map-mere-eq-unit-trunc-Set A = pair unit-trunc-Set (reflects-mere-eq (trunc-Set A) unit-trunc-Set) abstract is-set-quotient-trunc-Set : {l1 l2 : Level} (A : UU l1) → is-set-quotient l2 ( mere-eq-Eq-Rel A) ( trunc-Set A) ( reflecting-map-mere-eq-unit-trunc-Set A) is-set-quotient-trunc-Set A = is-set-quotient-is-set-truncation ( trunc-Set A) ( unit-trunc-Set) ( λ {l} → is-set-truncation-trunc-Set A) abstract is-surjective-and-effective-unit-trunc-Set : {l1 : Level} (A : UU l1) → is-surjective-and-effective (mere-eq-Eq-Rel A) unit-trunc-Set is-surjective-and-effective-unit-trunc-Set A = is-surjective-and-effective-is-set-quotient ( mere-eq-Eq-Rel A) ( trunc-Set A) ( unit-trunc-Set) ( reflects-mere-eq (trunc-Set A) unit-trunc-Set) ( λ {l} → is-set-quotient-trunc-Set A) abstract is-surjective-unit-trunc-Set : {l1 : Level} (A : UU l1) → is-surjective (unit-trunc-Set {A = A}) is-surjective-unit-trunc-Set A = pr1 (is-surjective-and-effective-unit-trunc-Set A) abstract is-effective-unit-trunc-Set : {l1 : Level} (A : UU l1) → is-effective (mere-eq-Eq-Rel A) (unit-trunc-Set {A = A}) is-effective-unit-trunc-Set A = pr2 (is-surjective-and-effective-unit-trunc-Set A) abstract apply-effectiveness-unit-trunc-Set : {l1 : Level} {A : UU l1} {x y : A} → Id (unit-trunc-Set x) (unit-trunc-Set y) → mere-eq x y apply-effectiveness-unit-trunc-Set {A = A} {x} {y} = map-equiv (is-effective-unit-trunc-Set A x y) abstract apply-effectiveness-unit-trunc-Set' : {l1 : Level} {A : UU l1} {x y : A} → mere-eq x y → Id (unit-trunc-Set x) (unit-trunc-Set y) apply-effectiveness-unit-trunc-Set' {A = A} {x} {y} = map-inv-equiv (is-effective-unit-trunc-Set A x y) emb-trunc-Set : {l1 : Level} (A : UU l1) → type-trunc-Set A ↪ (A → Prop l1) emb-trunc-Set A = emb-is-surjective-and-effective ( mere-eq-Eq-Rel A) ( trunc-Set A) ( unit-trunc-Set) ( is-surjective-and-effective-unit-trunc-Set A) hom-slice-trunc-Set : {l1 : Level} (A : UU l1) → hom-slice (mere-eq-Prop {A = A}) (map-emb (emb-trunc-Set A)) hom-slice-trunc-Set A = pair ( unit-trunc-Set) ( triangle-emb-is-surjective-and-effective ( mere-eq-Eq-Rel A) ( trunc-Set A) ( unit-trunc-Set) ( is-surjective-and-effective-unit-trunc-Set A)) abstract is-image-trunc-Set : {l1 l2 : Level} (A : UU l1) → is-image l2 ( mere-eq-Prop {A = A}) ( emb-trunc-Set A) ( hom-slice-trunc-Set A) is-image-trunc-Set A = is-image-is-surjective-and-effective ( mere-eq-Eq-Rel A) ( trunc-Set A) ( unit-trunc-Set) ( is-surjective-and-effective-unit-trunc-Set A) -}
Uniqueness of trunc-Set
{- module _ {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) {h : type-hom-Set B (trunc-Set A)} (H : (h ∘ f) ~ unit-trunc-Set) where abstract is-equiv-is-set-truncation' : ({l : Level} → is-set-truncation l B f) → is-equiv h is-equiv-is-set-truncation' Sf = is-equiv-is-set-truncation-is-set-truncation ( B) ( f) ( trunc-Set A) ( unit-trunc-Set) ( H) ( Sf) ( λ {h} → is-set-truncation-trunc-Set A) abstract is-set-truncation-is-equiv' : is-equiv h → ({l : Level} → is-set-truncation l B f) is-set-truncation-is-equiv' Eh = is-set-truncation-is-equiv-is-set-truncation ( B) ( f) ( trunc-Set A) ( unit-trunc-Set) ( H) ( λ {l} → is-set-truncation-trunc-Set A) ( Eh) module _ {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) {h : type-hom-Set (trunc-Set A) B} (H : (h ∘ unit-trunc-Set) ~ f) where abstract is-equiv-is-set-truncation : ({l : Level} → is-set-truncation l B f) → is-equiv h is-equiv-is-set-truncation Sf = is-equiv-is-set-truncation-is-set-truncation ( trunc-Set A) ( unit-trunc-Set) ( B) ( f) ( H) ( λ {l} → is-set-truncation-trunc-Set A) ( Sf) abstract is-set-truncation-is-equiv : is-equiv h → ({l : Level} → is-set-truncation l B f) is-set-truncation-is-equiv Eh = is-set-truncation-is-set-truncation-is-equiv ( trunc-Set A) ( unit-trunc-Set) ( B) ( f) ( H) ( Eh) ( λ {l} → is-set-truncation-trunc-Set A) abstract is-equiv-unit-trunc-Set : {l : Level} (A : Set l) → is-equiv (unit-trunc-Set {A = type-Set A}) is-equiv-unit-trunc-Set A = is-equiv-is-set-truncation' A id refl-htpy ( is-set-truncation-id (is-set-type-Set A)) equiv-unit-trunc-Set : {l : Level} (A : Set l) → type-Set A ≃ type-trunc-Set (type-Set A) equiv-unit-trunc-Set A = pair unit-trunc-Set (is-equiv-unit-trunc-Set A) equiv-unit-trunc-empty-Set : empty ≃ type-trunc-Set empty equiv-unit-trunc-empty-Set = equiv-unit-trunc-Set empty-Set abstract is-empty-trunc-Set : {l : Level} {A : UU l} → is-empty A → is-empty (type-trunc-Set A) is-empty-trunc-Set f x = apply-universal-property-trunc-Set x empty-Set f abstract is-empty-is-empty-trunc-Set : {l : Level} {A : UU l} → is-empty (type-trunc-Set A) → is-empty A is-empty-is-empty-trunc-Set f = f ∘ unit-trunc-Set equiv-unit-trunc-unit-Set : unit ≃ type-trunc-Set unit equiv-unit-trunc-unit-Set = equiv-unit-trunc-Set unit-Set equiv-unit-trunc-ℕ-Set : ℕ ≃ type-trunc-Set ℕ equiv-unit-trunc-ℕ-Set = equiv-unit-trunc-Set ℕ-Set equiv-unit-trunc-ℤ-Set : ℤ ≃ type-trunc-Set ℤ equiv-unit-trunc-ℤ-Set = equiv-unit-trunc-Set ℤ-Set equiv-unit-trunc-Fin-Set : (k : ℕ) → Fin k ≃ type-trunc-Set (Fin k) equiv-unit-trunc-Fin-Set k = equiv-unit-trunc-Set (Fin-Set k) abstract is-contr-trunc-Set : {l : Level} {A : UU l} → is-contr A → is-contr (type-trunc-Set A) is-contr-trunc-Set {l} {A} H = is-contr-equiv' ( A) ( equiv-unit-trunc-Set (pair A (is-set-is-contr H))) ( H) module _ {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) (Sf : {l : Level} → is-set-truncation l B f) where abstract uniqueness-trunc-Set : is-contr ( Σ (type-trunc-Set A ≃ type-Set B) ( λ e → (map-equiv e ∘ unit-trunc-Set) ~ f)) uniqueness-trunc-Set = uniqueness-set-truncation (trunc-Set A) unit-trunc-Set B f ( λ {l} → is-set-truncation-trunc-Set A) ( Sf) equiv-uniqueness-trunc-Set : type-trunc-Set A ≃ type-Set B equiv-uniqueness-trunc-Set = pr1 (center uniqueness-trunc-Set) map-equiv-uniqueness-trunc-Set : type-trunc-Set A → type-Set B map-equiv-uniqueness-trunc-Set = map-equiv equiv-uniqueness-trunc-Set triangle-uniqueness-trunc-Set : (map-equiv-uniqueness-trunc-Set ∘ unit-trunc-Set) ~ f triangle-uniqueness-trunc-Set = pr2 (center uniqueness-trunc-Set) module _ {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) (Sf : {l : Level} → is-set-truncation l B f) where abstract uniqueness-trunc-Set' : is-contr ( Σ ( type-Set B ≃ type-trunc-Set A) ( λ e → (map-equiv e ∘ f) ~ unit-trunc-Set)) uniqueness-trunc-Set' = uniqueness-set-truncation B f (trunc-Set A) unit-trunc-Set Sf ( λ {l} → is-set-truncation-trunc-Set A) equiv-uniqueness-trunc-Set' : type-Set B ≃ type-trunc-Set A equiv-uniqueness-trunc-Set' = pr1 (center uniqueness-trunc-Set') map-equiv-uniqueness-trunc-Set' : type-Set B → type-trunc-Set A map-equiv-uniqueness-trunc-Set' = map-equiv equiv-uniqueness-trunc-Set' triangle-uniqueness-trunc-Set' : (map-equiv-uniqueness-trunc-Set' ∘ f) ~ unit-trunc-Set triangle-uniqueness-trunc-Set' = pr2 (center uniqueness-trunc-Set') -}
Proposition 18.5.5
{- module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) where abstract unique-map-trunc-Set : is-contr ( Σ ( type-trunc-Set A → type-trunc-Set B) ( λ h → (h ∘ unit-trunc-Set) ~ (unit-trunc-Set ∘ f))) unique-map-trunc-Set = universal-property-trunc-Set A (trunc-Set B) (unit-trunc-Set ∘ f) map-trunc-Set : type-trunc-Set A → type-trunc-Set B map-trunc-Set = pr1 (center unique-map-trunc-Set) naturality-trunc-Set : (map-trunc-Set ∘ unit-trunc-Set) ~ (unit-trunc-Set ∘ f) naturality-trunc-Set = pr2 (center unique-map-trunc-Set) htpy-map-trunc-Set : (h : type-trunc-Set A → type-trunc-Set B) → (H : (h ∘ unit-trunc-Set) ~ (unit-trunc-Set ∘ f)) → map-trunc-Set ~ h htpy-map-trunc-Set h H = htpy-eq ( ap pr1 ( eq-is-contr unique-map-trunc-Set { pair map-trunc-Set naturality-trunc-Set} { pair h H})) map-id-trunc-Set : {l1 : Level} {A : UU l1} → map-trunc-Set (id {A = A}) ~ id map-id-trunc-Set {l1} {A} = htpy-eq ( ap pr1 ( eq-is-contr ( universal-property-trunc-Set A (trunc-Set A) unit-trunc-Set) { pair (map-trunc-Set id) (naturality-trunc-Set id)} { pair id refl-htpy})) map-comp-trunc-Set : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (g : B → C) (f : A → B) → map-trunc-Set (g ∘ f) ~ (map-trunc-Set g ∘ map-trunc-Set f) map-comp-trunc-Set {A = A} {C = C} g f = htpy-eq ( ap pr1 ( eq-is-contr ( universal-property-trunc-Set A (trunc-Set C) (unit-trunc-Set ∘ (g ∘ f))) { pair (map-trunc-Set (g ∘ f)) (naturality-trunc-Set (g ∘ f))} { pair ( map-trunc-Set g ∘ map-trunc-Set f) ( ( map-trunc-Set g ·l naturality-trunc-Set f) ∙h ( naturality-trunc-Set g ·r f))})) htpy-trunc-Set : {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} → (f ~ g) → (map-trunc-Set f ~ map-trunc-Set g) htpy-trunc-Set {B = B} {f = f} {g} H = map-inv-is-equiv ( dependent-universal-property-trunc-Set ( λ x → set-Prop ( Id-Prop (trunc-Set B) (map-trunc-Set f x) (map-trunc-Set g x)))) ( λ a → ( naturality-trunc-Set f a) ∙ ( ( ap unit-trunc-Set (H a)) ∙ ( inv (naturality-trunc-Set g a)))) abstract is-equiv-map-trunc-Set : {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → is-equiv f → is-equiv (map-trunc-Set f) is-equiv-map-trunc-Set {f = f} H = pair ( pair ( map-trunc-Set (pr1 (pr1 H))) ( ( inv-htpy (map-comp-trunc-Set f (pr1 (pr1 H)))) ∙h ( ( htpy-trunc-Set (pr2 (pr1 H))) ∙h ( map-id-trunc-Set)))) ( pair ( map-trunc-Set (pr1 (pr2 H))) ( ( inv-htpy (map-comp-trunc-Set (pr1 (pr2 H)) f)) ∙h ( ( htpy-trunc-Set (pr2 (pr2 H))) ∙h ( map-id-trunc-Set)))) equiv-trunc-Set : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A ≃ B) → (type-trunc-Set A ≃ type-trunc-Set B) equiv-trunc-Set e = pair ( map-trunc-Set (map-equiv e)) ( is-equiv-map-trunc-Set (is-equiv-map-equiv e)) map-equiv-trunc-Set : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A ≃ B) → type-trunc-Set A → type-trunc-Set B map-equiv-trunc-Set e = map-equiv (equiv-trunc-Set e) -}
{- module _ {l1 l2 : Level} (A : UU l1) (B : UU l2) where abstract distributive-trunc-coprod-Set : is-contr ( Σ ( type-equiv-Set ( trunc-Set (coprod A B)) ( coprod-Set (trunc-Set A) (trunc-Set B))) ( λ e → ( map-equiv e ∘ unit-trunc-Set) ~ ( map-coprod unit-trunc-Set unit-trunc-Set))) distributive-trunc-coprod-Set = uniqueness-trunc-Set ( coprod-Set (trunc-Set A) (trunc-Set B)) ( map-coprod unit-trunc-Set unit-trunc-Set) ( λ {l} C → is-equiv-right-factor ( ev-inl-inr (λ x → type-Set C)) ( precomp-Set (map-coprod unit-trunc-Set unit-trunc-Set) C) ( universal-property-coprod (type-Set C)) ( is-equiv-comp ( map-prod ( precomp-Set unit-trunc-Set C) ( precomp-Set unit-trunc-Set C)) ( ev-inl-inr (λ x → type-Set C)) ( universal-property-coprod (type-Set C)) ( is-equiv-map-prod ( precomp-Set unit-trunc-Set C) ( precomp-Set unit-trunc-Set C) ( is-set-truncation-trunc-Set A C) ( is-set-truncation-trunc-Set B C)))) equiv-distributive-trunc-coprod-Set : type-equiv-Set ( trunc-Set (coprod A B)) ( coprod-Set (trunc-Set A) (trunc-Set B)) equiv-distributive-trunc-coprod-Set = pr1 (center distributive-trunc-coprod-Set) map-equiv-distributive-trunc-coprod-Set : type-hom-Set ( trunc-Set (coprod A B)) ( coprod-Set (trunc-Set A) (trunc-Set B)) map-equiv-distributive-trunc-coprod-Set = map-equiv equiv-distributive-trunc-coprod-Set triangle-distributive-trunc-coprod-Set : ( map-equiv-distributive-trunc-coprod-Set ∘ unit-trunc-Set) ~ ( map-coprod unit-trunc-Set unit-trunc-Set) triangle-distributive-trunc-coprod-Set = pr2 (center distributive-trunc-coprod-Set) -}
Set truncations of Σ-types
{- module _ {l1 l2 : Level} (A : UU l1) (B : A → UU l2) where abstract trunc-Σ-Set : is-contr ( Σ ( type-trunc-Set (Σ A B) ≃ type-trunc-Set (Σ A (λ x → type-trunc-Set (B x)))) ( λ e → ( map-equiv e ∘ unit-trunc-Set) ~ ( unit-trunc-Set ∘ tot (λ x → unit-trunc-Set)))) trunc-Σ-Set = uniqueness-trunc-Set ( trunc-Set (Σ A (λ x → type-trunc-Set (B x)))) ( unit-trunc-Set ∘ tot (λ x → unit-trunc-Set)) ( λ {l} C → is-equiv-right-factor ( ev-pair) ( precomp-Set (unit-trunc-Set ∘ tot (λ x → unit-trunc-Set)) C) ( is-equiv-ev-pair) ( is-equiv-htpy-equiv ( ( equiv-map-Π ( λ x → equiv-universal-property-trunc-Set (B x) C)) ∘e ( ( equiv-ev-pair) ∘e ( equiv-universal-property-trunc-Set ( Σ A (type-trunc-Set ∘ B)) C))) ( refl-htpy))) equiv-trunc-Σ-Set : type-trunc-Set (Σ A B) ≃ type-trunc-Set (Σ A (λ x → type-trunc-Set (B x))) equiv-trunc-Σ-Set = pr1 (center trunc-Σ-Set) map-equiv-trunc-Σ-Set : type-trunc-Set (Σ A B) → type-trunc-Set (Σ A (λ x → type-trunc-Set (B x))) map-equiv-trunc-Σ-Set = map-equiv equiv-trunc-Σ-Set square-trunc-Σ-Set : ( map-equiv-trunc-Σ-Set ∘ unit-trunc-Set) ~ ( unit-trunc-Set ∘ tot (λ x → unit-trunc-Set)) square-trunc-Σ-Set = pr2 (center trunc-Σ-Set) htpy-map-equiv-trunc-Σ-Set : map-trunc-Set (tot (λ x → unit-trunc-Set)) ~ map-equiv-trunc-Σ-Set htpy-map-equiv-trunc-Σ-Set = htpy-map-trunc-Set ( tot (λ x → unit-trunc-Set)) ( map-equiv-trunc-Σ-Set) ( square-trunc-Σ-Set) abstract is-equiv-map-trunc-tot-unit-trunc-Set : is-equiv (map-trunc-Set (tot (λ (x : A) → unit-trunc-Set {A = B x}))) is-equiv-map-trunc-tot-unit-trunc-Set = is-equiv-htpy-equiv ( equiv-trunc-Σ-Set) ( htpy-map-equiv-trunc-Σ-Set) -}
trunc-Set distributes over products
{- module _ {l1 l2 : Level} (A : UU l1) (B : UU l2) where abstract distributive-trunc-prod-Set : is-contr ( Σ ( type-trunc-Set (A × B) ≃ ( type-trunc-Set A × type-trunc-Set B)) ( λ e → ( map-equiv e ∘ unit-trunc-Set) ~ ( map-prod unit-trunc-Set unit-trunc-Set))) distributive-trunc-prod-Set = uniqueness-trunc-Set ( prod-Set (trunc-Set A) (trunc-Set B)) ( map-prod unit-trunc-Set unit-trunc-Set) ( λ {l} C → is-equiv-right-factor ( ev-pair) ( precomp-Set (map-prod unit-trunc-Set unit-trunc-Set) C) ( is-equiv-ev-pair) ( is-equiv-htpy-equiv ( ( equiv-universal-property-trunc-Set A (Π-Set' B (λ y → C))) ∘e ( ( equiv-postcomp ( type-trunc-Set A) (equiv-universal-property-trunc-Set B C)) ∘e ( equiv-ev-pair))) ( refl-htpy))) equiv-distributive-trunc-prod-Set : type-trunc-Set (A × B) ≃ ( type-trunc-Set A × type-trunc-Set B) equiv-distributive-trunc-prod-Set = pr1 (center distributive-trunc-prod-Set) map-equiv-distributive-trunc-prod-Set : type-trunc-Set (A × B) → type-trunc-Set A × type-trunc-Set B map-equiv-distributive-trunc-prod-Set = map-equiv equiv-distributive-trunc-prod-Set triangle-distributive-trunc-prod-Set : ( map-equiv-distributive-trunc-prod-Set ∘ unit-trunc-Set) ~ ( map-prod unit-trunc-Set unit-trunc-Set) triangle-distributive-trunc-prod-Set = pr2 (center distributive-trunc-prod-Set) -}
trunc-Set distributes over Π-types 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-htpy-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)) ( refl-htpy))) ( 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-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) -}