From 19d91dcf0d4328205d5de9168b739f6dbca96859 Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Tue, 25 Mar 2025 23:32:30 +0100
Subject: [PATCH 1/6] WIP

---
 src/foundation/constant-sequences.lagda.md    | 121 +++++++++++++
 ...ventually-pointed-sequences-types.lagda.md | 169 ++++++++++++++++++
 2 files changed, 290 insertions(+)
 create mode 100644 src/foundation/constant-sequences.lagda.md
 create mode 100644 src/foundation/eventually-pointed-sequences-types.lagda.md

diff --git a/src/foundation/constant-sequences.lagda.md b/src/foundation/constant-sequences.lagda.md
new file mode 100644
index 0000000000..4e34674c66
--- /dev/null
+++ b/src/foundation/constant-sequences.lagda.md
@@ -0,0 +1,121 @@
+# Constant sequences
+
+```agda
+module foundation.constant-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.constant-maps
+open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.pi-decompositions
+open import foundation.sequences
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [sequence](foundation.sequences.md) `u` is
+{{#concept "constant" Disambiguation="sequence" Agda=is-constant-sequence}}
+if `u p ＝ u q` for all `p` and `q`.
+
+## Definitions
+
+### Constant sequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-constant-sequence : UU l
+  is-constant-sequence = (p q : ℕ) → u p ＝ u q
+```
+
+### The type of constant sequences in a type
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  where
+
+  constant-sequence : UU l
+  constant-sequence = Σ (sequence A) is-constant-sequence
+```
+
+### Stationnary values of a sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-stationnary-value-sequence : ℕ → UU l
+  is-stationnary-value-sequence n = (u n) ＝ (u (succ-ℕ n))
+```
+
+## Properties
+
+### The value of a constant sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A} (H : is-constant-sequence u)
+  where
+
+  value-constant-sequence : A
+  value-constant-sequence = u zero-ℕ
+
+  eq-value-constant-sequence : (n : ℕ) → value-constant-sequence ＝ u n
+  eq-value-constant-sequence = H zero-ℕ
+```
+
+### Constant sequences are constant
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A)
+  where
+
+  is-constant-const-sequence : is-constant-sequence (const ℕ x)
+  is-constant-const-sequence p q = refl
+```
+
+### A sequence is constant if all its terms are equal to some element
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A) (u : sequence A)
+  where
+
+  is-constant-htpy-constant-sequence :
+    (const ℕ x) ~ u → is-constant-sequence u
+  is-constant-htpy-constant-sequence H p q = inv (H p) ∙ H q
+```
+
+### A sequence is constant if and only if all its values are stationnary
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-stationnary-value-is-constant-sequence :
+    is-constant-sequence u → Π ℕ (is-stationnary-value-sequence u)
+  is-stationnary-value-is-constant-sequence H n = H n (succ-ℕ n)
+
+  is-constant-is-stationnary-value-sequence :
+    Π ℕ (is-stationnary-value-sequence u) → is-constant-sequence u
+  is-constant-is-stationnary-value-sequence H =
+    is-constant-htpy-constant-sequence
+      ( u zero-ℕ)
+      ( u)
+      ( ind-ℕ (refl) (λ n K → K ∙ H n))
+```
diff --git a/src/foundation/eventually-pointed-sequences-types.lagda.md b/src/foundation/eventually-pointed-sequences-types.lagda.md
new file mode 100644
index 0000000000..02653c953b
--- /dev/null
+++ b/src/foundation/eventually-pointed-sequences-types.lagda.md
@@ -0,0 +1,169 @@
+# Eventually pointed sequences of types
+
+```agda
+module foundation.eventually-pointed-sequences-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.maximum-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.dependent-sequences
+open import foundation.function-types
+open import foundation.pi-decompositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A sequence of types `A : ℕ → UU l` is
+{{# concept "eventually pointed" Disambiguation="sequence of types"}}
+if `A n` is pointed for sufficiently
+[large](elementary-number-theory.inequality-natural-numbers.md)
+[natural numbers](elementary-number-theory.natural-numbers.md) `n`.
+
+## Definitions
+
+### Eventually pointed sequences of types
+
+```agda
+module _
+  {l : Level} (A : ℕ → UU l)
+  where
+
+  is-modulus-eventually-pointed-sequence : ℕ → UU l
+  is-modulus-eventually-pointed-sequence N = (n : ℕ) → leq-ℕ N n → A n
+
+  is-eventually-pointed-sequence : UU l
+  is-eventually-pointed-sequence = Σ ℕ is-modulus-eventually-pointed-sequence
+```
+
+### Modulus of an eventually pointed sequence of types
+
+```agda
+module _
+  {l : Level} {A : ℕ → UU l} (H : is-eventually-pointed-sequence A)
+  where
+
+  modulus-is-eventually-pointed-sequence : ℕ
+  modulus-is-eventually-pointed-sequence = pr1 H
+
+  is-modulus-modulus-is-eventually-pointed-sequence :
+    is-modulus-eventually-pointed-sequence A
+      modulus-is-eventually-pointed-sequence
+  is-modulus-modulus-is-eventually-pointed-sequence = pr2 H
+
+  value-is-eventually-pointed-sequence :
+    A modulus-is-eventually-pointed-sequence
+  value-is-eventually-pointed-sequence =
+    is-modulus-modulus-is-eventually-pointed-sequence
+      ( modulus-is-eventually-pointed-sequence)
+      ( refl-leq-ℕ modulus-is-eventually-pointed-sequence)
+```
+
+## Properties
+
+### Pointed sequences are eventually pointed
+
+```agda
+module _
+  {l : Level} {A : ℕ → UU l}
+  where
+
+  is-eventually-pointed-Π : Π ℕ A → is-eventually-pointed-sequence A
+  is-eventually-pointed-Π u = zero-ℕ , λ p _ → u p
+```
+
+### Any natural number greater than an eventual modulus is an eventual modulus
+
+```agda
+module _
+  {l : Level} (A : ℕ → UU l) (i j : ℕ) (I : leq-ℕ i j)
+  where
+
+  is-modulus-leq-modulus-is-eventually-pointed-seqence :
+    is-modulus-eventually-pointed-sequence A i →
+    is-modulus-eventually-pointed-sequence A j
+  is-modulus-leq-modulus-is-eventually-pointed-seqence H k K =
+    H k (transitive-leq-ℕ i j k K I)
+```
+
+### A sequence that eventually is eventually pointed is eventually pointed
+
+```agda
+module _
+  {l : Level} (A : ℕ → UU l)
+  where
+
+  is-eventually-pointed-is-eventually-modulus-eventually-pointed-sequence :
+    is-eventually-pointed-sequence (is-modulus-eventually-pointed-sequence A) →
+    is-eventually-pointed-sequence A
+  is-eventually-pointed-is-eventually-modulus-eventually-pointed-sequence
+    (N , H) = N , λ n K → H n K n (refl-leq-ℕ n)
+```
+
+### Eventual functorial action on eventually pointed sequences
+
+```agda
+module _
+  {l1 l2 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2}
+  where
+
+  map-is-eventually-pointed-sequence :
+    is-eventually-pointed-sequence (λ n → A n → B n) →
+    is-eventually-pointed-sequence A →
+    is-eventually-pointed-sequence B
+  map-is-eventually-pointed-sequence H K =
+    ( max-ℕ
+      ( modulus-is-eventually-pointed-sequence H)
+      ( modulus-is-eventually-pointed-sequence K)) ,
+    ( λ m I →
+      is-modulus-modulus-is-eventually-pointed-sequence H m
+        ( leq-left-leq-max-ℕ m
+          ( modulus-is-eventually-pointed-sequence H)
+          ( modulus-is-eventually-pointed-sequence K)
+          ( I))
+        ( is-modulus-modulus-is-eventually-pointed-sequence K m
+          ( leq-right-leq-max-ℕ m
+            ( modulus-is-eventually-pointed-sequence H)
+            ( modulus-is-eventually-pointed-sequence K)
+            ( I))))
+
+  map-Π-is-eventually-pointed-sequence :
+    ((n : ℕ) → A n → B n) →
+    is-eventually-pointed-sequence A →
+    is-eventually-pointed-sequence B
+  map-Π-is-eventually-pointed-sequence =
+    map-is-eventually-pointed-sequence ∘ is-eventually-pointed-Π
+```
+
+### Eventual binary functorial action on eventually pointed sequences
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2} {C : ℕ → UU l3}
+  where
+
+  map-binary-is-eventually-pointed-sequence :
+    is-eventually-pointed-sequence (λ n → A n → B n → C n) →
+    is-eventually-pointed-sequence A →
+    is-eventually-pointed-sequence B →
+    is-eventually-pointed-sequence C
+  map-binary-is-eventually-pointed-sequence I =
+    map-is-eventually-pointed-sequence ∘
+    map-is-eventually-pointed-sequence I
+
+  map-binary-Π-is-eventually-pointed-sequence :
+    ((n : ℕ) → A n → B n → C n) →
+    is-eventually-pointed-sequence A →
+    is-eventually-pointed-sequence B →
+    is-eventually-pointed-sequence C
+  map-binary-Π-is-eventually-pointed-sequence =
+    map-binary-is-eventually-pointed-sequence ∘ is-eventually-pointed-Π
+```

