From 1dac64567ff6018515e16b0c9cf0470090847712 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 11 Oct 2024 16:43:45 +0200
Subject: [PATCH 1/4] iteration dependent functions

---
 .../finitely-cyclic-maps.lagda.md             |   7 +-
 src/foundation.lagda.md                       |   1 +
 ...ndent-inverse-sequential-diagrams.lagda.md |  36 +++++-
 ...ences-inverse-sequential-diagrams.lagda.md |   7 +-
 .../inverse-sequential-diagrams.lagda.md      |   3 +-
 .../iterating-dependent-functions.lagda.md    | 115 +++++++++++++++++
 src/foundation/iterating-functions.lagda.md   |  16 ++-
 ...hisms-inverse-sequential-diagrams.lagda.md | 120 +++++++++---------
 .../multivariable-correspondences.lagda.md    |   3 +-
 9 files changed, 223 insertions(+), 85 deletions(-)
 create mode 100644 src/foundation/iterating-dependent-functions.lagda.md

diff --git a/src/elementary-number-theory/finitely-cyclic-maps.lagda.md b/src/elementary-number-theory/finitely-cyclic-maps.lagda.md
index d5cbb43992..d70daec324 100644
--- a/src/elementary-number-theory/finitely-cyclic-maps.lagda.md
+++ b/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))
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 83228240ab..a3ca8bb494 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -234,6 +234,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-dependent-functions public
 open import foundation.iterating-functions public
 open import foundation.iterating-involutions public
 open import foundation.kernel-span-diagrams-of-maps public
diff --git a/src/foundation/dependent-inverse-sequential-diagrams.lagda.md b/src/foundation/dependent-inverse-sequential-diagrams.lagda.md
index 962e766c42..aef65a37d3 100644
--- a/src/foundation/dependent-inverse-sequential-diagrams.lagda.md
+++ b/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-dependent-functions
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -114,9 +115,10 @@ 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)
 
@@ -124,8 +126,7 @@ module _
   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-dependent 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-dependent n
+    ( λ A → left-shift-dependent-inverse-sequential-diagram {A = A})
+    ( A)
 ```
 
 ## Table of files about sequential limits
diff --git a/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md b/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md
index c7439c75b1..3653847a20 100644
--- a/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md
+++ b/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) →
diff --git a/src/foundation/inverse-sequential-diagrams.lagda.md b/src/foundation/inverse-sequential-diagrams.lagda.md
index 967d3f4e29..28053d466e 100644
--- a/src/foundation/inverse-sequential-diagrams.lagda.md
+++ b/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
 ```
