Iterated cartesian product types
Content created by Fredrik Bakke, Victor Blanchi and Egbert Rijke.
Created on 2023-05-10.
Last modified on 2024-02-06.
module foundation.iterated-cartesian-product-types where
Imports
open import elementary-number-theory.natural-numbers open import finite-group-theory.permutations-standard-finite-types open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-function-types open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-function-types open import foundation.unit-type open import foundation.univalence open import foundation.universal-property-coproduct-types open import foundation.universal-property-empty-type open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.contractible-types open import foundation-core.coproduct-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.identity-types open import lists.arrays open import lists.concatenation-lists open import lists.lists open import lists.permutation-lists open import univalent-combinatorics.standard-finite-types
Idea
In this file, we give three definitions of the iterated cartesian product
A₁ × ... × Aₙ
of n
types A₁ , ... , Aₙ
. Two use a family of types over
Fin n
: the first uses recursion over Fin n
and the second is just
Π (Fin n) A
. The last one uses lists.
We show that :
- all of these definitions are equivalent
- iterated cartesian product of types is closed under permutations
Definitions
Via a family of types over Fin n
Using recursion
iterated-product-Fin-recursive : {l : Level} (n : ℕ) → ((Fin n) → UU l) → UU l iterated-product-Fin-recursive {l} zero-ℕ A = raise-unit l iterated-product-Fin-recursive (succ-ℕ n) A = A (inr star) × iterated-product-Fin-recursive n (A ∘ inl)
Using Π
-types
iterated-product-Fin-Π : {l : Level} (n : ℕ) → ((Fin n) → UU l) → UU l iterated-product-Fin-Π n A = (i : Fin n) → A i
Via lists
iterated-product-lists : {l : Level} → list (UU l) → UU l iterated-product-lists {l} nil = raise-unit l iterated-product-lists (cons A p) = A × iterated-product-lists p
Properties
The definitions using recursion and Π
-types are equivalent
equiv-iterated-product-Fin-recursive-Π : {l : Level} (n : ℕ) (A : (Fin n → UU l)) → iterated-product-Fin-recursive n A ≃ iterated-product-Fin-Π n A equiv-iterated-product-Fin-recursive-Π zero-ℕ A = equiv-is-contr is-contr-raise-unit (dependent-universal-property-empty' A) equiv-iterated-product-Fin-recursive-Π (succ-ℕ n) A = ( ( inv-equiv (equiv-dependent-universal-property-coproduct A)) ∘e ( ( commutative-product) ∘e ( ( equiv-product ( inv-equiv (left-unit-law-Π-is-contr is-contr-unit star)) ( id-equiv)) ∘e ( ( equiv-product ( id-equiv) ( equiv-iterated-product-Fin-recursive-Π n (A ∘ inl)))))))
The definitions using recursion and lists are equivalent
equiv-iterated-product-Fin-recursive-lists : {l : Level} (l : list (UU l)) → iterated-product-Fin-recursive ( length-array (array-list l)) ( functional-vec-array (array-list l)) ≃ iterated-product-lists l equiv-iterated-product-Fin-recursive-lists nil = id-equiv equiv-iterated-product-Fin-recursive-lists (cons x l) = equiv-product id-equiv (equiv-iterated-product-Fin-recursive-lists l)
The cartesian product of two iterated cartesian products (via list) is the iterated cartesian product of the concatenation of the corresponding lists
equiv-product-iterated-product-lists : {l : Level} (p q : list (UU l)) → (iterated-product-lists p × iterated-product-lists q) ≃ iterated-product-lists (concat-list p q) equiv-product-iterated-product-lists nil q = left-unit-law-product-is-contr (is-contr-raise-unit) equiv-product-iterated-product-lists (cons x p) q = ( ( equiv-product ( id-equiv) ( equiv-product-iterated-product-lists p q)) ∘e ( associative-product ( x) ( iterated-product-lists p) ( iterated-product-lists q)))
Iterated cartesian product is closed under permutations
permutation-iterated-product-Fin-Π : {l : Level} (n : ℕ) (A : (Fin n → UU l)) (t : Permutation n) → UU l permutation-iterated-product-Fin-Π n A t = iterated-product-Fin-Π n (A ∘ map-equiv t) equiv-permutation-iterated-product-Fin-Π : {l : Level} (n : ℕ) (A : (Fin n → UU l)) (t : Permutation n) → permutation-iterated-product-Fin-Π n A t ≃ iterated-product-Fin-Π n A equiv-permutation-iterated-product-Fin-Π n A t = equiv-Π (λ z → A z) t (λ a → id-equiv) eq-permutation-iterated-product-Fin-Π : {l : Level} (n : ℕ) (A : (Fin n → UU l)) (t : Permutation n) → permutation-iterated-product-Fin-Π n A t = iterated-product-Fin-Π n A eq-permutation-iterated-product-Fin-Π n A t = eq-equiv (equiv-permutation-iterated-product-Fin-Π n A t) permutation-iterated-product-Fin-recursive : {l : Level} (n : ℕ) (A : (Fin n → UU l)) (t : Permutation n) → UU l permutation-iterated-product-Fin-recursive n A t = iterated-product-Fin-recursive n (A ∘ map-equiv t) equiv-permutation-iterated-product-Fin-recursive : {l : Level} (n : ℕ) (A : (Fin n → UU l)) (t : Permutation n) → permutation-iterated-product-Fin-recursive n A t ≃ iterated-product-Fin-recursive n A equiv-permutation-iterated-product-Fin-recursive n A t = ( inv-equiv (equiv-iterated-product-Fin-recursive-Π n A)) ∘e ( equiv-permutation-iterated-product-Fin-Π n A t) ∘e ( equiv-iterated-product-Fin-recursive-Π n (A ∘ map-equiv t)) eq-permutation-iterated-product-Fin-recursive : {l : Level} (n : ℕ) (A : (Fin n → UU l)) (t : Permutation n) → permutation-iterated-product-Fin-recursive n A t = iterated-product-Fin-recursive n A eq-permutation-iterated-product-Fin-recursive n A t = eq-equiv (equiv-permutation-iterated-product-Fin-recursive n A t) permutation-iterated-product-lists : {l : Level} (L : list (UU l)) (t : Permutation (length-list L)) → UU l permutation-iterated-product-lists L t = iterated-product-lists (permute-list L t) equiv-permutation-iterated-product-lists : {l : Level} (L : list (UU l)) (t : Permutation (length-list L)) → permutation-iterated-product-lists L t ≃ iterated-product-lists L equiv-permutation-iterated-product-lists L t = ( equiv-iterated-product-Fin-recursive-lists L ∘e ( ( equiv-permutation-iterated-product-Fin-recursive ( length-list L) ( functional-vec-array (array-list L)) ( t)) ∘e ( equiv-eq ( ap ( λ p → iterated-product-Fin-recursive ( length-array p) ( functional-vec-array p)) ( is-retraction-array-list ( length-list L , ( functional-vec-array (array-list L) ∘ map-equiv t)))) ∘e ( inv-equiv ( equiv-iterated-product-Fin-recursive-lists (permute-list L t)))))) eq-permutation-iterated-product-lists : {l : Level} (L : list (UU l)) (t : Permutation (length-list L)) → permutation-iterated-product-lists L t = iterated-product-lists L eq-permutation-iterated-product-lists L t = eq-equiv (equiv-permutation-iterated-product-lists L t)
Recent changes
- 2024-02-06. Fredrik Bakke. Rename
(co)prod
to(co)product
(#1017). - 2024-01-12. Fredrik Bakke. Make type arguments implicit for
eq-equiv
(#998). - 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).