From ff0e5f2dcc1cdd494aaef656e44d5b87fc7e7919 Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Wed, 26 Mar 2025 01:01:59 +0100
Subject: [PATCH 2/6] eventual behavior

---
 src/foundation.lagda.md                       |   4 +
 src/foundation/constant-sequences.lagda.md    |   4 +-
 .../eventually-constant-sequences.lagda.md    |  98 ++++++++++++
 .../eventually-equal-sequences.lagda.md       | 147 ++++++++++++++++++
 ...ventually-pointed-sequences-types.lagda.md |   8 +-
 5 files changed, 255 insertions(+), 6 deletions(-)
 create mode 100644 src/foundation/eventually-constant-sequences.lagda.md
 create mode 100644 src/foundation/eventually-equal-sequences.lagda.md

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index fa5ed4f5b6..6a7b11cce1 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -87,6 +87,7 @@ open import foundation.connected-components-universes public
 open import foundation.connected-maps public
 open import foundation.connected-types public
 open import foundation.constant-maps public
+open import foundation.constant-sequences public
 open import foundation.constant-span-diagrams public
 open import foundation.constant-type-families public
 open import foundation.continuations public
@@ -177,6 +178,9 @@ open import foundation.equivalences-span-diagrams-families-of-types public
 open import foundation.equivalences-spans public
 open import foundation.equivalences-spans-families-of-types public
 open import foundation.evaluation-functions public
+open import foundation.eventually-constant-sequences public
+open import foundation.eventually-equal-sequences public
+open import foundation.eventually-pointed-sequences-types public
 open import foundation.exclusive-disjunction public
 open import foundation.exclusive-sum public
 open import foundation.existential-quantification public
diff --git a/src/foundation/constant-sequences.lagda.md b/src/foundation/constant-sequences.lagda.md
index 4e34674c66..4a5097a813 100644
--- a/src/foundation/constant-sequences.lagda.md
+++ b/src/foundation/constant-sequences.lagda.md
@@ -23,8 +23,8 @@ open import foundation.universe-levels
 ## Idea
 
 A [sequence](foundation.sequences.md) `u` is