diff --git a/src/foundation/iterating-dependent-functions.lagda.md b/src/foundation/iterating-dependent-functions.lagda.md
new file mode 100644
index 0000000000..038042fa4e
--- /dev/null
+++ b/src/foundation/iterating-dependent-functions.lagda.md
@@ -0,0 +1,115 @@
+# Iterating dependent functions
+
+```agda
+module foundation.iterating-dependent-functions 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 dependent map `g : (x : X) → C x → C (f x)` over a map `f : X → X` then
+`g` can be
+{{#concept "iterated" Disambiguation="dependent map of types" Agda=iterate-dependent}}
+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-dependent :
+    (k : ℕ) → ((x : X) → C x → C (f x)) → (x : X) → C x → C (iterate k f x)
+  iterate-dependent zero-ℕ g x y = y
+  iterate-dependent (succ-ℕ k) g x y =
+    g (iterate k f x) (iterate-dependent k g x y)
+
+  iterate-dependent' :
+    (k : ℕ) → ((x : X) → C x → C (f x)) → (x : X) → C x → C (iterate' k f x)
+  iterate-dependent' zero-ℕ g x y = y
+  iterate-dependent' (succ-ℕ k) g x y = iterate-dependent' 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-dependent-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-dependent k g x y))
+      ( iterate-dependent k g (f x) (g x y))
+  reassociate-iterate-dependent-succ-ℕ zero-ℕ g x y = refl
+  reassociate-iterate-dependent-succ-ℕ (succ-ℕ k) g x y =
+    equational-reasoning
+      tr C
+        ( reassociate-iterate-succ-ℕ (succ-ℕ k) f x)
+        ( g (iterate (succ-ℕ k) f x) (iterate-dependent (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-dependent k g x y)))
+      by
+        tr-ap f g
+          ( reassociate-iterate-succ-ℕ k f x)
+          ( iterate-dependent (succ-ℕ k) g x y)
+      ＝ g (iterate k f (f x)) (iterate-dependent k g (f x) (g x y))
+      by
+        ap
+          ( g (iterate k f (f x)))
+          ( reassociate-iterate-dependent-succ-ℕ k g x y)
+
+  reassociate-iterate-dependent :
+    (k : ℕ) (g : (x : X) → C x → C (f x)) (x : X) (y : C x) →
+    dependent-identification C
+      ( reassociate-iterate k f x)
+      ( iterate-dependent k g x y)
+      ( iterate-dependent' k g x y)
+  reassociate-iterate-dependent zero-ℕ g x y = refl
+  reassociate-iterate-dependent (succ-ℕ k) g x y =
+    concat-dependent-identification C
+      ( reassociate-iterate-succ-ℕ k f x)
+      ( reassociate-iterate k f (f x))
+      ( reassociate-iterate-dependent-succ-ℕ k g x y)
+      (reassociate-iterate-dependent k g (f x) (g x y))
+```
diff --git a/src/foundation/iterating-functions.lagda.md b/src/foundation/iterating-functions.lagda.md
index edf0a3ddd1..339d4eed0c 100644
--- a/src/foundation/iterating-functions.lagda.md
+++ b/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)
diff --git a/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md b/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md
index 794b939f5a..515f06b8ce 100644
--- a/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md
+++ b/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md
@@ -48,50 +48,50 @@ the form
 ### Morphisms of inverse sequential diagrams of types
 
 ```agda
-naturality-hom-inverse-sequential-diagram :
+module _
   {l1 l2 : Level}
   (A : inverse-sequential-diagram l1)
   (B : inverse-sequential-diagram l2)
-  (h :
-    (n : ℕ) →
-    family-inverse-sequential-diagram A n →
-    family-inverse-sequential-diagram B n)
-  (n : ℕ) → UU (l1 ⊔ l2)
-naturality-hom-inverse-sequential-diagram A B =
-  naturality-section-dependent-inverse-sequential-diagram A
-    ( const-dependent-inverse-sequential-diagram A B)
+  where
 
-hom-inverse-sequential-diagram :
-  {l1 l2 : Level}
-  (A : inverse-sequential-diagram l1)
-  (B : inverse-sequential-diagram l2) →
-  UU (l1 ⊔ l2)
-hom-inverse-sequential-diagram A B =
-  section-dependent-inverse-sequential-diagram A
-    ( const-dependent-inverse-sequential-diagram A B)
+  naturality-hom-inverse-sequential-diagram :
+    (h :
+      (n : ℕ) →
+      family-inverse-sequential-diagram A n →
+      family-inverse-sequential-diagram B n) →
+    UU (l1 ⊔ l2)
+  naturality-hom-inverse-sequential-diagram =
+    naturality-section-dependent-inverse-sequential-diagram A
+      ( const-dependent-inverse-sequential-diagram A B)
+
+  hom-inverse-sequential-diagram : UU (l1 ⊔ l2)
+  hom-inverse-sequential-diagram =
+    section-dependent-inverse-sequential-diagram A
+      ( const-dependent-inverse-sequential-diagram A B)
 
 module _
   {l1 l2 : Level}
   (A : inverse-sequential-diagram l1)
   (B : inverse-sequential-diagram l2)
+  (f : hom-inverse-sequential-diagram A B)
   where
 
   map-hom-inverse-sequential-diagram :
-    hom-inverse-sequential-diagram A B → (n : ℕ) →
+    (n : ℕ) →
     family-inverse-sequential-diagram A n →
     family-inverse-sequential-diagram B n
   map-hom-inverse-sequential-diagram =
     map-section-dependent-inverse-sequential-diagram A
       ( const-dependent-inverse-sequential-diagram A B)
+      ( f)
 
   naturality-map-hom-inverse-sequential-diagram :
-    (f : hom-inverse-sequential-diagram A B) (n : ℕ) →
     naturality-hom-inverse-sequential-diagram A B
-      ( map-hom-inverse-sequential-diagram f)
-      ( n)
+      ( map-hom-inverse-sequential-diagram)
   naturality-map-hom-inverse-sequential-diagram =
     naturality-map-section-dependent-inverse-sequential-diagram A
       ( const-dependent-inverse-sequential-diagram A B)
+      ( f)
 ```
 
 ### Identity morphism on inverse sequential diagrams of types
