Iterated cartesian product types

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.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-function-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-core.cartesian-product-types
open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.functions
open import foundation-core.identity-types
open import foundation-core.type-arithmetic-cartesian-product-types
open import foundation-core.universe-levels

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))
          ( isretr-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)