-{{#concept "constant" Disambiguation="sequence" Agda=is-constant-sequence}}
-if `u p ＝ u q` for all `p` and `q`.
+{{#concept "constant" Disambiguation="sequence" Agda=is-constant-sequence}} if
+`u p ＝ u q` for all `p` and `q`.
 
 ## Definitions
 
diff --git a/src/foundation/eventually-constant-sequences.lagda.md b/src/foundation/eventually-constant-sequences.lagda.md
new file mode 100644
index 0000000000..8bf5fa48ac
--- /dev/null
+++ b/src/foundation/eventually-constant-sequences.lagda.md
@@ -0,0 +1,98 @@
+# Eventually constant sequences
+
+```agda
+module foundation.eventually-constant-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.based-induction-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.maximum-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.constant-maps
+open import foundation.constant-sequences
+open import foundation.dependent-pair-types
+open import foundation.eventually-equal-sequences
+open import foundation.eventually-pointed-sequences-types
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
+open import foundation.sequences
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [sequence](foundation.sequences.md) `u` is
+{{#concept "eventually constant" Disambiguation="sequence" Agda=is-eventually-constant-sequence}}
+if `u p ＝ u q` for sufficiently large `p` and `q`.
+
+## Definitions
+
+### Eventually constant sequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-eventually-constant-sequence : UU l
+  is-eventually-constant-sequence =
+    is-eventually-pointed-sequence
+      (λ p → is-eventually-pointed-sequence (λ q → u p ＝ u q))
+```
+
+### The eventual value of an eventually constant sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A}
+  (H : is-eventually-constant-sequence u)
+  where
+
+  value-is-eventually-constant-sequence : A
+  value-is-eventually-constant-sequence =
+    u (modulus-is-eventually-pointed-sequence H)
+
+  is-eventual-value-is-eventually-constant-sequence :
+    is-eventually-pointed-sequence
+      (λ n → value-is-eventually-constant-sequence ＝ u n)
+  is-eventual-value-is-eventually-constant-sequence =
+    value-at-modulus-is-eventually-pointed-sequence H
+```
+
+## Properties
+
+### Constant sequences are eventually constant
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A} (H : is-constant-sequence u)
+  where
+
+  is-eventually-constant-is-constant-sequence :
+    is-eventually-constant-sequence u
+  pr1 is-eventually-constant-is-constant-sequence = zero-ℕ
+  pr2 is-eventually-constant-is-constant-sequence p I = (zero-ℕ , λ q J → H p q)
+```
+
+### An eventually constant sequence is eventually equal to the constant sequence of its eventual value
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A}
+  (H : is-eventually-constant-sequence u)
+  where
+
+  eventually-eq-value-is-eventually-constant-sequence :
+    eventually-eq-sequence
+      ( const ℕ (value-is-eventually-constant-sequence H))
+      ( u)
+  eventually-eq-value-is-eventually-constant-sequence =
+    is-eventual-value-is-eventually-constant-sequence H
+```
diff --git a/src/foundation/eventually-equal-sequences.lagda.md b/src/foundation/eventually-equal-sequences.lagda.md
new file mode 100644
index 0000000000..24bac29ed2
--- /dev/null
+++ b/src/foundation/eventually-equal-sequences.lagda.md
@@ -0,0 +1,147 @@
+# Eventually equal sequences
+
+```agda
+module foundation.eventually-equal-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.maximum-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.eventually-pointed-sequences-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.sequences
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Two [sequences](foundation.sequences.md) `u` and `v` are
+{{#concept "eventually equal" Disambiguation="sequences" Agda=eventually-eq-sequence}}
+if `u n ＝ v n` for sufficiently large
+[natural numbers](elementary-number-theory.natural-numbers.md) `n : ℕ`.
+
+## Definitions
+
+### The relation of being eventually equal sequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v : sequence A)
+  where
+
+  eventually-eq-sequence : UU l
+  eventually-eq-sequence = is-eventually-pointed-sequence (λ n → u n ＝ v n)
+```
+
+### Modulus of eventual equality
+
+```agda
+module _
+  {l : Level} {A : UU l} {u v : sequence A} (H : eventually-eq-sequence u v)
+  where
+
+  modulus-eventually-eq-sequence : ℕ
+  modulus-eventually-eq-sequence = pr1 H
+
+  is-modulus-eventually-eq-sequence :
+    (n : ℕ) → leq-ℕ modulus-eventually-eq-sequence n → u n ＝ v n
+  is-modulus-eventually-eq-sequence = pr2 H
+```
+
+## Properties
+
+### Any sequence is asymptotically equal to itself
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  refl-eventually-eq-sequence : (u : sequence A) → eventually-eq-sequence u u
+  pr1 (refl-eventually-eq-sequence u) = zero-ℕ
+  pr2 (refl-eventually-eq-sequence u) m H = refl
+```
+
+### Homotopic sequences are eventually equal
+
+```agda
+  eventually-eq-htpy-sequence :
+    {u v : sequence A} → (u ~ v) → eventually-eq-sequence u v
+  eventually-eq-htpy-sequence {u} {v} I = (zero-ℕ , λ n H → I n)
+```
+
+### Eventual equality is a symmetric relation
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v : sequence A)
+  where
+
+  symmetric-eventually-eq-sequence :
+    eventually-eq-sequence u v → eventually-eq-sequence v u
+  symmetric-eventually-eq-sequence =
+    map-Π-is-eventually-pointed-sequence (λ n → inv)
+
+module _
+  {l : Level} {A : UU l} {u v : sequence A}
+  where
+
+  inv-eventually-eq-sequence :
+    eventually-eq-sequence u v → eventually-eq-sequence v u
+  inv-eventually-eq-sequence = symmetric-eventually-eq-sequence u v
+```
+
+### Eventual equality is a transitive relation
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v w : sequence A)
+  where
+
+  transitive-eventually-eq-sequence :
+    eventually-eq-sequence v w →
+    eventually-eq-sequence u v →
+    eventually-eq-sequence u w
+  transitive-eventually-eq-sequence =
+    map-binary-Π-is-eventually-pointed-sequence (λ n I J → J ∙ I)
+```
+
+### Conjugation of asymptotical equality
+
+```agda
+module _
+  {l : Level} {A : UU l} {u u' v v' : sequence A}
+  where
+
+  conjugate-eventually-eq-sequence :
+    eventually-eq-sequence u u' →
+    eventually-eq-sequence v v' →
+    eventually-eq-sequence u v →
+    eventually-eq-sequence u' v'
+  conjugate-eventually-eq-sequence H K I =
+    transitive-eventually-eq-sequence u' u v'
+      ( transitive-eventually-eq-sequence u v v' K I)
+      ( inv-eventually-eq-sequence H)
+
+  conjugate-eventually-eq-sequence' :
+    eventually-eq-sequence u u' →
+    eventually-eq-sequence v v' →
+    eventually-eq-sequence u' v' →
+    eventually-eq-sequence u v
+  conjugate-eventually-eq-sequence' H K I =
+    transitive-eventually-eq-sequence u u' v
+      ( transitive-eventually-eq-sequence u' v' v
+        (inv-eventually-eq-sequence K) I)
+      ( H)
+```
diff --git a/src/foundation/eventually-pointed-sequences-types.lagda.md b/src/foundation/eventually-pointed-sequences-types.lagda.md
index 02653c953b..988483484a 100644
--- a/src/foundation/eventually-pointed-sequences-types.lagda.md
+++ b/src/foundation/eventually-pointed-sequences-types.lagda.md
@@ -23,8 +23,8 @@ open import foundation.universe-levels
 ## Idea
 
 A sequence of types `A : ℕ → UU l` is
-{{# concept "eventually pointed" Disambiguation="sequence of types"}}
-if `A n` is pointed for sufficiently
+{{# concept "eventually pointed" Disambiguation="sequence of types"}} if `A n`
+is pointed for sufficiently
 [large](elementary-number-theory.inequality-natural-numbers.md)
 [natural numbers](elementary-number-theory.natural-numbers.md) `n`.
 
@@ -59,9 +59,9 @@ module _
       modulus-is-eventually-pointed-sequence
   is-modulus-modulus-is-eventually-pointed-sequence = pr2 H
 
-  value-is-eventually-pointed-sequence :
+  value-at-modulus-is-eventually-pointed-sequence :
     A modulus-is-eventually-pointed-sequence
-  value-is-eventually-pointed-sequence =
+  value-at-modulus-is-eventually-pointed-sequence =
     is-modulus-modulus-is-eventually-pointed-sequence
       ( modulus-is-eventually-pointed-sequence)
       ( refl-leq-ℕ modulus-is-eventually-pointed-sequence)

From 15a1f5c48487481fe5fe6b47673f4e8e7200a09b Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Wed, 26 Mar 2025 01:47:08 +0100
Subject: [PATCH 3/6] remove constant sequences

---
 src/foundation.lagda.md                       |   1 -
 src/foundation/constant-sequences.lagda.md    | 121 ------------------
 .../eventually-constant-sequences.lagda.md    |  11 +-
 3 files changed, 5 insertions(+), 128 deletions(-)
 delete mode 100644 src/foundation/constant-sequences.lagda.md

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 6a7b11cce1..39c69a1216 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -87,7 +87,6 @@ open import foundation.connected-components-universes public
 open import foundation.connected-maps public
 open import foundation.connected-types public
 open import foundation.constant-maps public
-open import foundation.constant-sequences public
 open import foundation.constant-span-diagrams public
 open import foundation.constant-type-families public
 open import foundation.continuations public
diff --git a/src/foundation/constant-sequences.lagda.md b/src/foundation/constant-sequences.lagda.md
deleted file mode 100644
index 4a5097a813..0000000000
--- a/src/foundation/constant-sequences.lagda.md
+++ /dev/null
@@ -1,121 +0,0 @@
-# Constant sequences
-
-```agda
-module foundation.constant-sequences where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import elementary-number-theory.natural-numbers
-
-open import foundation.constant-maps
-open import foundation.dependent-pair-types
-open import foundation.homotopies
-open import foundation.identity-types
-open import foundation.pi-decompositions
-open import foundation.sequences
-open import foundation.universe-levels
-```
-
-</details>
-
-## Idea
-
-A [sequence](foundation.sequences.md) `u` is
-{{#concept "constant" Disambiguation="sequence" Agda=is-constant-sequence}} if
-`u p ＝ u q` for all `p` and `q`.
-
-## Definitions
-
-### Constant sequences
-
-```agda
-module _
-  {l : Level} {A : UU l} (u : sequence A)
-  where
-
-  is-constant-sequence : UU l
-  is-constant-sequence = (p q : ℕ) → u p ＝ u q
-```
-
-### The type of constant sequences in a type
-
-```agda
-module _
-  {l : Level} (A : UU l)
-  where
-
-  constant-sequence : UU l
-  constant-sequence = Σ (sequence A) is-constant-sequence
-```
-
-### Stationnary values of a sequence
-
-```agda
-module _
-  {l : Level} {A : UU l} (u : sequence A)
-  where
-
-  is-stationnary-value-sequence : ℕ → UU l
-  is-stationnary-value-sequence n = (u n) ＝ (u (succ-ℕ n))
-```
-
-## Properties
-
-### The value of a constant sequence
-
-```agda
-module _
-  {l : Level} {A : UU l} {u : sequence A} (H : is-constant-sequence u)
-  where
-
-  value-constant-sequence : A
-  value-constant-sequence = u zero-ℕ
-
-  eq-value-constant-sequence : (n : ℕ) → value-constant-sequence ＝ u n
-  eq-value-constant-sequence = H zero-ℕ
-```
-
-### Constant sequences are constant
-
-```agda
-module _
-  {l : Level} {A : UU l} (x : A)
-  where
-
-  is-constant-const-sequence : is-constant-sequence (const ℕ x)
-  is-constant-const-sequence p q = refl
-```
-
-### A sequence is constant if all its terms are equal to some element
-
-```agda
-module _
-  {l : Level} {A : UU l} (x : A) (u : sequence A)
-  where
-
-  is-constant-htpy-constant-sequence :
-    (const ℕ x) ~ u → is-constant-sequence u
-  is-constant-htpy-constant-sequence H p q = inv (H p) ∙ H q
-```
-
-### A sequence is constant if and only if all its values are stationnary
-
-```agda
-module _
-  {l : Level} {A : UU l} (u : sequence A)
-  where
-
-  is-stationnary-value-is-constant-sequence :
-    is-constant-sequence u → Π ℕ (is-stationnary-value-sequence u)
-  is-stationnary-value-is-constant-sequence H n = H n (succ-ℕ n)
-
-  is-constant-is-stationnary-value-sequence :
-    Π ℕ (is-stationnary-value-sequence u) → is-constant-sequence u
-  is-constant-is-stationnary-value-sequence H =
-    is-constant-htpy-constant-sequence
-      ( u zero-ℕ)
-      ( u)
-      ( ind-ℕ (refl) (λ n K → K ∙ H n))
-```
diff --git a/src/foundation/eventually-constant-sequences.lagda.md b/src/foundation/eventually-constant-sequences.lagda.md
index 8bf5fa48ac..9f3f1960b4 100644
--- a/src/foundation/eventually-constant-sequences.lagda.md
+++ b/src/foundation/eventually-constant-sequences.lagda.md
@@ -13,7 +13,6 @@ open import elementary-number-theory.maximum-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.constant-maps
-open import foundation.constant-sequences
 open import foundation.dependent-pair-types
 open import foundation.eventually-equal-sequences
 open import foundation.eventually-pointed-sequences-types
@@ -72,13 +71,13 @@ module _
 
 ```agda
 module _
-  {l : Level} {A : UU l} {u : sequence A} (H : is-constant-sequence u)
+  {l : Level} {A : UU l} (x : A)
   where
 
-  is-eventually-constant-is-constant-sequence :
-    is-eventually-constant-sequence u
-  pr1 is-eventually-constant-is-constant-sequence = zero-ℕ
-  pr2 is-eventually-constant-is-constant-sequence p I = (zero-ℕ , λ q J → H p q)
+  is-eventually-constant-const-sequence :
+    is-eventually-constant-sequence (const ℕ x)
+  pr1 is-eventually-constant-const-sequence = zero-ℕ
+  pr2 is-eventually-constant-const-sequence p I = (zero-ℕ , λ _ _ → refl)
 ```
 
 ### An eventually constant sequence is eventually equal to the constant sequence of its eventual value

From c7508f4f68eb8321a7168977e392feaf1f816d73 Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Wed, 26 Mar 2025 02:20:01 +0100
Subject: [PATCH 4/6] rename is-eventually/has-modulus-eventually

---
 .../eventually-constant-sequences.lagda.md    |  47 +++----
 .../eventually-equal-sequences.lagda.md       | 100 ++++++++-------
 ...ventually-pointed-sequences-types.lagda.md | 115 +++++++++---------
 3 files changed, 137 insertions(+), 125 deletions(-)

diff --git a/src/foundation/eventually-constant-sequences.lagda.md b/src/foundation/eventually-constant-sequences.lagda.md
index 9f3f1960b4..ca57985db8 100644
--- a/src/foundation/eventually-constant-sequences.lagda.md
+++ b/src/foundation/eventually-constant-sequences.lagda.md
@@ -40,10 +40,10 @@ module _
   {l : Level} {A : UU l} (u : sequence A)
   where
 
-  is-eventually-constant-sequence : UU l
-  is-eventually-constant-sequence =
-    is-eventually-pointed-sequence
-      (λ p → is-eventually-pointed-sequence (λ q → u p ＝ u q))
+  has-modulus-eventually-constant-sequence : UU l
+  has-modulus-eventually-constant-sequence =
+    has-modulus-eventually-pointed-sequence
+      (λ p → has-modulus-eventually-pointed-sequence (λ q → u p ＝ u q))
 ```
 
 ### The eventual value of an eventually constant sequence
@@ -51,18 +51,18 @@ module _
 ```agda
 module _
   {l : Level} {A : UU l} {u : sequence A}
-  (H : is-eventually-constant-sequence u)
+  (H : has-modulus-eventually-constant-sequence u)
   where
 
-  value-is-eventually-constant-sequence : A
-  value-is-eventually-constant-sequence =
-    u (modulus-is-eventually-pointed-sequence H)
+  value-has-modulus-eventually-constant-sequence : A
+  value-has-modulus-eventually-constant-sequence =
+    u (modulus-has-modulus-eventually-pointed-sequence H)
 
-  is-eventual-value-is-eventually-constant-sequence :
-    is-eventually-pointed-sequence
-      (λ n → value-is-eventually-constant-sequence ＝ u n)
-  is-eventual-value-is-eventually-constant-sequence =
-    value-at-modulus-is-eventually-pointed-sequence H
+  is-eventual-value-has-modulus-eventually-constant-sequence :
+    has-modulus-eventually-pointed-sequence
+      (λ n → value-has-modulus-eventually-constant-sequence ＝ u n)
+  is-eventual-value-has-modulus-eventually-constant-sequence =
+    value-at-modulus-has-modulus-eventually-pointed-sequence H
 ```
 
 ## Properties
@@ -74,10 +74,11 @@ module _
   {l : Level} {A : UU l} (x : A)
   where
 
-  is-eventually-constant-const-sequence :
-    is-eventually-constant-sequence (const ℕ x)
-  pr1 is-eventually-constant-const-sequence = zero-ℕ
-  pr2 is-eventually-constant-const-sequence p I = (zero-ℕ , λ _ _ → refl)
+  has-modulus-eventually-constant-const-sequence :
+    has-modulus-eventually-constant-sequence (const ℕ x)
+  pr1 has-modulus-eventually-constant-const-sequence = zero-ℕ
+  pr2 has-modulus-eventually-constant-const-sequence p I =
+    (zero-ℕ , λ _ _ → refl)
 ```
 
 ### An eventually constant sequence is eventually equal to the constant sequence of its eventual value
@@ -85,13 +86,13 @@ module _
 ```agda
 module _
   {l : Level} {A : UU l} {u : sequence A}
-  (H : is-eventually-constant-sequence u)
+  (H : has-modulus-eventually-constant-sequence u)
   where
 
-  eventually-eq-value-is-eventually-constant-sequence :
-    eventually-eq-sequence
-      ( const ℕ (value-is-eventually-constant-sequence H))
+  has-modulus-eventually-eq-value-has-modulus-eventually-constant-sequence :
+    has-modulus-eventually-eq-sequence
+      ( const ℕ (value-has-modulus-eventually-constant-sequence H))
       ( u)
-  eventually-eq-value-is-eventually-constant-sequence =
-    is-eventual-value-is-eventually-constant-sequence H
+  has-modulus-eventually-eq-value-has-modulus-eventually-constant-sequence =
+    is-eventual-value-has-modulus-eventually-constant-sequence H
 ```
diff --git a/src/foundation/eventually-equal-sequences.lagda.md b/src/foundation/eventually-equal-sequences.lagda.md
index 24bac29ed2..c433e87b76 100644
--- a/src/foundation/eventually-equal-sequences.lagda.md
+++ b/src/foundation/eventually-equal-sequences.lagda.md
@@ -40,23 +40,25 @@ module _
   {l : Level} {A : UU l} (u v : sequence A)
   where
 
-  eventually-eq-sequence : UU l
-  eventually-eq-sequence = is-eventually-pointed-sequence (λ n → u n ＝ v n)
+  has-modulus-eventually-eq-sequence : UU l
+  has-modulus-eventually-eq-sequence =
+    has-modulus-eventually-pointed-sequence (λ n → u n ＝ v n)
 ```
 
 ### Modulus of eventual equality
 
 ```agda
 module _
-  {l : Level} {A : UU l} {u v : sequence A} (H : eventually-eq-sequence u v)
+  {l : Level} {A : UU l} {u v : sequence A}
+  (H : has-modulus-eventually-eq-sequence u v)
   where
 
-  modulus-eventually-eq-sequence : ℕ
-  modulus-eventually-eq-sequence = pr1 H
+  modulus-has-modulus-eventually-eq-sequence : ℕ
+  modulus-has-modulus-eventually-eq-sequence = pr1 H
 
-  is-modulus-eventually-eq-sequence :
-    (n : ℕ) → leq-ℕ modulus-eventually-eq-sequence n → u n ＝ v n
-  is-modulus-eventually-eq-sequence = pr2 H
+  is-modulus-has-modulus-eventually-eq-sequence :
+    (n : ℕ) → leq-ℕ modulus-has-modulus-eventually-eq-sequence n → u n ＝ v n
+  is-modulus-has-modulus-eventually-eq-sequence = pr2 H
 ```
 
 ## Properties
@@ -65,20 +67,21 @@ module _
 
 ```agda
 module _
-  {l : Level} {A : UU l}
+  {l : Level} {A : UU l} (u : sequence A)
   where
 
-  refl-eventually-eq-sequence : (u : sequence A) → eventually-eq-sequence u u
-  pr1 (refl-eventually-eq-sequence u) = zero-ℕ
-  pr2 (refl-eventually-eq-sequence u) m H = refl
+  refl-has-modulus-eventually-eq-sequence :
+    has-modulus-eventually-eq-sequence u u
+  pr1 refl-has-modulus-eventually-eq-sequence = zero-ℕ
+  pr2 refl-has-modulus-eventually-eq-sequence m H = refl
 ```
 
 ### Homotopic sequences are eventually equal
 
 ```agda
-  eventually-eq-htpy-sequence :
-    {u v : sequence A} → (u ~ v) → eventually-eq-sequence u v
-  eventually-eq-htpy-sequence {u} {v} I = (zero-ℕ , λ n H → I n)
+  has-modulus-eventually-eq-htpy-sequence :
+    {u v : sequence A} → (u ~ v) → has-modulus-eventually-eq-sequence u v
+  has-modulus-eventually-eq-htpy-sequence {u} {v} I = (zero-ℕ , λ n H → I n)
 ```
 
 ### Eventual equality is a symmetric relation
@@ -88,18 +91,21 @@ module _
   {l : Level} {A : UU l} (u v : sequence A)
   where
 
-  symmetric-eventually-eq-sequence :
-    eventually-eq-sequence u v → eventually-eq-sequence v u
-  symmetric-eventually-eq-sequence =
-    map-Π-is-eventually-pointed-sequence (λ n → inv)
+  symmetric-has-modulus-eventually-eq-sequence :
+    has-modulus-eventually-eq-sequence u v →
+    has-modulus-eventually-eq-sequence v u
+  symmetric-has-modulus-eventually-eq-sequence =
+    map-Π-has-modulus-eventually-pointed-sequence (λ n → inv)
 
 module _
   {l : Level} {A : UU l} {u v : sequence A}
   where
 
-  inv-eventually-eq-sequence :
-    eventually-eq-sequence u v → eventually-eq-sequence v u
-  inv-eventually-eq-sequence = symmetric-eventually-eq-sequence u v
+  inv-has-modulus-eventually-eq-sequence :
+    has-modulus-eventually-eq-sequence u v →
+    has-modulus-eventually-eq-sequence v u
+  inv-has-modulus-eventually-eq-sequence =
+    symmetric-has-modulus-eventually-eq-sequence u v
 ```
 
 ### Eventual equality is a transitive relation
@@ -109,12 +115,12 @@ module _
   {l : Level} {A : UU l} (u v w : sequence A)
   where
 
-  transitive-eventually-eq-sequence :
-    eventually-eq-sequence v w →
-    eventually-eq-sequence u v →
-    eventually-eq-sequence u w
-  transitive-eventually-eq-sequence =
-    map-binary-Π-is-eventually-pointed-sequence (λ n I J → J ∙ I)
+  transitive-has-modulus-eventually-eq-sequence :
+    has-modulus-eventually-eq-sequence v w →
+    has-modulus-eventually-eq-sequence u v →
+    has-modulus-eventually-eq-sequence u w
+  transitive-has-modulus-eventually-eq-sequence =
+    map-binary-Π-has-modulus-eventually-pointed-sequence (λ n I J → J ∙ I)
 ```
 
 ### Conjugation of asymptotical equality
@@ -124,24 +130,24 @@ module _
   {l : Level} {A : UU l} {u u' v v' : sequence A}
   where
 
-  conjugate-eventually-eq-sequence :
-    eventually-eq-sequence u u' →
-    eventually-eq-sequence v v' →
-    eventually-eq-sequence u v →
-    eventually-eq-sequence u' v'
-  conjugate-eventually-eq-sequence H K I =
-    transitive-eventually-eq-sequence u' u v'
-      ( transitive-eventually-eq-sequence u v v' K I)
-      ( inv-eventually-eq-sequence H)
-
-  conjugate-eventually-eq-sequence' :
-    eventually-eq-sequence u u' →
-    eventually-eq-sequence v v' →
-    eventually-eq-sequence u' v' →
-    eventually-eq-sequence u v
-  conjugate-eventually-eq-sequence' H K I =
-    transitive-eventually-eq-sequence u u' v
-      ( transitive-eventually-eq-sequence u' v' v
-        (inv-eventually-eq-sequence K) I)
+  conjugate-has-modulus-eventually-eq-sequence :
+    has-modulus-eventually-eq-sequence u u' →
+    has-modulus-eventually-eq-sequence v v' →
+    has-modulus-eventually-eq-sequence u v →
+    has-modulus-eventually-eq-sequence u' v'
+  conjugate-has-modulus-eventually-eq-sequence H K I =
+    transitive-has-modulus-eventually-eq-sequence u' u v'
+      ( transitive-has-modulus-eventually-eq-sequence u v v' K I)
+      ( inv-has-modulus-eventually-eq-sequence H)
+
+  conjugate-has-modulus-eventually-eq-sequence' :
+    has-modulus-eventually-eq-sequence u u' →
+    has-modulus-eventually-eq-sequence v v' →
+    has-modulus-eventually-eq-sequence u' v' →
+    has-modulus-eventually-eq-sequence u v
+  conjugate-has-modulus-eventually-eq-sequence' H K I =
+    transitive-has-modulus-eventually-eq-sequence u u' v
+      ( transitive-has-modulus-eventually-eq-sequence u' v' v
+        (inv-has-modulus-eventually-eq-sequence K) I)
       ( H)
 ```
diff --git a/src/foundation/eventually-pointed-sequences-types.lagda.md b/src/foundation/eventually-pointed-sequences-types.lagda.md
index 988483484a..00a35600c4 100644
--- a/src/foundation/eventually-pointed-sequences-types.lagda.md
+++ b/src/foundation/eventually-pointed-sequences-types.lagda.md
@@ -40,31 +40,32 @@ module _
   is-modulus-eventually-pointed-sequence : ℕ → UU l
   is-modulus-eventually-pointed-sequence N = (n : ℕ) → leq-ℕ N n → A n
 
-  is-eventually-pointed-sequence : UU l
-  is-eventually-pointed-sequence = Σ ℕ is-modulus-eventually-pointed-sequence
+  has-modulus-eventually-pointed-sequence : UU l
+  has-modulus-eventually-pointed-sequence =
+    Σ ℕ is-modulus-eventually-pointed-sequence
 ```
 
 ### Modulus of an eventually pointed sequence of types
 
 ```agda
 module _
-  {l : Level} {A : ℕ → UU l} (H : is-eventually-pointed-sequence A)
+  {l : Level} {A : ℕ → UU l} (H : has-modulus-eventually-pointed-sequence A)
   where
 
-  modulus-is-eventually-pointed-sequence : ℕ
-  modulus-is-eventually-pointed-sequence = pr1 H
+  modulus-has-modulus-eventually-pointed-sequence : ℕ
+  modulus-has-modulus-eventually-pointed-sequence = pr1 H
 
-  is-modulus-modulus-is-eventually-pointed-sequence :
+  is-modulus-modulus-has-modulus-eventually-pointed-sequence :
     is-modulus-eventually-pointed-sequence A
-      modulus-is-eventually-pointed-sequence
-  is-modulus-modulus-is-eventually-pointed-sequence = pr2 H
-
-  value-at-modulus-is-eventually-pointed-sequence :
-    A modulus-is-eventually-pointed-sequence
-  value-at-modulus-is-eventually-pointed-sequence =
-    is-modulus-modulus-is-eventually-pointed-sequence
-      ( modulus-is-eventually-pointed-sequence)
-      ( refl-leq-ℕ modulus-is-eventually-pointed-sequence)
+      modulus-has-modulus-eventually-pointed-sequence
+  is-modulus-modulus-has-modulus-eventually-pointed-sequence = pr2 H
+
+  value-at-modulus-has-modulus-eventually-pointed-sequence :
+    A modulus-has-modulus-eventually-pointed-sequence
+  value-at-modulus-has-modulus-eventually-pointed-sequence =
+    is-modulus-modulus-has-modulus-eventually-pointed-sequence
+      ( modulus-has-modulus-eventually-pointed-sequence)
+      ( refl-leq-ℕ modulus-has-modulus-eventually-pointed-sequence)
 ```
 
 ## Properties
@@ -76,8 +77,9 @@ module _
   {l : Level} {A : ℕ → UU l}
   where
 
-  is-eventually-pointed-Π : Π ℕ A → is-eventually-pointed-sequence A
-  is-eventually-pointed-Π u = zero-ℕ , λ p _ → u p
+  has-modulus-eventually-pointed-Π :
+    Π ℕ A → has-modulus-eventually-pointed-sequence A
+  has-modulus-eventually-pointed-Π u = zero-ℕ , λ p _ → u p
 ```
 
 ### Any natural number greater than an eventual modulus is an eventual modulus
@@ -87,10 +89,10 @@ module _
   {l : Level} (A : ℕ → UU l) (i j : ℕ) (I : leq-ℕ i j)
   where
 
-  is-modulus-leq-modulus-is-eventually-pointed-seqence :
+  is-modulus-leq-modulus-has-modulus-eventually-pointed-seqence :
     is-modulus-eventually-pointed-sequence A i →
     is-modulus-eventually-pointed-sequence A j
-  is-modulus-leq-modulus-is-eventually-pointed-seqence H k K =
+  is-modulus-leq-modulus-has-modulus-eventually-pointed-seqence H k K =
     H k (transitive-leq-ℕ i j k K I)
 ```
 
@@ -101,10 +103,11 @@ module _
   {l : Level} (A : ℕ → UU l)
   where
 
-  is-eventually-pointed-is-eventually-modulus-eventually-pointed-sequence :
-    is-eventually-pointed-sequence (is-modulus-eventually-pointed-sequence A) →
-    is-eventually-pointed-sequence A
-  is-eventually-pointed-is-eventually-modulus-eventually-pointed-sequence
+  has-modulus-eventually-pointed-is-eventually-modulus-eventually-pointed-sequence :
+    has-modulus-eventually-pointed-sequence
+      (is-modulus-eventually-pointed-sequence A) →
+    has-modulus-eventually-pointed-sequence A
+  has-modulus-eventually-pointed-is-eventually-modulus-eventually-pointed-sequence
     (N , H) = N , λ n K → H n K n (refl-leq-ℕ n)
 ```
 
@@ -115,32 +118,33 @@ module _
   {l1 l2 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2}
   where
 
-  map-is-eventually-pointed-sequence :
-    is-eventually-pointed-sequence (λ n → A n → B n) →
-    is-eventually-pointed-sequence A →
-    is-eventually-pointed-sequence B
-  map-is-eventually-pointed-sequence H K =
+  map-has-modulus-eventually-pointed-sequence :
+    has-modulus-eventually-pointed-sequence (λ n → A n → B n) →
+    has-modulus-eventually-pointed-sequence A →
+    has-modulus-eventually-pointed-sequence B
+  map-has-modulus-eventually-pointed-sequence H K =
     ( max-ℕ
-      ( modulus-is-eventually-pointed-sequence H)
-      ( modulus-is-eventually-pointed-sequence K)) ,
+      ( modulus-has-modulus-eventually-pointed-sequence H)
+      ( modulus-has-modulus-eventually-pointed-sequence K)) ,
     ( λ m I →
-      is-modulus-modulus-is-eventually-pointed-sequence H m
+      is-modulus-modulus-has-modulus-eventually-pointed-sequence H m
         ( leq-left-leq-max-ℕ m
-          ( modulus-is-eventually-pointed-sequence H)
-          ( modulus-is-eventually-pointed-sequence K)
+          ( modulus-has-modulus-eventually-pointed-sequence H)
+          ( modulus-has-modulus-eventually-pointed-sequence K)
           ( I))
-        ( is-modulus-modulus-is-eventually-pointed-sequence K m
+        ( is-modulus-modulus-has-modulus-eventually-pointed-sequence K m
           ( leq-right-leq-max-ℕ m
-            ( modulus-is-eventually-pointed-sequence H)
-            ( modulus-is-eventually-pointed-sequence K)
+            ( modulus-has-modulus-eventually-pointed-sequence H)
+            ( modulus-has-modulus-eventually-pointed-sequence K)
             ( I))))
 
-  map-Π-is-eventually-pointed-sequence :
+  map-Π-has-modulus-eventually-pointed-sequence :
     ((n : ℕ) → A n → B n) →
-    is-eventually-pointed-sequence A →
-    is-eventually-pointed-sequence B
-  map-Π-is-eventually-pointed-sequence =
-    map-is-eventually-pointed-sequence ∘ is-eventually-pointed-Π
+    has-modulus-eventually-pointed-sequence A →
+    has-modulus-eventually-pointed-sequence B
+  map-Π-has-modulus-eventually-pointed-sequence =
+    map-has-modulus-eventually-pointed-sequence ∘
+    has-modulus-eventually-pointed-Π
 ```
 
 ### Eventual binary functorial action on eventually pointed sequences
@@ -150,20 +154,21 @@ module _
   {l1 l2 l3 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2} {C : ℕ → UU l3}
   where
 
-  map-binary-is-eventually-pointed-sequence :
-    is-eventually-pointed-sequence (λ n → A n → B n → C n) →
-    is-eventually-pointed-sequence A →
-    is-eventually-pointed-sequence B →
-    is-eventually-pointed-sequence C
-  map-binary-is-eventually-pointed-sequence I =
-    map-is-eventually-pointed-sequence ∘
-    map-is-eventually-pointed-sequence I
+  map-binary-has-modulus-eventually-pointed-sequence :
+    has-modulus-eventually-pointed-sequence (λ n → A n → B n → C n) →
+    has-modulus-eventually-pointed-sequence A →
+    has-modulus-eventually-pointed-sequence B →
+    has-modulus-eventually-pointed-sequence C
+  map-binary-has-modulus-eventually-pointed-sequence I =
+    map-has-modulus-eventually-pointed-sequence ∘
+    map-has-modulus-eventually-pointed-sequence I
 
-  map-binary-Π-is-eventually-pointed-sequence :
+  map-binary-Π-has-modulus-eventually-pointed-sequence :
     ((n : ℕ) → A n → B n → C n) →
-    is-eventually-pointed-sequence A →
-    is-eventually-pointed-sequence B →
-    is-eventually-pointed-sequence C
-  map-binary-Π-is-eventually-pointed-sequence =
-    map-binary-is-eventually-pointed-sequence ∘ is-eventually-pointed-Π
+    has-modulus-eventually-pointed-sequence A →
+    has-modulus-eventually-pointed-sequence B →
+    has-modulus-eventually-pointed-sequence C
+  map-binary-Π-has-modulus-eventually-pointed-sequence =
+    map-binary-has-modulus-eventually-pointed-sequence ∘
+    has-modulus-eventually-pointed-Π
 ```

From 5fcaac09839977f573941cb7d06810c408ad202f Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Wed, 26 Mar 2025 02:34:53 +0100
Subject: [PATCH 5/6] fix links

---
 src/foundation/eventually-constant-sequences.lagda.md | 2 +-
 src/foundation/eventually-equal-sequences.lagda.md    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/foundation/eventually-constant-sequences.lagda.md b/src/foundation/eventually-constant-sequences.lagda.md
index ca57985db8..ab6a9b31f7 100644
--- a/src/foundation/eventually-constant-sequences.lagda.md
+++ b/src/foundation/eventually-constant-sequences.lagda.md
@@ -28,7 +28,7 @@ open import foundation.universe-levels
 ## Idea
 
 A [sequence](foundation.sequences.md) `u` is
-{{#concept "eventually constant" Disambiguation="sequence" Agda=is-eventually-constant-sequence}}
+{{#concept "eventually constant" Disambiguation="sequence" Agda=has-modulus-eventually-constant-sequence}}
 if `u p ＝ u q` for sufficiently large `p` and `q`.
 
 ## Definitions
diff --git a/src/foundation/eventually-equal-sequences.lagda.md b/src/foundation/eventually-equal-sequences.lagda.md
index c433e87b76..592123e78d 100644
--- a/src/foundation/eventually-equal-sequences.lagda.md
+++ b/src/foundation/eventually-equal-sequences.lagda.md
@@ -27,7 +27,7 @@ open import foundation-core.function-types
 ## Idea
 
 Two [sequences](foundation.sequences.md) `u` and `v` are
-{{#concept "eventually equal" Disambiguation="sequences" Agda=eventually-eq-sequence}}
+{{#concept "eventually equal" Disambiguation="sequences" Agda=has-modulus-eventually-eq-sequence}}
 if `u n ＝ v n` for sufficiently large
 [natural numbers](elementary-number-theory.natural-numbers.md) `n : ℕ`.
 

From f7b86a43069caff84181ee22b71060a9010b6031 Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Wed, 26 Mar 2025 02:46:58 +0100
Subject: [PATCH 6/6] fix name

---
 src/foundation/eventually-constant-sequences.lagda.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/foundation/eventually-constant-sequences.lagda.md b/src/foundation/eventually-constant-sequences.lagda.md
index ab6a9b31f7..87cf65e693 100644
--- a/src/foundation/eventually-constant-sequences.lagda.md
+++ b/src/foundation/eventually-constant-sequences.lagda.md
@@ -58,10 +58,10 @@ module _
   value-has-modulus-eventually-constant-sequence =
     u (modulus-has-modulus-eventually-pointed-sequence H)
 
-  is-eventual-value-has-modulus-eventually-constant-sequence :
+  has-modulus-eventual-value-has-modulus-eventually-constant-sequence :
     has-modulus-eventually-pointed-sequence
       (λ n → value-has-modulus-eventually-constant-sequence ＝ u n)
-  is-eventual-value-has-modulus-eventually-constant-sequence =
+  has-modulus-eventual-value-has-modulus-eventually-constant-sequence =
     value-at-modulus-has-modulus-eventually-pointed-sequence H
 ```
 
@@ -94,5 +94,5 @@ module _
       ( const ℕ (value-has-modulus-eventually-constant-sequence H))
       ( u)
   has-modulus-eventually-eq-value-has-modulus-eventually-constant-sequence =
-    is-eventual-value-has-modulus-eventually-constant-sequence H
+    has-modulus-eventual-value-has-modulus-eventually-constant-sequence H
 ```