Iterating families of maps over a map

src/elementary-number-theory/finitely-cyclic-maps.lagda.md

@@ -58,7 +58,10 @@ module _
     (f : X → X) (H : is-finitely-cyclic-map f) →
     (f ∘ map-inv-is-finitely-cyclic-map f H) ~ id
   is-section-map-inv-is-finitely-cyclic-map f H x =
-    ( iterate-succ-ℕ (length-path-is-finitely-cyclic-map H (f x) x) f x) ∙
+    ( reassociate-iterate-succ-ℕ
+      ( length-path-is-finitely-cyclic-map H (f x) x)
+      ( f)
+      ( x)) ∙
     ( eq-is-finitely-cyclic-map H (f x) x)
 
   is-retraction-map-inv-is-finitely-cyclic-map :
@@ -70,7 +73,7 @@ module _
       ( inv (eq-is-finitely-cyclic-map H (f x) x))) ∙
     ( ( ap
         ( iterate (length-path-is-finitely-cyclic-map H (f (f x)) (f x)) f)
-          ( iterate-succ-ℕ
+          ( reassociate-iterate-succ-ℕ
             ( length-path-is-finitely-cyclic-map H (f x) x) f (f x))) ∙
       ( ( iterate-iterate
           ( length-path-is-finitely-cyclic-map H (f (f x)) (f x))

src/foundation.lagda.md

@@ -241,6 +241,7 @@ open import foundation.iterated-cartesian-product-types public
 open import foundation.iterated-dependent-pair-types public
 open import foundation.iterated-dependent-product-types public
 open import foundation.iterating-automorphisms public
+open import foundation.iterating-families-of-maps public
 open import foundation.iterating-functions public
 open import foundation.iterating-involutions public
 open import foundation.kernel-span-diagrams-of-maps public

src/foundation/dependent-inverse-sequential-diagrams.lagda.md

@@ -11,6 +11,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.inverse-sequential-diagrams
+open import foundation.iterating-families-of-maps
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -114,18 +115,18 @@ module _
   naturality-section-dependent-inverse-sequential-diagram :
     (h :
       (n : ℕ) (x : family-inverse-sequential-diagram A n) →
-      family-dependent-inverse-sequential-diagram B n x)
-    (n : ℕ) → UU (l1 ⊔ l2)
-  naturality-section-dependent-inverse-sequential-diagram h n =
+      family-dependent-inverse-sequential-diagram B n x) →
+    UU (l1 ⊔ l2)
+  naturality-section-dependent-inverse-sequential-diagram h =
+    ( n : ℕ) →
     h n ∘ map-inverse-sequential-diagram A n ~
     map-dependent-inverse-sequential-diagram B n _ ∘ h (succ-ℕ n)
 
   section-dependent-inverse-sequential-diagram : UU (l1 ⊔ l2)
   section-dependent-inverse-sequential-diagram =
     Σ ( (n : ℕ) (x : family-inverse-sequential-diagram A n) →
         family-dependent-inverse-sequential-diagram B n x)
-      ( λ h → (n : ℕ) →
-        naturality-section-dependent-inverse-sequential-diagram h n)
+      ( naturality-section-dependent-inverse-sequential-diagram)
 
   map-section-dependent-inverse-sequential-diagram :
     section-dependent-inverse-sequential-diagram →
@@ -134,10 +135,9 @@ module _
   map-section-dependent-inverse-sequential-diagram = pr1
 
   naturality-map-section-dependent-inverse-sequential-diagram :
-    (f : section-dependent-inverse-sequential-diagram) (n : ℕ) →
+    (f : section-dependent-inverse-sequential-diagram) →
     naturality-section-dependent-inverse-sequential-diagram
       ( map-section-dependent-inverse-sequential-diagram f)
-      ( n)
   naturality-map-section-dependent-inverse-sequential-diagram = pr2
 ```
 
@@ -158,6 +158,17 @@ pr1 (right-shift-dependent-inverse-sequential-diagram B) n =
   family-dependent-inverse-sequential-diagram B (succ-ℕ n)
 pr2 (right-shift-dependent-inverse-sequential-diagram B) n =
   map-dependent-inverse-sequential-diagram B (succ-ℕ n)
+
+iterated-right-shift-dependent-inverse-sequential-diagram :
+  {l1 l2 : Level} (n : ℕ) →
+  (A : inverse-sequential-diagram l1) →
+  dependent-inverse-sequential-diagram l2 A →
+  dependent-inverse-sequential-diagram l2
+    ( iterated-right-shift-inverse-sequential-diagram n A)
+iterated-right-shift-dependent-inverse-sequential-diagram n A =
+  iterate-family-of-maps n
+    ( λ A → right-shift-dependent-inverse-sequential-diagram {A = A})
+    ( A)
 ```
 
 ### Left shifting a dependent inverse sequential diagram
@@ -179,6 +190,17 @@ pr2 (left-shift-dependent-inverse-sequential-diagram B) 0 x =
   raise-terminal-map (family-dependent-inverse-sequential-diagram B 0 x)
 pr2 (left-shift-dependent-inverse-sequential-diagram B) (succ-ℕ n) =
   map-dependent-inverse-sequential-diagram B n
+
+iterated-left-shift-dependent-inverse-sequential-diagram :
+  {l1 l2 : Level} (n : ℕ) →
+  (A : inverse-sequential-diagram l1) →
+  dependent-inverse-sequential-diagram l2 A →
+  dependent-inverse-sequential-diagram l2
+    ( iterated-left-shift-inverse-sequential-diagram n A)
+iterated-left-shift-dependent-inverse-sequential-diagram n A =
+  iterate-family-of-maps n
+    ( λ A → left-shift-dependent-inverse-sequential-diagram {A = A})
+    ( A)
 ```
 
 ## Table of files about sequential limits

src/foundation/equivalences-inverse-sequential-diagrams.lagda.md

@@ -9,6 +9,7 @@ module foundation.equivalences-inverse-sequential-diagrams where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.binary-homotopies
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-function-types
 open import foundation.fundamental-theorem-of-identity-types
@@ -56,8 +57,7 @@ equiv-inverse-sequential-diagram A B =
   Σ ( (n : ℕ) →
       family-inverse-sequential-diagram A n ≃
       family-inverse-sequential-diagram B n)
-    ( λ e →
-      (n : ℕ) → naturality-hom-inverse-sequential-diagram A B (map-equiv ∘ e) n)
+    ( λ e → naturality-hom-inverse-sequential-diagram A B (map-equiv ∘ e))
 
 hom-equiv-inverse-sequential-diagram :
   {l1 l2 : Level}
@@ -94,8 +94,7 @@ is-torsorial-equiv-inverse-sequential-diagram A =
     ( is-torsorial-Eq-Π
       ( λ n → is-torsorial-equiv (family-inverse-sequential-diagram A n)))
     ( family-inverse-sequential-diagram A , λ n → id-equiv)
-    ( is-torsorial-Eq-Π
-      ( λ n → is-torsorial-htpy (map-inverse-sequential-diagram A n)))
+    ( is-torsorial-binary-htpy (map-inverse-sequential-diagram A))
 
 is-equiv-equiv-eq-inverse-sequential-diagram :
   {l : Level} (A B : inverse-sequential-diagram l) →

src/foundation/inverse-sequential-diagrams.lagda.md

@@ -79,8 +79,7 @@ pr2 (right-shift-inverse-sequential-diagram A) n =
   map-inverse-sequential-diagram A (succ-ℕ n)
 
 iterated-right-shift-inverse-sequential-diagram :
-  {l : Level} (n : ℕ) →
-  inverse-sequential-diagram l → inverse-sequential-diagram l
+  {l : Level} → ℕ → inverse-sequential-diagram l → inverse-sequential-diagram l
 iterated-right-shift-inverse-sequential-diagram n =
   iterate n right-shift-inverse-sequential-diagram
 ```

src/foundation/iterating-families-of-maps.lagda.md

@@ -0,0 +1,116 @@
+# Iterating families of maps over a map
+
+```agda
+module foundation.iterating-families-of-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.exponentiation-natural-numbers
+open import elementary-number-theory.multiplication-natural-numbers
+open import elementary-number-theory.multiplicative-monoid-of-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-higher-identifications-functions
+open import foundation.action-on-identifications-dependent-functions
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-homotopies
+open import foundation.dependent-identifications
+open import foundation.dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.iterating-functions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import foundation-core.commuting-squares-of-maps
+open import foundation-core.endomorphisms
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.sets
+
+open import group-theory.monoid-actions
+```
+
+</details>
+
+## Idea
+
+Given a family of maps `g : (x : X) → C x → C (f x)` over a map `f : X → X`,
+then `g` can be
+{{#concept "iterated" Disambiguation="family of maps over a map of types" Agda=iterate-family-of-maps}}
+by repeatedly applying `g`.
+
+## Definition
+
+### Iterating dependent functions
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} {C : X → UU l2} {f : X → X}
+  where
+
+  iterate-family-of-maps :
+    (k : ℕ) → ((x : X) → C x → C (f x)) → (x : X) → C x → C (iterate k f x)
+  iterate-family-of-maps zero-ℕ g x y = y
+  iterate-family-of-maps (succ-ℕ k) g x y =
+    g (iterate k f x) (iterate-family-of-maps k g x y)
+
+  iterate-family-of-maps' :
+    (k : ℕ) → ((x : X) → C x → C (f x)) → (x : X) → C x → C (iterate' k f x)
+  iterate-family-of-maps' zero-ℕ g x y = y
+  iterate-family-of-maps' (succ-ℕ k) g x y =
+    iterate-family-of-maps' k g (f x) (g x y)
+```
+
+## Properties
+
+### The two definitions of iterating dependent functions are homotopic
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} {C : X → UU l2} {f : X → X}
+  where
+
+  reassociate-iterate-family-of-maps-succ-ℕ :
+    (k : ℕ) (g : (x : X) → C x → C (f x)) (x : X) (y : C x) →
+    dependent-identification C
+      ( reassociate-iterate-succ-ℕ k f x)
+      ( g (iterate k f x) (iterate-family-of-maps k g x y))
+      ( iterate-family-of-maps k g (f x) (g x y))
+  reassociate-iterate-family-of-maps-succ-ℕ zero-ℕ g x y = refl
+  reassociate-iterate-family-of-maps-succ-ℕ (succ-ℕ k) g x y =
+    equational-reasoning
+      tr C
+        ( reassociate-iterate-succ-ℕ (succ-ℕ k) f x)
+        ( g (iterate (succ-ℕ k) f x) (iterate-family-of-maps (succ-ℕ k) g x y))
+      ＝
+      g ( iterate k f (f x))
+        ( tr C
+          ( reassociate-iterate-succ-ℕ k f x)
+          ( g (iterate k f x) (iterate-family-of-maps k g x y)))
+      by
+        tr-ap f g
+          ( reassociate-iterate-succ-ℕ k f x)
+          ( iterate-family-of-maps (succ-ℕ k) g x y)
+      ＝ g (iterate k f (f x)) (iterate-family-of-maps k g (f x) (g x y))
+      by
+        ap
+          ( g (iterate k f (f x)))
+          ( reassociate-iterate-family-of-maps-succ-ℕ k g x y)
+
+  reassociate-iterate-family-of-maps :
+    (k : ℕ) (g : (x : X) → C x → C (f x)) (x : X) (y : C x) →
+    dependent-identification C
+      ( reassociate-iterate k f x)
+      ( iterate-family-of-maps k g x y)
+      ( iterate-family-of-maps' k g x y)
+  reassociate-iterate-family-of-maps zero-ℕ g x y = refl
+  reassociate-iterate-family-of-maps (succ-ℕ k) g x y =
+    concat-dependent-identification C
+      ( reassociate-iterate-succ-ℕ k f x)
+      ( reassociate-iterate k f (f x))
+      ( reassociate-iterate-family-of-maps-succ-ℕ k g x y)
+      ( reassociate-iterate-family-of-maps k g (f x) (g x y))
+```

src/foundation/iterating-functions.lagda.md

@@ -85,15 +85,16 @@ module _
   {l : Level} {X : UU l}
   where
 
-  iterate-succ-ℕ :
+  reassociate-iterate-succ-ℕ :
     (k : ℕ) (f : X → X) (x : X) → iterate (succ-ℕ k) f x ＝ iterate k f (f x)
-  iterate-succ-ℕ zero-ℕ f x = refl
-  iterate-succ-ℕ (succ-ℕ k) f x = ap f (iterate-succ-ℕ k f x)
+  reassociate-iterate-succ-ℕ zero-ℕ f x = refl
+  reassociate-iterate-succ-ℕ (succ-ℕ k) f x =
+    ap f (reassociate-iterate-succ-ℕ k f x)
 
   reassociate-iterate : (k : ℕ) (f : X → X) → iterate k f ~ iterate' k f
   reassociate-iterate zero-ℕ f x = refl
   reassociate-iterate (succ-ℕ k) f x =
-    iterate-succ-ℕ k f x ∙ reassociate-iterate k f (f x)
+    reassociate-iterate-succ-ℕ k f x ∙ reassociate-iterate k f (f x)
 ```
 
 ### For any map `f : X → X`, iterating `f` defines a monoid action of ℕ on `X`
@@ -108,7 +109,8 @@ module _
     iterate (k +ℕ l) f x ＝ iterate k f (iterate l f x)
   iterate-add-ℕ k zero-ℕ f x = refl
   iterate-add-ℕ k (succ-ℕ l) f x =
-    ap f (iterate-add-ℕ k l f x) ∙ iterate-succ-ℕ k f (iterate l f x)
+    ap f (iterate-add-ℕ k l f x) ∙
+    reassociate-iterate-succ-ℕ k f (iterate l f x)
 
   left-unit-law-iterate-add-ℕ :
     (l : ℕ) (f : X → X) (x : X) →
@@ -140,7 +142,7 @@ module _
   iterate-mul-ℕ (succ-ℕ k) l f x =
     ( iterate-add-ℕ (k *ℕ l) l f x) ∙
     ( ( iterate-mul-ℕ k l f (iterate l f x)) ∙
-      ( inv (iterate-succ-ℕ k (iterate l f) x)))
+      ( inv (reassociate-iterate-succ-ℕ k (iterate l f) x)))
 
   iterate-exp-ℕ :
     (k l : ℕ) (f : X → X) (x : X) →
@@ -149,7 +151,7 @@ module _
   iterate-exp-ℕ (succ-ℕ k) l f x =
     ( iterate-mul-ℕ (exp-ℕ l k) l f x) ∙
     ( ( iterate-exp-ℕ k l (iterate l f) x) ∙
-      ( inv (htpy-eq (iterate-succ-ℕ k (iterate l) f) x)))
+      ( inv (htpy-eq (reassociate-iterate-succ-ℕ k (iterate l) f) x)))
 
 module _
   {l : Level} (X : Set l)