# Iterated cartesian product types

Content created by Fredrik Bakke, Victor Blanchi and Egbert Rijke.

Created on 2023-05-10.

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-coprod A)) ∘e
( ( commutative-prod) ∘e
( ( equiv-prod
( inv-equiv (left-unit-law-Π-is-contr is-contr-unit star))
( id-equiv)) ∘e
( ( equiv-prod
( 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-prod 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-prod-is-contr (is-contr-raise-unit)
equiv-product-iterated-product-lists (cons x p) q =
( ( equiv-prod
( id-equiv)
( equiv-product-iterated-product-lists p q)) ∘e
( associative-prod 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
( permutation-iterated-product-Fin-Π n A t)
( iterated-product-Fin-Π n A)
( 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
( permutation-iterated-product-Fin-recursive n A t)
( iterated-product-Fin-recursive n A)
( 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
( permutation-iterated-product-lists L t)
( iterated-product-lists L)
( equiv-permutation-iterated-product-lists L t)