@@ -107,39 +107,38 @@ pr2 (id-hom-inverse-sequential-diagram A) n = refl-htpy
 ### Composition of morphisms of inverse sequential diagrams of types
 
 ```agda
-map-comp-hom-inverse-sequential-diagram :
-  {l : Level} (A B C : inverse-sequential-diagram l) →
-  hom-inverse-sequential-diagram B C → hom-inverse-sequential-diagram A B →
-  (n : ℕ) →
-  family-inverse-sequential-diagram A n → family-inverse-sequential-diagram C n
-map-comp-hom-inverse-sequential-diagram A B C g f n =
-  map-hom-inverse-sequential-diagram B C g n ∘
-  map-hom-inverse-sequential-diagram A B f n
-
-naturality-comp-hom-inverse-sequential-diagram :
-  {l : Level} (A B C : inverse-sequential-diagram l)
-  (g : hom-inverse-sequential-diagram B C)
-  (f : hom-inverse-sequential-diagram A B)
-  (n : ℕ) →
-  naturality-hom-inverse-sequential-diagram A C
-    ( map-comp-hom-inverse-sequential-diagram A B C g f)
-    ( n)
-naturality-comp-hom-inverse-sequential-diagram A B C g f n x =
-  ( ap
-    ( map-hom-inverse-sequential-diagram B C g n)
-    ( naturality-map-hom-inverse-sequential-diagram A B f n x)) ∙
-  ( naturality-map-hom-inverse-sequential-diagram B C g n
-    ( map-hom-inverse-sequential-diagram A B f (succ-ℕ n) x))
-
-comp-hom-inverse-sequential-diagram :
-  {l : Level} (A B C : inverse-sequential-diagram l) →
-  hom-inverse-sequential-diagram B C →
-  hom-inverse-sequential-diagram A B →
-  hom-inverse-sequential-diagram A C
-pr1 (comp-hom-inverse-sequential-diagram A B C g f) =
-  map-comp-hom-inverse-sequential-diagram A B C g f
-pr2 (comp-hom-inverse-sequential-diagram A B C g f) =
-  naturality-comp-hom-inverse-sequential-diagram A B C g f
+module _
+  {l1 l2 l3 : Level}
+  ( A : inverse-sequential-diagram l1)
+  ( B : inverse-sequential-diagram l2)
+  ( C : inverse-sequential-diagram l3)
+  ( g : hom-inverse-sequential-diagram B C)
+  ( f : hom-inverse-sequential-diagram A B)
+  where
+
+  map-comp-hom-inverse-sequential-diagram :
+    (n : ℕ) →
+    family-inverse-sequential-diagram A n →
+    family-inverse-sequential-diagram C n
+  map-comp-hom-inverse-sequential-diagram n =
+    map-hom-inverse-sequential-diagram B C g n ∘
+    map-hom-inverse-sequential-diagram A B f n
+
+  naturality-comp-hom-inverse-sequential-diagram :
+    naturality-hom-inverse-sequential-diagram A C
+      ( map-comp-hom-inverse-sequential-diagram)
+  naturality-comp-hom-inverse-sequential-diagram n x =
+    ( ap
+      ( map-hom-inverse-sequential-diagram B C g n)
+      ( naturality-map-hom-inverse-sequential-diagram A B f n x)) ∙
+    ( naturality-map-hom-inverse-sequential-diagram B C g n
+      ( map-hom-inverse-sequential-diagram A B f (succ-ℕ n) x))
+
+  comp-hom-inverse-sequential-diagram :
+    hom-inverse-sequential-diagram A C
+  comp-hom-inverse-sequential-diagram =
+    map-comp-hom-inverse-sequential-diagram ,
+    naturality-comp-hom-inverse-sequential-diagram
 ```
 
 ## Properties
@@ -158,8 +157,9 @@ module _
     ((n : ℕ) →
       map-hom-inverse-sequential-diagram A B f n ~
       map-hom-inverse-sequential-diagram A B g n) →
-    (n : ℕ) → UU (l1 ⊔ l2)
-  coherence-htpy-hom-inverse-sequential-diagram f g H n =
+    UU (l1 ⊔ l2)
+  coherence-htpy-hom-inverse-sequential-diagram f g H =
+    (n : ℕ) →
     ( naturality-map-hom-inverse-sequential-diagram A B f n ∙h
       map-inverse-sequential-diagram B n ·l H (succ-ℕ n)) ~
     ( H n ·r map-inverse-sequential-diagram A n ∙h
@@ -171,7 +171,7 @@ module _
     Σ ( (n : ℕ) →
         map-hom-inverse-sequential-diagram A B f n ~
         map-hom-inverse-sequential-diagram A B g n)
-      ( λ H → (n : ℕ) → coherence-htpy-hom-inverse-sequential-diagram f g H n)
+      ( coherence-htpy-hom-inverse-sequential-diagram f g)
 
   refl-htpy-hom-inverse-sequential-diagram :
     (f : hom-inverse-sequential-diagram A B) →
@@ -193,11 +193,9 @@ module _
       ( is-torsorial-binary-htpy (map-hom-inverse-sequential-diagram A B f))
       ( map-hom-inverse-sequential-diagram A B f ,
         refl-binary-htpy (map-hom-inverse-sequential-diagram A B f))
-      ( is-torsorial-Eq-Π
+      ( is-torsorial-binary-htpy
         ( λ n →
-          is-torsorial-htpy
-            ( naturality-map-hom-inverse-sequential-diagram A B f n ∙h
-              refl-htpy)))
+          naturality-map-hom-inverse-sequential-diagram A B f n ∙h refl-htpy))
 
   is-equiv-htpy-eq-hom-inverse-sequential-diagram :
     (f g : hom-inverse-sequential-diagram A B) →
