diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 429dd75e39..2b6573771b 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -177,6 +177,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/eventually-constant-sequences.lagda.md b/src/foundation/eventually-constant-sequences.lagda.md
new file mode 100644
index 0000000000..87cf65e693
--- /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.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=has-modulus-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
+
+  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
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A}
+  (H : has-modulus-eventually-constant-sequence u)
+  where
+
+  value-has-modulus-eventually-constant-sequence : A
+  value-has-modulus-eventually-constant-sequence =
+    u (modulus-has-modulus-eventually-pointed-sequence H)
+
+  has-modulus-eventual-value-has-modulus-eventually-constant-sequence :
+    has-modulus-eventually-pointed-sequence
+      (λ n → value-has-modulus-eventually-constant-sequence ＝ u n)
+  has-modulus-eventual-value-has-modulus-eventually-constant-sequence =
+    value-at-modulus-has-modulus-eventually-pointed-sequence H
+```
+
+## Properties
+
+### Constant sequences are eventually constant
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A)
+  where
+
+  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
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A}
+  (H : has-modulus-eventually-constant-sequence u)
+  where
+
+  has-modulus-eventually-eq-value-has-modulus-eventually-constant-sequence :
+    has-modulus-eventually-eq-sequence
+      ( const ℕ (value-has-modulus-eventually-constant-sequence H))
+      ( u)
+  has-modulus-eventually-eq-value-has-modulus-eventually-constant-sequence =
+    has-modulus-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
new file mode 100644
index 0000000000..592123e78d
--- /dev/null
+++ b/src/foundation/eventually-equal-sequences.lagda.md
@@ -0,0 +1,153 @@
+# 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=has-modulus-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
+
+  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 : has-modulus-eventually-eq-sequence u v)
+  where
+
+  modulus-has-modulus-eventually-eq-sequence : ℕ
+  modulus-has-modulus-eventually-eq-sequence = pr1 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
+
+### Any sequence is asymptotically equal to itself
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  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
+  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
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v : sequence A)
+  where
+
+  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-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
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v w : sequence A)
+  where
+
+  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
+
+```agda
+module _
+  {l : Level} {A : UU l} {u u' v v' : sequence A}
+  where
+
+  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
new file mode 100644
index 0000000000..00a35600c4
--- /dev/null
+++ b/src/foundation/eventually-pointed-sequences-types.lagda.md
@@ -0,0 +1,174 @@
+# 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
+
+  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 : has-modulus-eventually-pointed-sequence A)
+  where
+
+  modulus-has-modulus-eventually-pointed-sequence : ℕ
+  modulus-has-modulus-eventually-pointed-sequence = pr1 H
+
+  is-modulus-modulus-has-modulus-eventually-pointed-sequence :
+    is-modulus-eventually-pointed-sequence A
+      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
+
+### Pointed sequences are eventually pointed
+
+```agda
+module _
+  {l : Level} {A : ℕ → UU l}
+  where
+
+  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
+
+```agda
+module _
+  {l : Level} (A : ℕ → UU l) (i j : ℕ) (I : leq-ℕ i j)
+  where
+
+  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-has-modulus-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
+
+  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)
+```
+
+### Eventual functorial action on eventually pointed sequences
+
+```agda
+module _
+  {l1 l2 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2}
+  where
+
+  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-has-modulus-eventually-pointed-sequence H)
+      ( modulus-has-modulus-eventually-pointed-sequence K)) ,
+    ( λ m I →
+      is-modulus-modulus-has-modulus-eventually-pointed-sequence H m
+        ( leq-left-leq-max-ℕ m
+          ( modulus-has-modulus-eventually-pointed-sequence H)
+          ( modulus-has-modulus-eventually-pointed-sequence K)
+          ( I))
+        ( is-modulus-modulus-has-modulus-eventually-pointed-sequence K m
+          ( leq-right-leq-max-ℕ m
+            ( modulus-has-modulus-eventually-pointed-sequence H)
+            ( modulus-has-modulus-eventually-pointed-sequence K)
+            ( I))))
+
+  map-Π-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 =
+    map-has-modulus-eventually-pointed-sequence ∘
+    has-modulus-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-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-Π-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 =
+    map-binary-has-modulus-eventually-pointed-sequence ∘
+    has-modulus-eventually-pointed-Π
+```