Iterated cartesian product is closed by permutation (#617)

I have shown that the 3 definitions of iterated cartesian product of
types is closed by permutation.

Author: VictorBlanchi

src/foundation/iterated-cartesian-product-types.lagda.md

@@ -9,21 +9,30 @@ module foundation.iterated-cartesian-product-types where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import finite-group-theory.permutations-standard-finite-types
+
 open import foundation.cartesian-product-types
 open import foundation.contractible-types
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
 open import foundation.functions
 open import foundation.functoriality-cartesian-product-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.identity-types
+open import foundation.propositions
 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 lists.arrays
 open import lists.lists
+open import lists.permutation-lists
 
 open import univalent-combinatorics.standard-finite-types
 ```
@@ -35,8 +44,12 @@ open import univalent-combinatorics.standard-finite-types
 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 also show that the first two
-definitions are equivalent.
+`Π (Fin n) A`. The last one uses lists.
+
+We show that :
+
+- all these definitions are equivalent
+- iterated cartesian product of types is closed under permutations
 
 ## Definitions
 
@@ -53,7 +66,7 @@ iterated-product-Fin-recursive (succ-ℕ n) A =
   A (inr star) × iterated-product-Fin-recursive n (A ∘ inl)
 ```
 
-#### Using `Π` type
+#### Using `Π`-types
 
 ```agda
 iterated-product-Fin-Π :
@@ -71,9 +84,9 @@ iterated-product-lists {l} nil = raise-unit l
 iterated-product-lists (cons A p) = A × iterated-product-lists p
 ```
 
-## Property
+## Properties
 
-### Equivalence between the first two definitions
+### The definitions using recursion and `Π`-types are equivalent
 
 ```agda
 equiv-iterated-product-Fin-recursive-Π :
@@ -92,3 +105,102 @@ equiv-iterated-product-Fin-recursive-Π (succ-ℕ n) A =
               ( id-equiv)
               ( equiv-iterated-product-Fin-recursive-Π n (A ∘ inl)))))))
 ```
+
+### The definitions using recursion and lists are equivalent
+
+```agda
+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)
+```
+
+### Iterated cartesian product is closed under permutations
+
+```agda
+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)
+```

src/lists/arrays.lagda.md

@@ -153,3 +153,21 @@ module _
       isretr-array-list
       issec-array-list
 ```
+
+### Computational rules of the equivalence between arrays and lists
+
+```agda
+  compute-length-list-list-vec :
+    (n : ℕ) (v : vec A n) →
+    length-list (list-vec n v) ＝ n
+  compute-length-list-list-vec zero-ℕ v = refl
+  compute-length-list-list-vec (succ-ℕ n) (x ∷ v) =
+    ap succ-ℕ (compute-length-list-list-vec n v)
+
+  compute-length-list-list-array :
+    (t : array A) → length-list (list-array t) ＝ length-array t
+  compute-length-list-list-array t =
+    compute-length-list-list-vec
+      ( length-array t)
+      ( listed-vec-functional-vec (length-array t) (functional-vec-array t))
+```

src/lists/permutation-lists.lagda.md

@@ -41,6 +41,6 @@ module _
   permute-list : (l : list A) → Permutation (length-list l) → list A
   permute-list l s =
     list-array
-      ( pr1 (array-list l) ,
-        pr2 (array-list l) ∘ (map-equiv s))
+      ( length-array (array-list l) ,
+        functional-vec-array (array-list l) ∘ (map-equiv s))
 ```