diff --git a/src/foundation/multivariable-correspondences.lagda.md b/src/foundation/multivariable-correspondences.lagda.md
index 9d753057aa..817901c593 100644
--- a/src/foundation/multivariable-correspondences.lagda.md
+++ b/src/foundation/multivariable-correspondences.lagda.md
@@ -19,8 +19,7 @@ open import univalent-combinatorics.standard-finite-types
 ## Idea
 
 Consider a family of types `A` indexed by `Fin n`. An `n`-ary correspondence of
-tuples `(x₁, …, xₙ)` where `x_i : A_i` is a type family over
-`(i : Fin n) → A i`.
+tuples `(x₁, …, xₙ)` where `xᵢ : A i` is a type family over `(i : Fin n) → A i`.
 
 ## Definition
 

From 9e8dfe77b96c54fcfdcf0e8cc701bda868fa7bba Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 11 Oct 2024 16:58:09 +0200
Subject: [PATCH 2/4] a missing space

---
 src/foundation/iterating-dependent-functions.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/iterating-dependent-functions.lagda.md b/src/foundation/iterating-dependent-functions.lagda.md
index 038042fa4e..7d5c360fb0 100644
--- a/src/foundation/iterating-dependent-functions.lagda.md
+++ b/src/foundation/iterating-dependent-functions.lagda.md
@@ -111,5 +111,5 @@ module _
       ( reassociate-iterate-succ-ℕ k f x)
       ( reassociate-iterate k f (f x))
       ( reassociate-iterate-dependent-succ-ℕ k g x y)
-      (reassociate-iterate-dependent k g (f x) (g x y))
+      ( reassociate-iterate-dependent k g (f x) (g x y))
 ```

From 96a19da1c6d33444f4f0af95abb377d16d6a6f3e Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 13 Oct 2024 23:11:30 +0200
Subject: [PATCH 3/4] iterating dependent functions -> iterating families of
 maps

---
 src/foundation.lagda.md                       |  1 -
 ...ndent-inverse-sequential-diagrams.lagda.md |  6 +-
 ...md => iterating-families-of-maps.lagda.md} | 58 +++++++++----------
 3 files changed, 32 insertions(+), 33 deletions(-)
 rename src/foundation/{iterating-dependent-functions.lagda.md => iterating-families-of-maps.lagda.md} (60%)

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index a3ca8bb494..83228240ab 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -234,7 +234,6 @@ 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-dependent-functions public
 open import foundation.iterating-functions public
 open import foundation.iterating-involutions public
 open import foundation.kernel-span-diagrams-of-maps public
diff --git a/src/foundation/dependent-inverse-sequential-diagrams.lagda.md b/src/foundation/dependent-inverse-sequential-diagrams.lagda.md
index aef65a37d3..f48ea9d065 100644
--- a/src/foundation/dependent-inverse-sequential-diagrams.lagda.md
+++ b/src/foundation/dependent-inverse-sequential-diagrams.lagda.md
@@ -11,7 +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-dependent-functions
+open import foundation.iterating-families-of-maps
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -166,7 +166,7 @@ iterated-right-shift-dependent-inverse-sequential-diagram :
   dependent-inverse-sequential-diagram l2
     ( iterated-right-shift-inverse-sequential-diagram n A)
 iterated-right-shift-dependent-inverse-sequential-diagram n A =
-  iterate-dependent n
+  iterate-family-of-maps n
     ( λ A → right-shift-dependent-inverse-sequential-diagram {A = A})
     ( A)
 ```
@@ -198,7 +198,7 @@ iterated-left-shift-dependent-inverse-sequential-diagram :
   dependent-inverse-sequential-diagram l2
     ( iterated-left-shift-inverse-sequential-diagram n A)
 iterated-left-shift-dependent-inverse-sequential-diagram n A =
-  iterate-dependent n
+  iterate-family-of-maps n
     ( λ A → left-shift-dependent-inverse-sequential-diagram {A = A})
     ( A)
 ```
diff --git a/src/foundation/iterating-dependent-functions.lagda.md b/src/foundation/iterating-families-of-maps.lagda.md
similarity index 60%
rename from src/foundation/iterating-dependent-functions.lagda.md
rename to src/foundation/iterating-families-of-maps.lagda.md
index 7d5c360fb0..c9f5ee9761 100644
--- a/src/foundation/iterating-dependent-functions.lagda.md
+++ b/src/foundation/iterating-families-of-maps.lagda.md
@@ -1,7 +1,7 @@
-# Iterating dependent functions
+# Iterating families of maps over a map
 
 ```agda
-module foundation.iterating-dependent-functions where
+module foundation.iterating-families-of-maps where
 ```
 
 <details><summary>Imports</summary>
@@ -37,9 +37,9 @@ open import group-theory.monoid-actions
 
 ## Idea
 
-Given a dependent map `g : (x : X) → C x → C (f x)` over a map `f : X → X` then
-`g` can be
-{{#concept "iterated" Disambiguation="dependent map of types" Agda=iterate-dependent}}
+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
@@ -51,16 +51,16 @@ module _
   {l1 l2 : Level} {X : UU l1} {C : X → UU l2} {f : X → X}
   where
 
-  iterate-dependent :
+  iterate-family-of-maps :
     (k : ℕ) → ((x : X) → C x → C (f x)) → (x : X) → C x → C (iterate k f x)
-  iterate-dependent zero-ℕ g x y = y
-  iterate-dependent (succ-ℕ k) g x y =
-    g (iterate k f x) (iterate-dependent k g x y)
+  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-dependent' :
+  iterate-family-of-maps' :
     (k : ℕ) → ((x : X) → C x → C (f x)) → (x : X) → C x → C (iterate' k f x)
-  iterate-dependent' zero-ℕ g x y = y
-  iterate-dependent' (succ-ℕ k) g x y = iterate-dependent' k g (f x) (g x y)
+  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
@@ -72,44 +72,44 @@ module _
   {l1 l2 : Level} {X : UU l1} {C : X → UU l2} {f : X → X}
   where
 
-  reassociate-iterate-dependent-succ-ℕ :
+  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-dependent k g x y))
-      ( iterate-dependent k g (f x) (g x y))
-  reassociate-iterate-dependent-succ-ℕ zero-ℕ g x y = refl
-  reassociate-iterate-dependent-succ-ℕ (succ-ℕ k) g x y =
+      ( 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-dependent (succ-ℕ k) g x y))
+        ( 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-dependent k g x y)))
+          ( 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-dependent (succ-ℕ k) g x y)
-      ＝ g (iterate k f (f x)) (iterate-dependent k g (f x) (g x y))
+          ( 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-dependent-succ-ℕ k g x y)
+          ( reassociate-iterate-family-of-maps-succ-ℕ k g x y)
 
-  reassociate-iterate-dependent :
+  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-dependent k g x y)
-      ( iterate-dependent' k g x y)
-  reassociate-iterate-dependent zero-ℕ g x y = refl
-  reassociate-iterate-dependent (succ-ℕ k) g x y =
+      ( 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-dependent-succ-ℕ k g x y)
-      ( reassociate-iterate-dependent k g (f x) (g x y))
+      ( reassociate-iterate-family-of-maps-succ-ℕ k g x y)
+      ( reassociate-iterate-family-of-maps k g (f x) (g x y))
 ```

From c552c837d81973cc056e0c39e8c1784387ab325f Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 13 Oct 2024 23:12:41 +0200
Subject: [PATCH 4/4] pre-commit

---
 src/foundation.lagda.md                            | 1 +
 src/foundation/iterating-families-of-maps.lagda.md | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 83228240ab..cdd2cce616 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -234,6 +234,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
diff --git a/src/foundation/iterating-families-of-maps.lagda.md b/src/foundation/iterating-families-of-maps.lagda.md
index c9f5ee9761..97b4fa1ce6 100644
--- a/src/foundation/iterating-families-of-maps.lagda.md
+++ b/src/foundation/iterating-families-of-maps.lagda.md
@@ -60,7 +60,8 @@ module _
   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)
+  iterate-family-of-maps' (succ-ℕ k) g x y =
+    iterate-family-of-maps' k g (f x) (g x y)
 ```
 
 ## Properties