diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index 92bf495587..17d5a5ee62 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -37,6 +37,7 @@ open import elementary-number-theory.decidable-total-order-natural-numbers publi
 open import elementary-number-theory.decidable-total-order-rational-numbers public
 open import elementary-number-theory.decidable-total-order-standard-finite-types public
 open import elementary-number-theory.decidable-types public
+open import elementary-number-theory.decreasing-sequences-natural-numbers public
 open import elementary-number-theory.difference-integers public
 open import elementary-number-theory.difference-rational-numbers public
 open import elementary-number-theory.dirichlet-convolution public
@@ -64,6 +65,7 @@ open import elementary-number-theory.greatest-common-divisor-natural-numbers pub
 open import elementary-number-theory.group-of-integers public
 open import elementary-number-theory.half-integers public
 open import elementary-number-theory.hardy-ramanujan-number public
+open import elementary-number-theory.increasing-sequences-natural-numbers public
 open import elementary-number-theory.inequality-integer-fractions public
 open import elementary-number-theory.inequality-integers public
 open import elementary-number-theory.inequality-natural-numbers public
@@ -144,6 +146,8 @@ open import elementary-number-theory.strict-inequality-integer-fractions public
 open import elementary-number-theory.strict-inequality-integers public
 open import elementary-number-theory.strict-inequality-natural-numbers public
 open import elementary-number-theory.strict-inequality-rational-numbers public
+open import elementary-number-theory.strictly-decreasing-sequences-natural-numbers public
+open import elementary-number-theory.strictly-increasing-sequences-natural-numbers public
 open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public
 open import elementary-number-theory.strong-induction-natural-numbers public
 open import elementary-number-theory.sums-of-natural-numbers public
diff --git a/src/elementary-number-theory/decreasing-sequences-natural-numbers.lagda.md b/src/elementary-number-theory/decreasing-sequences-natural-numbers.lagda.md
new file mode 100644
index 0000000000..4ef89df848
--- /dev/null
+++ b/src/elementary-number-theory/decreasing-sequences-natural-numbers.lagda.md
@@ -0,0 +1,397 @@
+# Decreasing sequences of natural numbers
+
+```agda
+module elementary-number-theory.decreasing-sequences-natural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.based-induction-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
+open import elementary-number-theory.strictly-decreasing-sequences-natural-numbers
+open import elementary-number-theory.strictly-increasing-sequences-natural-numbers
+
+open import foundation.asymptotical-dependent-sequences
+open import foundation.asymptotical-value-sequences
+open import foundation.asymptotically-constant-sequences
+open import foundation.cartesian-product-types
+open import foundation.constant-sequences
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.functoriality-coproduct-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.subsequences
+open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-empty-type
+open import foundation.universe-levels
+
+open import order-theory.decreasing-sequences-posets
+open import order-theory.sequences-posets
+```
+
+</details>
+
+## Idea
+
+A sequence of natural numbers is **decreasing** if it reverses
+[inequality of natural numbers](elementary-number-theory.inequality-natural-numbers.md).
+
+## Definitions
+
+### Decreasing values of sequences of natural numbers
+
+```agda
+module _
+  (f : sequence ℕ) (n : ℕ)
+  where
+
+  is-decreasing-value-sequence-ℕ : UU lzero
+  is-decreasing-value-sequence-ℕ =
+    is-decreasing-value-sequence-poset ℕ-Poset f n
+```
+
+### Decreasing sequences of natural numbers
+
+```agda
+module _
+  (f : sequence ℕ)
+  where
+
+  is-decreasing-sequence-ℕ : UU lzero
+  is-decreasing-sequence-ℕ = is-decreasing-sequence-poset ℕ-Poset f
+```
+
+## Properties
+
+### A decreasing sequence of natural numbers that takes the value zero is asymptotically equal to zero
+
+```agda
+module _
+  {f : sequence ℕ} (H : is-decreasing-sequence-ℕ f)
+  where
+
+  ∞-zero-value-is-zero-value-decreasing-sequence-ℕ :
+    Σ ℕ (is-value-sequence zero-ℕ f) → is-∞-value-sequence zero-ℕ f
+  ∞-zero-value-is-zero-value-decreasing-sequence-ℕ =
+    tot
+      ( λ n K k I →
+        is-zero-leq-zero-ℕ'
+          ( f k)
+          ( inv-tr (leq-ℕ (f k)) K (H n k I)))
+```
+
+### A decreasing value of a sequence of natural numbers is either stationnary or strictly decreasing
+
+```agda
+module _
+  (f : sequence ℕ) (n : ℕ)
+  where
+
+  decide-is-stationnary-is-decreasing-value-sequence-ℕ :
+    is-decreasing-value-sequence-ℕ f n →
+    (is-stationnary-value-sequence f n) +
+    (is-strict-decreasing-value-sequence-ℕ f n)
+  decide-is-stationnary-is-decreasing-value-sequence-ℕ H =
+    map-coproduct inv id (eq-or-le-leq-ℕ (f (succ-ℕ n)) (f n) H)
+```
+
+### Any value of a decreasing sequence of natural numbers that is not a strict value is stationnary
+
+```agda
+module _
+  (f : sequence ℕ)
+  where
+
+  stationnary-value-is-not-strict-value-decreasing-sequence-ℕ :
+    is-decreasing-sequence-ℕ f →
+    (n : ℕ) →
+    ¬ (is-strict-decreasing-value-sequence-ℕ f n) →
+    is-stationnary-value-sequence f n
+  stationnary-value-is-not-strict-value-decreasing-sequence-ℕ H n K =
+    map-right-unit-law-coproduct-is-empty
+      ( is-stationnary-value-sequence f n)
+      ( is-strict-decreasing-value-sequence-ℕ f n)
+      ( K)
+      ( decide-is-stationnary-is-decreasing-value-sequence-ℕ
+        ( f)
+        ( n)
+        ( decreasing-value-is-decreasing-sequence-poset ℕ-Poset {f} H n))
+```
+
+### A decreasing sequence of natural numbers that has no strictly decreasing value is constant
+
+```agda
+module _
+  {f : sequence ℕ} (H : is-decreasing-sequence-ℕ f)
+  where
+
+  constant-no-strict-decreasing-value-decreasing-sequence-ℕ :
+    ((n : ℕ) → ¬ (is-strict-decreasing-value-sequence-ℕ f n)) →
+    is-constant-sequence f
+  constant-no-strict-decreasing-value-decreasing-sequence-ℕ K =
+    is-constant-is-stationnary-value-sequence f
+      ( λ n →
+        stationnary-value-is-not-strict-value-decreasing-sequence-ℕ
+          ( f)
+          ( H)
+          ( n)
+          ( K n))
+```
+
+### A decreasing sequence of natural numbers that asymptotically has no strictly decreasing value is asymptotically constant
+
+```agda
+module _
+  {f : sequence ℕ} (H : is-decreasing-sequence-ℕ f)
+  where
+
+  ∞-constant-∞-no-strict-value-decreasing-sequence-ℕ :
+    asymptotically (λ n → ¬ (is-strict-decreasing-value-sequence-ℕ f n)) →
+    is-∞-constant-sequence f
+  ∞-constant-∞-no-strict-value-decreasing-sequence-ℕ =
+    ( ∞-constant-is-∞-stationnary-sequence f) ∘
+    ( map-asymptotically-Π
+      ( stationnary-value-is-not-strict-value-decreasing-sequence-ℕ f H))
+```
+
+### A decreasing sequence of natural numbers with bounded strictly decreasing values is asymptotically constant
+
+```agda
+module _
+  (f : sequence ℕ) (N : ℕ)
+  where
+
+  is-upper-bound-strict-decreasing-value-sequence-ℕ : UU lzero
+  is-upper-bound-strict-decreasing-value-sequence-ℕ =
+    (n : ℕ) → is-strict-decreasing-value-sequence-ℕ f n → le-ℕ n N
+
+module _
+  {f : sequence ℕ} (H : is-decreasing-sequence-ℕ f)
+  where
+
+  ∞-constant-is-upper-bounded-strict-value-decreasing-sequence-ℕ :
+    Σ ℕ (is-upper-bound-strict-decreasing-value-sequence-ℕ f) →
+    is-∞-constant-sequence f
+  ∞-constant-is-upper-bounded-strict-value-decreasing-sequence-ℕ =
+    ( ∞-constant-∞-no-strict-value-decreasing-sequence-ℕ H) ∘
+    ( rec-Σ (λ N I → (N , (λ n J L → contradiction-le-ℕ n N (I n L) J))))
+```
+
+### Asymptotical strictly decreasing values
+
+```agda
+module _
+  (f : sequence ℕ) (N n : ℕ)
+  where
+
+  is-∞-strict-decreasing-value-prop-sequence-ℕ : Prop lzero
+  is-∞-strict-decreasing-value-prop-sequence-ℕ =
+    product-Prop
+      (leq-ℕ-Prop N n)
+      (is-strict-decreasing-value-prop-sequence-ℕ f n)
+
+  is-∞-strict-decreasing-value-sequence-ℕ : UU lzero
+  is-∞-strict-decreasing-value-sequence-ℕ =
+    type-Prop is-∞-strict-decreasing-value-prop-sequence-ℕ
+
+  is-prop-is-∞-strict-decreasing-value-sequence-ℕ :
+    is-prop is-∞-strict-decreasing-value-sequence-ℕ
+  is-prop-is-∞-strict-decreasing-value-sequence-ℕ =
+    is-prop-type-Prop is-∞-strict-decreasing-value-prop-sequence-ℕ
+```
+
+### A decreasing sequence of natural numbers with no asymptotical strictly decreasing values is asymptotically constant
+
+```agda
+module _
+  {f : sequence ℕ} (H : is-decreasing-sequence-ℕ f)
+  where
+
+  ∞-constant-no-∞-strict-decreasing-value-decreasing-sequence-ℕ :
+    Σ ℕ (λ N → ¬ Σ ℕ (is-∞-strict-decreasing-value-sequence-ℕ f N)) →
+    is-∞-constant-sequence f
+  ∞-constant-no-∞-strict-decreasing-value-decreasing-sequence-ℕ =
+    ( ∞-constant-∞-no-strict-value-decreasing-sequence-ℕ H) ∘
+    ( tot (λ n K p I J → K (p , ( I , J))))
+```
+
+### A decreasing sequence of natural numbers cannot have arbitrarily large strict decreasing values
+
+```agda
+module _
+  {f : sequence ℕ} (H : is-decreasing-sequence-ℕ f)
+  (K : (N : ℕ) → Σ ℕ (is-∞-strict-decreasing-value-sequence-ℕ f N))
+  where
+
+  extract-∞-strict-decreasing-value-sequence-ℕ : ℕ → ℕ
+  extract-∞-strict-decreasing-value-sequence-ℕ zero-ℕ = pr1 (K zero-ℕ)
+  extract-∞-strict-decreasing-value-sequence-ℕ (succ-ℕ n) =
+    pr1 (K (succ-ℕ (extract-∞-strict-decreasing-value-sequence-ℕ n)))
+
+  is-strict-value-∞-strict-decreasing-value-sequence-ℕ :
+    (n : ℕ) →
+    is-strict-decreasing-value-sequence-ℕ f
+      (extract-∞-strict-decreasing-value-sequence-ℕ n)
+  is-strict-value-∞-strict-decreasing-value-sequence-ℕ zero-ℕ =
+    pr2 (pr2 (K zero-ℕ))
+  is-strict-value-∞-strict-decreasing-value-sequence-ℕ (succ-ℕ n) =
+    pr2 (pr2 (K (succ-ℕ (extract-∞-strict-decreasing-value-sequence-ℕ n))))
+
+  leq-succ-extract-∞-strict-decreasing-value-sequence-ℕ :
+    (n : ℕ) →
+    leq-ℕ
+      (succ-ℕ (extract-∞-strict-decreasing-value-sequence-ℕ n))
+      (extract-∞-strict-decreasing-value-sequence-ℕ (succ-ℕ n))
+  leq-succ-extract-∞-strict-decreasing-value-sequence-ℕ n =
+    pr1
+      ( pr2
+        ( K
+          ( succ-ℕ
+            ( extract-∞-strict-decreasing-value-sequence-ℕ n))))
+
+  no-∞-strict-decreasing-value-decreasing-sequence-ℕ : empty
+  no-∞-strict-decreasing-value-decreasing-sequence-ℕ =
+    no-strict-decreasing-value-sequence-ℕ
+      ( f ∘ extract-∞-strict-decreasing-value-sequence-ℕ)
+      ( λ n →
+        concatenate-leq-le-ℕ
+        { f (extract-∞-strict-decreasing-value-sequence-ℕ (succ-ℕ n))}
+        { f (succ-ℕ (extract-∞-strict-decreasing-value-sequence-ℕ n))}
+        { f (extract-∞-strict-decreasing-value-sequence-ℕ n)}
+        ( H
+          ( succ-ℕ (extract-∞-strict-decreasing-value-sequence-ℕ n))
+          ( extract-∞-strict-decreasing-value-sequence-ℕ (succ-ℕ n))
+        ( leq-succ-extract-∞-strict-decreasing-value-sequence-ℕ n))
+        ( is-strict-value-∞-strict-decreasing-value-sequence-ℕ n))
+```
+
+### The subsequences of a decreasing sequence of natural numbers don't all have a strict decreasing value
+
+```agda
+module _
+  {u : sequence ℕ} (H : is-decreasing-sequence-ℕ u)
+  (K : Π-subsequence (Σ ℕ ∘ is-strict-decreasing-value-sequence-ℕ) u)
+  where
+
+  extract-strict-decreasing-value-subsequence-ℕ : ℕ → ℕ
+  extract-strict-decreasing-value-subsequence-ℕ zero-ℕ =
+    pr1 (K (refl-subsequence u))
+  extract-strict-decreasing-value-subsequence-ℕ (succ-ℕ n) =
+    skip-ℕ
+      ( extract-strict-decreasing-value-subsequence-ℕ n)
+      ( pr1
+        ( K
+          ( skip-subsequence
+            ( extract-strict-decreasing-value-subsequence-ℕ n)
+            ( u))))
+
+  is-strict-value-extract-strict-decreasing-value-subsequence-ℕ :
+    (n : ℕ) →
+    is-strict-decreasing-value-sequence-ℕ u
+      (extract-strict-decreasing-value-subsequence-ℕ n)
+  is-strict-value-extract-strict-decreasing-value-subsequence-ℕ zero-ℕ =
+    pr2 (K (refl-subsequence u))
+  is-strict-value-extract-strict-decreasing-value-subsequence-ℕ (succ-ℕ n) =
+    pr2
+      ( K
+        ( skip-subsequence
+          ( extract-strict-decreasing-value-subsequence-ℕ n)
+          ( u)))
+
+  no-strict-decreasing-value-Π-subsequence-ℕ : empty
+  no-strict-decreasing-value-Π-subsequence-ℕ =
+    no-strict-decreasing-value-sequence-ℕ
+      ( u ∘ extract-strict-decreasing-value-subsequence-ℕ)
+      ( λ n →
+        concatenate-leq-le-ℕ
+        { u (extract-strict-decreasing-value-subsequence-ℕ (succ-ℕ n))}
+        { u (succ-ℕ (extract-strict-decreasing-value-subsequence-ℕ n))}
+        { u (extract-strict-decreasing-value-subsequence-ℕ n)}
+        ( H
+          ( succ-ℕ (extract-strict-decreasing-value-subsequence-ℕ n))
+          ( skip-ℕ
+            ( extract-strict-decreasing-value-subsequence-ℕ n)
+            ( pr1
+              ( K
+              ( strict-increasing-skip-ℕ
+                ( extract-strict-decreasing-value-subsequence-ℕ n)))))
+          ( leq-add-ℕ
+            ( extract-strict-decreasing-value-subsequence-ℕ n)
+            ( pr1
+              ( K
+              ( strict-increasing-skip-ℕ
+                ( extract-strict-decreasing-value-subsequence-ℕ n))))))
+        ( is-strict-value-extract-strict-decreasing-value-subsequence-ℕ n))
+```
+
+### Decreasing sequences of natural numbers have arbitrarily long stationnary intervals
+
+```agda
+stationnary-interval-bounded-decreasing-sequence-ℕ :
+    (u : sequence ℕ) (H : is-decreasing-sequence-ℕ u) (M : ℕ) →
+    (leq-ℕ (u zero-ℕ) M) →
+    ((p : ℕ) → Σ ℕ (λ n → u (p +ℕ n) ＝ u n))
+stationnary-interval-bounded-decreasing-sequence-ℕ u H zero-ℕ I p =
+  ( zero-ℕ ,
+    antisymmetric-leq-ℕ
+      ( u p)
+      ( u zero-ℕ)
+      ( H zero-ℕ p (leq-zero-ℕ p))
+      ( transitive-leq-ℕ (u 0) 0 (u p) (leq-zero-ℕ (u p)) I))
+stationnary-interval-bounded-decreasing-sequence-ℕ u H (succ-ℕ M) I p =
+  rec-coproduct
+    ( λ J → (zero-ℕ , J))
+    ( λ J →
+      rec-Σ
+        ( λ k H → (skip-ℕ p k , H))
+        ( stationnary-interval-bounded-decreasing-sequence-ℕ
+          ( sequence-subsequence u (skip-subsequence p u))
+          ( decreasing-Π-subsequence-decreasing-sequence-poset
+            ( ℕ-Poset)
+            ( u)
+            ( H)
+            ( skip-subsequence p u))
+          ( M)
+          ( transitive-leq-ℕ
+            ( u (succ-ℕ p))
+            ( u p)
+            ( M)
+            ( leq-le-succ-ℕ
+              ( u p)
+              ( M)
+              ( concatenate-le-leq-ℕ {u p} {u 0} {succ-ℕ M} J I))
+              ( H p (succ-ℕ p) (succ-leq-ℕ p)))
+          ( p)))
+    ( eq-or-le-leq-ℕ
+      ( u p)
+      ( u zero-ℕ)
+      ( H zero-ℕ p (leq-zero-ℕ p)))
+
+module _
+  {u : sequence ℕ} (H : is-decreasing-sequence-ℕ u)
+  where
+
+  stationnary-interval-decreasing-sequence-ℕ :
+    (p : ℕ) → Σ ℕ (λ n → u (p +ℕ n) ＝ u n)
+  stationnary-interval-decreasing-sequence-ℕ =
+    stationnary-interval-bounded-decreasing-sequence-ℕ
+      ( u)
+      ( H)
+      ( u 0)
+      ( refl-leq-ℕ (u 0))
+```
+
+## External links
+
+- [Decreasing sequences of natural numbers](https://ncatlab.org/nlab/show/natural+number#decreasing_sequences_of_natural_numbers)
+  at $n$Lab
diff --git a/src/elementary-number-theory/increasing-sequences-natural-numbers.lagda.md b/src/elementary-number-theory/increasing-sequences-natural-numbers.lagda.md
new file mode 100644
index 0000000000..bdc7711943
--- /dev/null
+++ b/src/elementary-number-theory/increasing-sequences-natural-numbers.lagda.md
@@ -0,0 +1,97 @@
+# Increasing sequences of natural numbers
+
+```agda
+module elementary-number-theory.increasing-sequences-natural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
+open import elementary-number-theory.strictly-increasing-sequences-natural-numbers
+
+open import foundation.constant-sequences
+open import foundation.coproduct-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.type-arithmetic-empty-type
+open import foundation.universe-levels
+
+open import order-theory.increasing-sequences-posets
+open import order-theory.sequences-posets
+```
+
+</details>
+
+## Idea
+
+A sequence of natural numbers is **increasing** if it preserves
+[inequality of natural numbers](elementary-number-theory.inequality-natural-numbers.md).
+
+## Definitions
+
+### Increasing values of sequences of natural numbers
+
+```agda
+module _
+  (f : sequence ℕ) (n : ℕ)
+  where
+
+  is-increasing-value-sequence-ℕ : UU lzero
+  is-increasing-value-sequence-ℕ =
+    is-increasing-value-sequence-poset ℕ-Poset f n
+```
+
+### Increasing sequences of natural numbers
+
+```agda
+module _
+  (f : sequence ℕ)
+  where
+
+  is-increasing-sequence-ℕ : UU lzero
+  is-increasing-sequence-ℕ = is-increasing-sequence-poset ℕ-Poset f
+```
+
+## Properties
+
+### An increasing value of a sequence of natural numbers is either stationnary or strictly increasing
+
+```agda
+module _
+  (f : sequence ℕ) (n : ℕ)
+  where
+
+  decide-is-stationnary-is-increasing-value-sequence-ℕ :
+    is-increasing-value-sequence-ℕ f n →
+    (is-stationnary-value-sequence f n) +
+    (is-strict-increasing-value-sequence-ℕ f n)
+  decide-is-stationnary-is-increasing-value-sequence-ℕ =
+    eq-or-le-leq-ℕ (f n) (f (succ-ℕ n))
+```
+
+### Any value of an increasing sequence of natural numbers that is not a strict value is stationnary
+
+```agda
+module _
+  (f : sequence ℕ)
+  where
+
+  stationnary-value-is-not-strict-value-increasing-sequence-ℕ :
+    is-increasing-sequence-ℕ f →
+    (n : ℕ) →
+    ¬ (is-strict-increasing-value-sequence-ℕ f n) →
+    is-stationnary-value-sequence f n
+  stationnary-value-is-not-strict-value-increasing-sequence-ℕ H n K =
+    map-right-unit-law-coproduct-is-empty
+      ( is-stationnary-value-sequence f n)
+      ( is-strict-increasing-value-sequence-ℕ f n)
+      ( K)
+      ( decide-is-stationnary-is-increasing-value-sequence-ℕ
+        ( f)
+        ( n)
+        ( increasing-value-is-increasing-sequence-poset ℕ-Poset {f} H n))
+```
diff --git a/src/elementary-number-theory/maximum-natural-numbers.lagda.md b/src/elementary-number-theory/maximum-natural-numbers.lagda.md
index 8e670f94dd..81be225b3f 100644
--- a/src/elementary-number-theory/maximum-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/maximum-natural-numbers.lagda.md
@@ -75,6 +75,14 @@ leq-left-leq-max-ℕ k (succ-ℕ m) zero-ℕ H = H
 leq-left-leq-max-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H =
   leq-left-leq-max-ℕ k m n H
 
+leq-left-max-ℕ : (m n : ℕ) → m ≤-ℕ (max-ℕ m n)
+leq-left-max-ℕ m n =
+  leq-left-leq-max-ℕ
+    ( max-ℕ m n)
+    ( m)
+    ( n)
+    ( refl-leq-ℕ (max-ℕ m n))
+
 leq-right-leq-max-ℕ :
   (k m n : ℕ) → (max-ℕ m n) ≤-ℕ k → n ≤-ℕ k
 leq-right-leq-max-ℕ k zero-ℕ zero-ℕ H = star
@@ -83,6 +91,14 @@ leq-right-leq-max-ℕ k (succ-ℕ m) zero-ℕ H = star
 leq-right-leq-max-ℕ (succ-ℕ k) (succ-ℕ m) (succ-ℕ n) H =
   leq-right-leq-max-ℕ k m n H
 
+leq-right-max-ℕ : (m n : ℕ) → n ≤-ℕ (max-ℕ m n)
+leq-right-max-ℕ m n =
+  leq-right-leq-max-ℕ
+    ( max-ℕ m n)
+    ( m)
+    ( n)
+    ( refl-leq-ℕ (max-ℕ m n))
+
 is-least-upper-bound-max-ℕ :
   (m n : ℕ) → is-least-binary-upper-bound-Poset ℕ-Poset m n (max-ℕ m n)
 is-least-upper-bound-max-ℕ m n =
@@ -91,8 +107,7 @@ is-least-upper-bound-max-ℕ m n =
     { m}
     { n}
     { max-ℕ m n}
-    ( leq-left-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n)) ,
-      leq-right-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n)))
+    ( leq-left-max-ℕ m n , leq-right-max-ℕ m n)
     ( λ x (H , K) → leq-max-ℕ x m n H K)
 ```
 
diff --git a/src/elementary-number-theory/strictly-decreasing-sequences-natural-numbers.lagda.md b/src/elementary-number-theory/strictly-decreasing-sequences-natural-numbers.lagda.md
new file mode 100644
index 0000000000..12e8dc2dd6
--- /dev/null
+++ b/src/elementary-number-theory/strictly-decreasing-sequences-natural-numbers.lagda.md
@@ -0,0 +1,139 @@
+# Strictly decreasing sequences of natural numbers
+
+```agda
+module elementary-number-theory.strictly-decreasing-sequences-natural-numbers 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.natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
+
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A sequences of natural numbers is **strictly decreasing** if it reverses
+[strict inequality](elementary-number-theory.strict-inequality-natural-numbers.md)
+of natural numbers.
+
+Strictly decreasing sequences of natural numbers don't exist.
+
+## Definitions
+
+### Strictly decreasing sequences of natural numbers
+
+```agda
+module _
+  (f : sequence ℕ)
+  where
+
+  is-strict-decreasing-sequence-ℕ : UU lzero
+  is-strict-decreasing-sequence-ℕ =
+    (i j : ℕ) → le-ℕ i j → le-ℕ (f j) (f i)
+```
+
+### Strict decreasing values of sequences of natural numbers
+
+```agda
+module _
+  (f : sequence ℕ) (n : ℕ)
+  where
+
+  is-strict-decreasing-value-prop-sequence-ℕ : Prop lzero
+  is-strict-decreasing-value-prop-sequence-ℕ = le-ℕ-Prop (f (succ-ℕ n)) (f n)
+
+  is-strict-decreasing-value-sequence-ℕ : UU lzero
+  is-strict-decreasing-value-sequence-ℕ =
+    type-Prop is-strict-decreasing-value-prop-sequence-ℕ
+
+  is-prop-is-strict-decreasing-value-sequence-ℕ :
+    is-prop is-strict-decreasing-value-sequence-ℕ
+  is-prop-is-strict-decreasing-value-sequence-ℕ =
+    is-prop-type-Prop is-strict-decreasing-value-prop-sequence-ℕ
+```
+
+## Properties
+
+### A sequence is strictly decreasing if and only if all its values are strictly decreasing
+
+```agda
+module _
+  (f : sequence ℕ)
+  where
+
+  strict-decreasing-value-is-strict-decreasing-sequence-ℕ :
+    is-strict-decreasing-sequence-ℕ f →
+    ((n : ℕ) → is-strict-decreasing-value-sequence-ℕ f n)
+  strict-decreasing-value-is-strict-decreasing-sequence-ℕ H n =
+    H n (succ-ℕ n) (succ-le-ℕ n)
+
+  strict-decreasing-is-strict-decreasing-value-sequence-ℕ :
+    ((n : ℕ) → is-strict-decreasing-value-sequence-ℕ f n) →
+    is-strict-decreasing-sequence-ℕ f
+  strict-decreasing-is-strict-decreasing-value-sequence-ℕ H p q I =
+    based-ind-ℕ
+      ( succ-ℕ p)
+      ( λ k → le-ℕ (f k) (f p))
+      ( H p)
+      ( λ n J → transitive-le-ℕ (f (succ-ℕ n)) (f n) (f p) (H n))
+      ( q)
+      ( leq-succ-le-ℕ p q I)
+```
+
+### There exist no strictly decreasing sequences of natural numbers
+
+```agda
+no-bounded-strict-decreasing-sequence-ℕ :
+  (f : sequence ℕ) →
+  (N : ℕ) →
+  leq-ℕ (f zero-ℕ) N →
+  is-strict-decreasing-sequence-ℕ f →
+  empty
+no-bounded-strict-decreasing-sequence-ℕ f zero-ℕ K H =
+  concatenate-le-leq-ℕ
+    { f 1}
+    { f 0}
+    { 0}
+    ( H 0 1 (succ-le-ℕ 0))
+    ( K)
+no-bounded-strict-decreasing-sequence-ℕ f (succ-ℕ N) K H =
+  no-bounded-strict-decreasing-sequence-ℕ
+    ( f ∘ succ-ℕ)
+    ( N)
+    ( leq-le-succ-ℕ
+      ( f 1)
+      ( N)
+      ( concatenate-le-leq-ℕ
+        { f 1}
+        { f 0}
+        { succ-ℕ N}
+        ( H 0 1 (succ-le-ℕ 0))
+        ( K)))
+    ( λ i j → H (succ-ℕ i) (succ-ℕ j))
+
+module _
+  (f : sequence ℕ)
+  where
+
+  no-strict-decreasing-sequence-ℕ : ¬ (is-strict-decreasing-sequence-ℕ f)
+  no-strict-decreasing-sequence-ℕ =
+    no-bounded-strict-decreasing-sequence-ℕ f (f 0) (refl-leq-ℕ (f 0))
+
+  no-strict-decreasing-value-sequence-ℕ :
+    ¬ ((n : ℕ) → is-strict-decreasing-value-sequence-ℕ f n)
+  no-strict-decreasing-value-sequence-ℕ =
+    ( no-strict-decreasing-sequence-ℕ) ∘
+    ( strict-decreasing-is-strict-decreasing-value-sequence-ℕ f)
+```
diff --git a/src/elementary-number-theory/strictly-increasing-sequences-natural-numbers.lagda.md b/src/elementary-number-theory/strictly-increasing-sequences-natural-numbers.lagda.md
new file mode 100644
index 0000000000..88284ead5f
--- /dev/null
+++ b/src/elementary-number-theory/strictly-increasing-sequences-natural-numbers.lagda.md
@@ -0,0 +1,325 @@
+# Strictly increasing sequences of natural numbers
+
+```agda
+module elementary-number-theory.strictly-increasing-sequences-natural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.based-induction-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.functoriality-coproduct-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.subtypes
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A sequences of natural numbers is **strictly increasing** if it preserves
+[strict inequality](elementary-number-theory.strict-inequality-natural-numbers.md)
+of natural numbers.
+
+The identity sequence is strictly increasing. Strictly increasing sequences of
+natural numbers are stable under composition. Strictly increasing sequences of
+natural numbers and can get arbitrarily large.
+
+## Definitions
+
+### Strictly increasing sequences of natural numbers
+
+```agda
+module _
+  (f : sequence ℕ)
+  where
+
+  is-strict-increasing-prop-sequence-ℕ : Prop lzero
+  is-strict-increasing-prop-sequence-ℕ =
+    Π-Prop ℕ
+      ( λ i →
+        Π-Prop ℕ
+          ( λ j → hom-Prop (le-ℕ-Prop i j) (le-ℕ-Prop (f i) (f j))))
+
+  is-strict-increasing-sequence-ℕ : UU lzero
+  is-strict-increasing-sequence-ℕ =
+    type-Prop is-strict-increasing-prop-sequence-ℕ
+
+  is-prop-is-strict-increasing-sequence-ℕ :
+    is-prop is-strict-increasing-sequence-ℕ
+  is-prop-is-strict-increasing-sequence-ℕ =
+    is-prop-type-Prop is-strict-increasing-prop-sequence-ℕ
+```
+
+### The type of strictly increasing sequences of natural numbers
+
+```agda
+strict-increasing-sequence-ℕ : UU lzero
+strict-increasing-sequence-ℕ = type-subtype is-strict-increasing-prop-sequence-ℕ
+
+module _
+  (f : strict-increasing-sequence-ℕ)
+  where
+
+  sequence-strict-increasing-sequence-ℕ : sequence ℕ
+  sequence-strict-increasing-sequence-ℕ = pr1 f
+
+  is-strict-increasing-sequence-strict-increasing-sequence-ℕ :
+    is-strict-increasing-sequence-ℕ
+      sequence-strict-increasing-sequence-ℕ
+  is-strict-increasing-sequence-strict-increasing-sequence-ℕ = pr2 f
+```
+
+### Strictly increasing values of a sequence of natural numbers
+
+```agda
+module _
+  (f : sequence ℕ) (n : ℕ)
+  where
+
+  is-strict-increasing-value-prop-sequence-ℕ : Prop lzero
+  is-strict-increasing-value-prop-sequence-ℕ = le-ℕ-Prop (f n) (f (succ-ℕ n))
+
+  is-strict-increasing-value-sequence-ℕ : UU lzero
+  is-strict-increasing-value-sequence-ℕ =
+    type-Prop is-strict-increasing-value-prop-sequence-ℕ
+
+  is-prop-is-strict-increasing-value-sequence-ℕ :
+    is-prop is-strict-increasing-value-sequence-ℕ
+  is-prop-is-strict-increasing-value-sequence-ℕ =
+    is-prop-type-Prop is-strict-increasing-value-prop-sequence-ℕ
+```
+
+## Properties
+
+### A sequence of natural numbers is strictly invceasing if and only if all its values are strictly increasing
+
+```agda
+module _
+  (f : sequence ℕ)
+  where
+
+  strict-increasing-value-is-strict-increasing-sequence-ℕ :
+    is-strict-increasing-sequence-ℕ f →
+    ((n : ℕ) → is-strict-increasing-value-sequence-ℕ f n)
+  strict-increasing-value-is-strict-increasing-sequence-ℕ H n =
+    H n (succ-ℕ n) (succ-le-ℕ n)
+
+  strict-increasing-is-strict-increasing-value-sequence-ℕ :
+    ((n : ℕ) → is-strict-increasing-value-sequence-ℕ f n) →
+    is-strict-increasing-sequence-ℕ f
+  strict-increasing-is-strict-increasing-value-sequence-ℕ H p q I =
+    based-ind-ℕ
+      ( succ-ℕ p)
+      ( λ k → le-ℕ (f p) (f k))
+      ( H p)
+      ( λ n J K → transitive-le-ℕ (f p) (f n) (f (succ-ℕ n)) K ((H n)))
+      ( q)
+      ( leq-succ-le-ℕ p q I)
+
+module _
+  (f : strict-increasing-sequence-ℕ) (n : ℕ)
+  where
+
+  strict-increasing-value-strict-increasing-sequence-ℕ :
+    is-strict-increasing-value-sequence-ℕ
+      (sequence-strict-increasing-sequence-ℕ f)
+      (n)
+  strict-increasing-value-strict-increasing-sequence-ℕ =
+    strict-increasing-value-is-strict-increasing-sequence-ℕ
+      ( sequence-strict-increasing-sequence-ℕ f)
+      ( is-strict-increasing-sequence-strict-increasing-sequence-ℕ f)
+      ( n)
+```
+
+### Strictly increasing sequences of natural numbers preserve inequality
+
+```agda
+module _
+  (f : strict-increasing-sequence-ℕ) (p q : ℕ)
+  where
+
+  preserves-leq-strict-increasing-sequence-ℕ :
+    leq-ℕ p q →
+    leq-ℕ
+      (sequence-strict-increasing-sequence-ℕ f p)
+      (sequence-strict-increasing-sequence-ℕ f q)
+  preserves-leq-strict-increasing-sequence-ℕ =
+    ( leq-eq-or-le-ℕ
+      (sequence-strict-increasing-sequence-ℕ f p)
+      (sequence-strict-increasing-sequence-ℕ f q)) ∘
+    ( map-coproduct
+      ( ap (sequence-strict-increasing-sequence-ℕ f))
+      ( is-strict-increasing-sequence-strict-increasing-sequence-ℕ
+        ( f)
+        ( p)
+        ( q))) ∘
+    ( eq-or-le-leq-ℕ p q)
+```
+
+### The identity sequence is strictly increasing
+
+```agda
+is-strict-increasing-id-ℕ : is-strict-increasing-sequence-ℕ id
+is-strict-increasing-id-ℕ i j = id
+
+strict-increasing-id-ℕ : strict-increasing-sequence-ℕ
+strict-increasing-id-ℕ = (id , is-strict-increasing-id-ℕ)
+```
+
+### The identity sequence is lesser than all strictly increasing sequences of natural numbers
+
+```agda
+module _
+  (f : strict-increasing-sequence-ℕ)
+  where
+
+  leq-id-strict-increasing-sequence-ℕ :
+    (n : ℕ) → leq-ℕ n (sequence-strict-increasing-sequence-ℕ f n)
+  leq-id-strict-increasing-sequence-ℕ =
+    ind-ℕ
+      ( leq-zero-ℕ (sequence-strict-increasing-sequence-ℕ f zero-ℕ))
+      ( λ n H →
+        leq-succ-le-ℕ
+          ( n)
+          ( sequence-strict-increasing-sequence-ℕ f (succ-ℕ n))
+          ( concatenate-leq-le-ℕ
+            { n}
+            { sequence-strict-increasing-sequence-ℕ f n}
+            { sequence-strict-increasing-sequence-ℕ f (succ-ℕ n)}
+            ( H)
+            ( is-strict-increasing-sequence-strict-increasing-sequence-ℕ
+              ( f)
+              ( n)
+              ( succ-ℕ n)
+              ( succ-le-ℕ n))))
+```
+
+### The successor function is strictly increasing
+
+```agda
+is-strict-increasing-succ-ℕ : is-strict-increasing-sequence-ℕ succ-ℕ
+is-strict-increasing-succ-ℕ i j H = H
+
+strict-increasing-succ-ℕ : strict-increasing-sequence-ℕ
+strict-increasing-succ-ℕ = (succ-ℕ , is-strict-increasing-succ-ℕ)
+```
+
+### The composition of strictly increasing sequences of natural numbers is strictly increasing
+
+```agda
+module _
+  (g f : sequence ℕ)
+  (G : is-strict-increasing-sequence-ℕ g)
+  (F : is-strict-increasing-sequence-ℕ f)
+  where
+
+  is-strict-increasing-comp-is-strict-increasing-sequence-ℕ :
+    is-strict-increasing-sequence-ℕ (g ∘ f)
+  is-strict-increasing-comp-is-strict-increasing-sequence-ℕ p q =
+    G (f p) (f q) ∘ (F p q)
+
+comp-strict-increasing-sequence-ℕ :
+  strict-increasing-sequence-ℕ →
+  strict-increasing-sequence-ℕ →
+  strict-increasing-sequence-ℕ
+comp-strict-increasing-sequence-ℕ g f =
+  ( ( sequence-strict-increasing-sequence-ℕ g) ∘
+    ( sequence-strict-increasing-sequence-ℕ f)) ,
+  ( is-strict-increasing-comp-is-strict-increasing-sequence-ℕ
+    ( sequence-strict-increasing-sequence-ℕ g)
+    ( sequence-strict-increasing-sequence-ℕ f)
+    ( is-strict-increasing-sequence-strict-increasing-sequence-ℕ g)
+    ( is-strict-increasing-sequence-strict-increasing-sequence-ℕ f))
+```
+
+### A strictly increasing sequence of natural numbers takes arbitrarily large values
+
+```agda
+module _
+  (f : strict-increasing-sequence-ℕ) (M : ℕ)
+  where
+
+  unbounded-strict-increasing-sequence-ℕ :
+    Σ ℕ (λ n → leq-ℕ M (sequence-strict-increasing-sequence-ℕ f n))
+  unbounded-strict-increasing-sequence-ℕ =
+    (M , leq-id-strict-increasing-sequence-ℕ f M)
+
+  modulus-unbounded-strict-increasing-sequence-ℕ : ℕ
+  modulus-unbounded-strict-increasing-sequence-ℕ =
+    pr1 unbounded-strict-increasing-sequence-ℕ
+
+  value-unbounded-strict-increasing-sequence-ℕ : ℕ
+  value-unbounded-strict-increasing-sequence-ℕ =
+    sequence-strict-increasing-sequence-ℕ f
+      modulus-unbounded-strict-increasing-sequence-ℕ
+
+  is-modulus-unbounded-strict-increasing-sequence-ℕ :
+    leq-ℕ M value-unbounded-strict-increasing-sequence-ℕ
+  is-modulus-unbounded-strict-increasing-sequence-ℕ =
+    pr2 unbounded-strict-increasing-sequence-ℕ
+
+  is-∞-modulus-unbounded-strict-increasing-sequence-ℕ :
+    (p : ℕ) →
+    leq-ℕ modulus-unbounded-strict-increasing-sequence-ℕ p →
+    leq-ℕ M (sequence-strict-increasing-sequence-ℕ f p)
+  is-∞-modulus-unbounded-strict-increasing-sequence-ℕ =
+    based-ind-ℕ
+      ( modulus-unbounded-strict-increasing-sequence-ℕ)
+      ( λ k → leq-ℕ M (sequence-strict-increasing-sequence-ℕ f k))
+      ( is-modulus-unbounded-strict-increasing-sequence-ℕ)
+      ( λ n I →
+        transitive-leq-ℕ
+          ( M)
+          ( sequence-strict-increasing-sequence-ℕ f n)
+          ( sequence-strict-increasing-sequence-ℕ f (succ-ℕ n))
+          ( leq-le-ℕ
+            ( sequence-strict-increasing-sequence-ℕ f n)
+            ( sequence-strict-increasing-sequence-ℕ f (succ-ℕ n))
+            ( strict-increasing-value-strict-increasing-sequence-ℕ f n)))
+```
+
+### The strictly increasing sequence of natural numbers that skips the `n + 1` first terms
+
+```agda
+skip-ℕ : ℕ → ℕ → ℕ
+skip-ℕ n m = succ-ℕ (n +ℕ m)
+
+is-strict-increasing-skip-ℕ :
+  (n : ℕ) → is-strict-increasing-sequence-ℕ (skip-ℕ n)
+is-strict-increasing-skip-ℕ n p q I =
+  concatenate-le-leq-ℕ
+    { add-ℕ n p}
+    { succ-ℕ (add-ℕ n p)}
+    { add-ℕ n q}
+    ( succ-le-ℕ (add-ℕ n p))
+    ( preserves-leq-right-add-ℕ n (succ-ℕ p) q (leq-succ-le-ℕ p q I))
+
+strict-increasing-skip-ℕ : (n : ℕ) → strict-increasing-sequence-ℕ
+strict-increasing-skip-ℕ n = (skip-ℕ n , is-strict-increasing-skip-ℕ n)
+
+associative-skip-ℕ : (i j k : ℕ) →
+  skip-ℕ (skip-ℕ i j) k ＝ skip-ℕ i (skip-ℕ j k)
+associative-skip-ℕ i j k =
+  ap
+    ( succ-ℕ)
+    ( ( left-successor-law-add-ℕ (i +ℕ j) k) ∙
+      ( ap succ-ℕ (associative-add-ℕ i j k)))
+
+le-skip-ℕ : (m n : ℕ) → le-ℕ m (skip-ℕ m n)
+le-skip-ℕ m n = le-succ-leq-ℕ m (m +ℕ n) (leq-add-ℕ m n)
+
+le-skip-ℕ' : (m n : ℕ) → le-ℕ m (skip-ℕ n m)
+le-skip-ℕ' m n = le-succ-leq-ℕ m (n +ℕ m) (leq-add-ℕ' m n)
+```
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index fa4a82900e..3fda099193 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -26,6 +26,10 @@ open import foundation.action-on-identifications-functions public
 open import foundation.apartness-relations public
 open import foundation.arithmetic-law-coproduct-and-sigma-decompositions public
 open import foundation.arithmetic-law-product-and-pi-decompositions public
+open import foundation.asymptotical-dependent-sequences public
+open import foundation.asymptotical-value-sequences public
+open import foundation.asymptotically-constant-sequences public
+open import foundation.asymptotically-equal-sequences public
 open import foundation.automorphisms public
 open import foundation.axiom-of-choice public
 open import foundation.bands public
@@ -81,6 +85,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.contractible-maps public
@@ -371,6 +376,7 @@ open import foundation.strongly-extensional-maps public
 open import foundation.structure public
 open import foundation.structure-identity-principle public
 open import foundation.structured-type-duality public
+open import foundation.subsequences public
 open import foundation.subsingleton-induction public
 open import foundation.subterminal-types public
 open import foundation.subtype-duality public
diff --git a/src/foundation/asymptotical-dependent-sequences.lagda.md b/src/foundation/asymptotical-dependent-sequences.lagda.md
new file mode 100644
index 0000000000..5cd16ca8e6
--- /dev/null
+++ b/src/foundation/asymptotical-dependent-sequences.lagda.md
@@ -0,0 +1,157 @@
+# Asymptotical dependent sequences
+
+```agda
+module foundation.asymptotical-dependent-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.dependent-sequences
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A dependent sequence `A : ℕ → UU l` is **asymptotical** if `A n` is pointed for
+sufficiently large natural numbers `n`.
+
+## Definitions
+
+### Asymptotical dependent sequences
+
+```agda
+module _
+  {l : Level} (A : ℕ → UU l)
+  where
+
+  is-modulus-dependent-sequence : ℕ → UU l
+  is-modulus-dependent-sequence N = (n : ℕ) → leq-ℕ N n → A n
+
+  asymptotically : UU l
+  asymptotically = Σ ℕ is-modulus-dependent-sequence
+```
+
+### Modulus of an asymptotical dependent sequence
+
+```agda
+module _
+  {l : Level} {A : ℕ → UU l} (H : asymptotically A)
+  where
+
+  modulus-∞-asymptotically : ℕ
+  modulus-∞-asymptotically = pr1 H
+
+  is-modulus-∞-asymptotically :
+    is-modulus-dependent-sequence A modulus-∞-asymptotically
+  is-modulus-∞-asymptotically = pr2 H
+
+  value-∞-asymptotically : A modulus-∞-asymptotically
+  value-∞-asymptotically =
+    is-modulus-∞-asymptotically
+      ( modulus-∞-asymptotically)
+      ( refl-leq-ℕ modulus-∞-asymptotically)
+```
+
+## Properties
+
+### Pointed dependent sequences are asymptotical
+
+```agda
+module _
+  {l : Level} {A : ℕ → UU l}
+  where
+
+  asymptotically-Π : ((n : ℕ) → A n) → asymptotically A
+  asymptotically-Π u = (zero-ℕ , λ p I → u p)
+```
+
+### Any natural number greater than an asymptotical modulus is an asymptotical modulus
+
+```agda
+module _
+  {l : Level} (A : ℕ → UU l) (i j : ℕ) (I : leq-ℕ i j)
+  where
+
+  is-increasing-is-modulus-dependent-sequence :
+    (is-modulus-dependent-sequence A i) → (is-modulus-dependent-sequence A j)
+  is-increasing-is-modulus-dependent-sequence H k K =
+    H k (transitive-leq-ℕ i j k K I)
+```
+
+### A dependent sequence that asymptotically has an asymptotical modulus is asymptotical
+
+```agda
+module _
+  {l : Level} (A : ℕ → UU l)
+  where
+
+  asymptotically-is-modulus-dependent-sequence :
+    asymptotically (is-modulus-dependent-sequence A) →
+    asymptotically A
+  asymptotically-is-modulus-dependent-sequence (N , H) =
+    (N , (λ n K → H n K n (refl-leq-ℕ n)))
+```
+
+### Asymptotical functorial action on asymptotical dependent sequences
+
+```agda
+module _
+  {l1 l2 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2}
+  where
+
+  map-asymptotically :
+    asymptotically (λ n → A n → B n) →
+    asymptotically A →
+    asymptotically B
+  map-asymptotically H K =
+    ( max-ℕ (modulus-∞-asymptotically H) (modulus-∞-asymptotically K)) ,
+    ( λ q I →
+      is-modulus-∞-asymptotically H q
+        ( leq-left-leq-max-ℕ q
+          ( modulus-∞-asymptotically H)
+          ( modulus-∞-asymptotically K)
+          ( I))
+        ( is-modulus-∞-asymptotically K q
+          ( leq-right-leq-max-ℕ q
+            ( modulus-∞-asymptotically H)
+            ( modulus-∞-asymptotically K)
+            ( I))))
+
+  map-asymptotically-Π :
+    ((n : ℕ) → A n → B n) →
+    asymptotically A →
+    asymptotically B
+  map-asymptotically-Π = map-asymptotically ∘ asymptotically-Π
+```
+
+### Asymptotical binary functorial action on asymptotical dependent sequences
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2} {C : ℕ → UU l3}
+  where
+
+  map-binary-asymptotically :
+    asymptotically (λ n → A n → B n → C n) →
+    asymptotically A →
+    asymptotically B →
+    asymptotically C
+  map-binary-asymptotically I = map-asymptotically ∘ (map-asymptotically I)
+
+  map-binary-asymptotically-Π :
+    ((n : ℕ) → A n → B n → C n) →
+    asymptotically A →
+    asymptotically B →
+    asymptotically C
+  map-binary-asymptotically-Π = map-binary-asymptotically ∘ asymptotically-Π
+```
diff --git a/src/foundation/asymptotical-value-sequences.lagda.md b/src/foundation/asymptotical-value-sequences.lagda.md
new file mode 100644
index 0000000000..1f5e943365
--- /dev/null
+++ b/src/foundation/asymptotical-value-sequences.lagda.md
@@ -0,0 +1,123 @@
+# Asymptotical value of a sequence
+
+```agda
+module foundation.asymptotical-value-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 elementary-number-theory.strictly-increasing-sequences-natural-numbers
+
+open import foundation.asymptotical-dependent-sequences
+open import foundation.asymptotically-equal-sequences
+open import foundation.constant-sequences
+open import foundation.dependent-pair-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.subsequences
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A sequence `u` in a type `A` has an **asymptotical value** `x : A` if `x ＝ u n`
+for sufficiently large natural numbers `n`.
+
+## Definitions
+
+### Asymptotical values of sequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A) (u : sequence A)
+  where
+
+  is-∞-value-sequence : UU l
+  is-∞-value-sequence = asymptotically (is-value-sequence x u)
+```
+
+### Modulus of an asymptotical value of a sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} {x : A} {u : sequence A} (H : is-∞-value-sequence x u)
+  where
+
+  modulus-∞-value-sequence : ℕ
+  modulus-∞-value-sequence = pr1 H
+
+  is-modulus-∞-value-sequence :
+    (n : ℕ) → leq-ℕ modulus-∞-value-sequence n → x ＝ u n
+  is-modulus-∞-value-sequence = pr2 H
+```
+
+## Properties
+
+### Asymptotical values are unique
+
+```agda
+module _
+  {l : Level} {A : UU l} (x y : A) (u : sequence A)
+  (H : is-∞-value-sequence x u) (K : is-∞-value-sequence y u)
+  where
+
+  all-eq-∞-value-sequence : x ＝ y
+  all-eq-∞-value-sequence =
+    value-∞-asymptotically
+      (map-binary-asymptotically-Π (λ n I J → I ∙ (inv J)) H K)
+```
+
+### A sequence has an asymptotical value if and only if it is asymptotically equal to some constant sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A) (u : sequence A)
+  where
+
+  eq-∞-const-sequence-is-∞-value-sequence :
+    is-∞-value-sequence x u → eq-∞-sequence (const-sequence x) u
+  eq-∞-const-sequence-is-∞-value-sequence = tot (λ n K → K)
+
+  is-∞-value-eq-∞-constant-sequence :
+    eq-∞-sequence (const-sequence x) u → is-∞-value-sequence x u
+  is-∞-value-eq-∞-constant-sequence = tot (λ n K → K)
+```
+
+### Asymptotical equality preserves asymptotical value
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A) (u v : sequence A)
+  where
+
+  preserves-∞-value-eq-∞-sequence :
+    eq-∞-sequence u v → is-∞-value-sequence x u → is-∞-value-sequence x v
+  preserves-∞-value-eq-∞-sequence =
+    map-binary-asymptotically-Π (λ n I H → H ∙ I)
+```
+
+### The asymptotical value of a sequence is an asymptotical value of all it subsequences
+
+```agda
+module _
+  {l : Level} {A : UU l} {x : A} {u : sequence A} (H : is-∞-value-sequence x u)
+  where
+
+  Π-subsequence-∞-value-sequence : Π-subsequence (is-∞-value-sequence x) u
+  Π-subsequence-∞-value-sequence v =
+    ( modulus-subsequence u v (modulus-∞-value-sequence H)) ,
+    ( λ n I →
+      is-modulus-∞-value-sequence
+        ( H)
+        ( extract-subsequence u v n)
+        ( is-modulus-subsequence u v (modulus-∞-value-sequence H) n I))
+```
diff --git a/src/foundation/asymptotically-constant-sequences.lagda.md b/src/foundation/asymptotically-constant-sequences.lagda.md
new file mode 100644
index 0000000000..07fc4e0185
--- /dev/null
+++ b/src/foundation/asymptotically-constant-sequences.lagda.md
@@ -0,0 +1,320 @@
+# Asymptotically constant sequences
+
+```agda
+module foundation.asymptotically-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 elementary-number-theory.strictly-increasing-sequences-natural-numbers
+
+open import foundation.asymptotical-dependent-sequences
+open import foundation.asymptotical-value-sequences
+open import foundation.asymptotically-equal-sequences
+open import foundation.constant-sequences
+open import foundation.dependent-pair-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.subsequences
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A sequence `u` is **asymptotically constant** if `u p ＝ u q` for sufficiently
+large `p` and `q`.
+
+## Definitions
+
+### Asymptotically constant sequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-∞-constant-sequence : UU l
+  is-∞-constant-sequence =
+    asymptotically (λ p → asymptotically (λ q → u p ＝ u q))
+```
+
+### The asymptotical value of an asymptotically 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 (modulus-∞-asymptotically H)
+
+  is-∞-value-∞-constant-sequence :
+    is-∞-value-sequence ∞-value-∞-constant-sequence u
+  is-∞-value-∞-constant-sequence = value-∞-asymptotically H
+
+  modulus-∞-value-∞-constant-sequence : ℕ
+  modulus-∞-value-∞-constant-sequence =
+    modulus-∞-asymptotically is-∞-value-∞-constant-sequence
+
+  is-modulus-∞-value-∞-constant-sequence :
+    (n : ℕ) →
+    leq-ℕ modulus-∞-value-∞-constant-sequence n →
+    ∞-value-∞-constant-sequence ＝ u n
+  is-modulus-∞-value-∞-constant-sequence =
+    is-modulus-∞-asymptotically is-∞-value-∞-constant-sequence
+
+  const-∞-value-∞-constant-sequence : sequence A
+  const-∞-value-∞-constant-sequence n = ∞-value-∞-constant-sequence
+```
+
+## Properties
+
+### Constant sequences are asymptotically constant
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A} (H : is-constant-sequence u)
+  where
+
+  ∞-constant-is-constant-sequence : is-∞-constant-sequence u
+  pr1 ∞-constant-is-constant-sequence = zero-ℕ
+  pr2 ∞-constant-is-constant-sequence p I = (zero-ℕ , λ q J → H p q)
+```
+
+### The asymptotical value of an asymptotically constant sequence is unique
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A}
+  (H K : is-∞-constant-sequence u)
+  where
+
+  all-equal-∞-value-∞-constant-sequence :
+    ∞-value-∞-constant-sequence H ＝ ∞-value-∞-constant-sequence K
+  all-equal-∞-value-∞-constant-sequence =
+    all-eq-∞-value-sequence
+      ( ∞-value-∞-constant-sequence H)
+      ( ∞-value-∞-constant-sequence K)
+      ( u)
+      ( is-∞-value-∞-constant-sequence H)
+      ( is-∞-value-∞-constant-sequence K)
+```
+
+### A sequence is asymptotically constant if it has some asymptotical value
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A) (u : sequence A)
+  where
+
+  ∞-constant-is-∞-value-sequence :
+    is-∞-value-sequence x u → is-∞-constant-sequence u
+  ∞-constant-is-∞-value-sequence H =
+    ( modulus-∞-value-sequence H) ,
+    ( λ p I →
+      ( modulus-∞-value-sequence H) ,
+      ( λ q J →
+        ( inv (is-modulus-∞-value-sequence H p I)) ∙
+        ( is-modulus-∞-value-sequence H q J)))
+```
+
+### An asymptotically constant sequence is asymptotically equal to the constant sequence of its asymptotical value
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A} (H : is-∞-constant-sequence u)
+  where
+
+  eq-∞-value-∞-constant-sequence :
+    eq-∞-sequence (const-∞-value-∞-constant-sequence H) u
+  eq-∞-value-∞-constant-sequence =
+    ( modulus-∞-value-∞-constant-sequence H) ,
+    ( is-modulus-∞-value-∞-constant-sequence H)
+
+  eq-∞-value-∞-constant-sequence' :
+    eq-∞-sequence u (const-∞-value-∞-constant-sequence H)
+  eq-∞-value-∞-constant-sequence' =
+    inv-eq-∞-sequence eq-∞-value-∞-constant-sequence
+```
+
+### Two asymptotically constant sequences are asymptotically equal if and only if their asymptotical value is the same
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v : sequence A)
+  (H : is-∞-constant-sequence u) (K : is-∞-constant-sequence v)
+  where
+
+  eq-∞-sequence-eq-∞-value-∞-constant-sequence :
+    (∞-value-∞-constant-sequence H) ＝ (∞-value-∞-constant-sequence K) →
+    eq-∞-sequence u v
+  eq-∞-sequence-eq-∞-value-∞-constant-sequence I =
+    conjugate-eq-∞-sequence
+      ( eq-∞-value-∞-constant-sequence H)
+      ( eq-∞-value-∞-constant-sequence K)
+      ( asymptotically-Π (λ n → I))
+
+  eq-∞-value-eq-∞-sequence-∞-constant-sequence :
+    eq-∞-sequence u v →
+    (∞-value-∞-constant-sequence H) ＝ (∞-value-∞-constant-sequence K)
+  eq-∞-value-eq-∞-sequence-∞-constant-sequence I =
+    value-∞-asymptotically
+    ( conjugate-eq-∞-sequence'
+      ( eq-∞-value-∞-constant-sequence H)
+      ( eq-∞-value-∞-constant-sequence K)
+      ( I))
+```
+
+### Any subsequence of an asymptotically constant sequence is asymptotically constant
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A) (H : is-∞-constant-sequence u)
+  where
+
+  ∞-constant-Π-subsequence : Π-subsequence is-∞-constant-sequence u
+  ∞-constant-Π-subsequence v =
+    ∞-constant-is-∞-value-sequence
+      ( ∞-value-∞-constant-sequence H)
+      ( sequence-subsequence u v)
+      ( Π-subsequence-∞-value-sequence
+        ( is-∞-value-∞-constant-sequence H)
+        ( v))
+```
+
+### A sequence asymptotically equal to an asymptotically constant sequence is asymptotically constant
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v : sequence A) (H : eq-∞-sequence u v)
+  where
+
+  preserves-∞-constant-eq-∞-sequence :
+    is-∞-constant-sequence u → is-∞-constant-sequence v
+  preserves-∞-constant-eq-∞-sequence K =
+    ∞-constant-is-∞-value-sequence
+      ( ∞-value-∞-constant-sequence K)
+      ( v)
+      ( transitive-eq-∞-sequence
+        ( const-∞-value-∞-constant-sequence K)
+        ( u)
+        ( v)
+        ( H)
+        ( eq-∞-value-∞-constant-sequence K))
+```
+
+### Asymptotically stationnary sequences
+
+#### The predicate of being asymptotically stationnary
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-∞-stationnary-sequence : UU l
+  is-∞-stationnary-sequence = asymptotically (is-stationnary-value-sequence u)
+
+  is-∞-constant-modulus-is-∞-stationnary-sequence :
+    (H : is-∞-stationnary-sequence) →
+    (n : ℕ) →
+    leq-ℕ (modulus-∞-asymptotically H) n →
+    u (modulus-∞-asymptotically H) ＝ u n
+  is-∞-constant-modulus-is-∞-stationnary-sequence H =
+    based-ind-ℕ
+      ( modulus-∞-asymptotically H)
+      ( λ n → u (modulus-∞-asymptotically H) ＝ u n)
+      ( refl)
+      ( λ n I K → K ∙ is-modulus-∞-asymptotically H n I)
+```
+
+#### A sequence is asymptotically constant if and only if it is asymptotically stationnary
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  ∞-constant-is-∞-stationnary-sequence :
+    is-∞-stationnary-sequence u → is-∞-constant-sequence u
+  ∞-constant-is-∞-stationnary-sequence H =
+    ∞-constant-is-∞-value-sequence
+      ( u (modulus-∞-asymptotically H))
+      ( u)
+      ( ( modulus-∞-asymptotically H) ,
+        ( is-∞-constant-modulus-is-∞-stationnary-sequence u H))
+
+  ∞-stationnary-is-∞-constant-sequence :
+    is-∞-constant-sequence u → is-∞-stationnary-sequence u
+  ∞-stationnary-is-∞-constant-sequence H =
+    ( ( modulus-∞-value-∞-constant-sequence H) ,
+      ( λ n I →
+        ( inv (is-modulus-∞-value-∞-constant-sequence H n I)) ∙
+        ( is-modulus-∞-value-∞-constant-sequence
+          ( H)
+          ( succ-ℕ n)
+          ( preserves-leq-succ-ℕ
+            ( modulus-∞-value-∞-constant-sequence H)
+            ( n)
+            ( I)))))
+```
+
+### A sequence is asymptotically constant if and only if it is asymptotically equal to all its subsequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  eq-∞-subsequence-is-∞-constant-sequence :
+    is-∞-constant-sequence u → Π-subsequence (eq-∞-sequence u) u
+  eq-∞-subsequence-is-∞-constant-sequence H v =
+    transitive-eq-∞-sequence
+      ( u)
+      ( const-∞-value-∞-constant-sequence H)
+      ( sequence-subsequence u v)
+      ( eq-∞-const-sequence-is-∞-value-sequence
+        ( ∞-value-∞-constant-sequence H)
+        ( sequence-subsequence u v)
+        ( Π-subsequence-∞-value-sequence (is-∞-value-∞-constant-sequence H) v))
+      ( eq-∞-value-∞-constant-sequence' H)
+
+  ∞-constant-eq-∞-sequence-subsequence :
+    Π-subsequence (eq-∞-sequence u) u → is-∞-constant-sequence u
+  ∞-constant-eq-∞-sequence-subsequence H =
+    ∞-constant-is-∞-stationnary-sequence
+      ( u)
+      ( H (skip-zero-sequence u))
+```
+
+### An asymptotically constant sequence has a constant subsequence
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A) (H : is-∞-constant-sequence u)
+  where
+
+  constant-subsequence-is-∞-constant-sequence :
+    Σ-subsequence is-constant-sequence u
+  constant-subsequence-is-∞-constant-sequence =
+    ( skip-subsequence (modulus-∞-value-∞-constant-sequence H) u) ,
+    ( λ p q →
+      ( inv
+        ( is-modulus-∞-value-∞-constant-sequence
+          ( H)
+          ( skip-ℕ (modulus-∞-value-∞-constant-sequence H) p)
+          ( leq-add-ℕ (modulus-∞-value-∞-constant-sequence H) (succ-ℕ p)))) ∙
+      ( is-modulus-∞-value-∞-constant-sequence
+        ( H)
+        ( skip-ℕ (modulus-∞-value-∞-constant-sequence H) q)
+        ( leq-add-ℕ (modulus-∞-value-∞-constant-sequence H) (succ-ℕ q))))
+```
diff --git a/src/foundation/asymptotically-equal-sequences.lagda.md b/src/foundation/asymptotically-equal-sequences.lagda.md
new file mode 100644
index 0000000000..4b5d525437
--- /dev/null
+++ b/src/foundation/asymptotically-equal-sequences.lagda.md
@@ -0,0 +1,135 @@
+# Asymptotically equal sequences
+
+```agda
+module foundation.asymptotically-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.asymptotical-dependent-sequences
+open import foundation.dependent-pair-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
+open import foundation.sequences
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Two sequences `u` and `v` are **asymptotically equal** if `u n ＝ v n` for any
+sufficiently large natural number `n`.
+
+## Definitions
+
+### The relation of being asymptotically equal sequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v : sequence A)
+  where
+
+  eq-∞-sequence : UU l
+  eq-∞-sequence = asymptotically (λ n → u n ＝ v n)
+```
+
+### Modulus of asymptotical equality
+
+```agda
+module _
+  {l : Level} {A : UU l} {u v : sequence A} (H : eq-∞-sequence u v)
+  where
+
+  modulus-eq-∞-sequence : ℕ
+  modulus-eq-∞-sequence = pr1 H
+
+  is-modulus-eq-∞-sequence :
+    (n : ℕ) → leq-ℕ modulus-eq-∞-sequence n → u n ＝ v n
+  is-modulus-eq-∞-sequence = pr2 H
+```
+
+## Properties
+
+### Any sequence is asymptotically equal to itself
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  refl-eq-∞-sequence : (u : sequence A) → eq-∞-sequence u u
+  pr1 (refl-eq-∞-sequence u) = zero-ℕ
+  pr2 (refl-eq-∞-sequence u) m H = refl
+
+  eq-∞-eq-sequence :
+    {u v : sequence A} → ((n : ℕ) → u n ＝ v n) → eq-∞-sequence u v
+  eq-∞-eq-sequence {u} {v} I = (zero-ℕ , λ n H → I n)
+```
+
+### Asymptotical equality is a symmetric relation
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v : sequence A)
+  where
+
+  symmetric-eq-∞-sequence : eq-∞-sequence u v → eq-∞-sequence v u
+  symmetric-eq-∞-sequence = map-asymptotically-Π (λ n → inv)
+
+module _
+  {l : Level} {A : UU l} {u v : sequence A}
+  where
+
+  inv-eq-∞-sequence : eq-∞-sequence u v → eq-∞-sequence v u
+  inv-eq-∞-sequence = symmetric-eq-∞-sequence u v
+```
+
+### Asymptotical equality is a transitive relation
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v w : sequence A)
+  where
+
+  transitive-eq-∞-sequence :
+    eq-∞-sequence v w →
+    eq-∞-sequence u v →
+    eq-∞-sequence u w
+  transitive-eq-∞-sequence = map-binary-asymptotically-Π (λ n I J → J ∙ I)
+```
+
+### Conjugation of asymptotical equality
+
+```agda
+module _
+  {l : Level} {A : UU l} {u u' v v' : sequence A}
+  where
+
+  conjugate-eq-∞-sequence :
+    eq-∞-sequence u u' →
+    eq-∞-sequence v v' →
+    eq-∞-sequence u v →
+    eq-∞-sequence u' v'
+  conjugate-eq-∞-sequence H K I =
+    transitive-eq-∞-sequence u' u v'
+      ( transitive-eq-∞-sequence u v v' K I)
+      ( inv-eq-∞-sequence H)
+
+  conjugate-eq-∞-sequence' :
+    eq-∞-sequence u u' →
+    eq-∞-sequence v v' →
+    eq-∞-sequence u' v' →
+    eq-∞-sequence u v
+  conjugate-eq-∞-sequence' H K I =
+    transitive-eq-∞-sequence u u' v
+      ( transitive-eq-∞-sequence u' v' v (inv-eq-∞-sequence K) I)
+      ( H)
+```
diff --git a/src/foundation/constant-sequences.lagda.md b/src/foundation/constant-sequences.lagda.md
new file mode 100644
index 0000000000..5e461cf986
--- /dev/null
+++ b/src/foundation/constant-sequences.lagda.md
@@ -0,0 +1,130 @@
+# Constant Sequences
+
+```agda
+module foundation.constant-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.sequences
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A sequence `u` is **constant** 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-ℕ
+```
+
+### The constant sequences in a type
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A)
+  where
+
+  const-sequence : sequence A
+  const-sequence n = x
+```
+
+### Constant sequences are constant
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A)
+  where
+
+  is-constant-const-sequence : is-constant-sequence (const-sequence 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-sequence 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 →
+    ((n : ℕ) → is-stationnary-value-sequence u n)
+  is-stationnary-value-is-constant-sequence H n = H n (succ-ℕ n)
+
+  is-constant-is-stationnary-value-sequence :
+    ((n : ℕ) → is-stationnary-value-sequence u n) →
+    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/dependent-sequences.lagda.md b/src/foundation/dependent-sequences.lagda.md
index 7590315c29..bc1128a8f2 100644
--- a/src/foundation/dependent-sequences.lagda.md
+++ b/src/foundation/dependent-sequences.lagda.md
@@ -35,6 +35,8 @@ dependent-sequence B = (n : ℕ) → B n
 ```agda
 map-dependent-sequence :
   {l1 l2 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2} →
-  ((n : ℕ) → A n → B n) → dependent-sequence A → dependent-sequence B
+  dependent-sequence (λ n → A n → B n) →
+  dependent-sequence A →
+  dependent-sequence B
 map-dependent-sequence f a = map-Π f a
 ```
diff --git a/src/foundation/sequences.lagda.md b/src/foundation/sequences.lagda.md
index 5a8b9fa482..a29bc3122d 100644
--- a/src/foundation/sequences.lagda.md
+++ b/src/foundation/sequences.lagda.md
@@ -7,7 +7,10 @@ module foundation.sequences where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
+
 open import foundation.dependent-sequences
+open import foundation.identity-types
 open import foundation.universe-levels
 
 open import foundation-core.function-types
@@ -28,6 +31,17 @@ sequence : {l : Level} → UU l → UU l
 sequence A = dependent-sequence (λ _ → A)
 ```
 
+### Values of a sequence
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  is-value-sequence : A → sequence A → ℕ → UU l
+  is-value-sequence x u n = x ＝ u n
+```
+
 ### Functorial action on maps of sequences
 
 ```agda
diff --git a/src/foundation/subsequences.lagda.md b/src/foundation/subsequences.lagda.md
new file mode 100644
index 0000000000..4cabe4a7e4
--- /dev/null
+++ b/src/foundation/subsequences.lagda.md
@@ -0,0 +1,236 @@
+# Subsequences
+
+```agda
+module foundation.subsequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.based-induction-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
+open import elementary-number-theory.strictly-increasing-sequences-natural-numbers
+
+open import foundation.asymptotical-dependent-sequences
+open import foundation.dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.subtypes
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A **subsequence** of a [sequence](foundation.sequences.md) `u : ℕ → A` is a
+sequence `u ∘ f` for some
+[strictly increasing](elementary-number-theory.strictly-increasing-sequences-natural-numbers.md)
+map `f : ℕ → ℕ`.
+
+## Definitions
+
+### Subsequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  subsequence : UU lzero
+  subsequence = strict-increasing-sequence-ℕ
+```
+
+### The extracted sequence of a subsequence
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A) (v : subsequence u)
+  where
+
+  extract-subsequence : ℕ → ℕ
+  extract-subsequence =
+    sequence-strict-increasing-sequence-ℕ v
+
+  is-strict-increasing-extract-subsequence :
+    is-strict-increasing-sequence-ℕ extract-subsequence
+  is-strict-increasing-extract-subsequence =
+    is-strict-increasing-sequence-strict-increasing-sequence-ℕ v
+
+  leq-id-extract-subsequence :
+    (p : ℕ) → leq-ℕ p (extract-subsequence p)
+  leq-id-extract-subsequence = leq-id-strict-increasing-sequence-ℕ v
+
+  preserves-leq-extract-subsequence :
+    (p q : ℕ) →
+    leq-ℕ p q →
+    leq-ℕ (extract-subsequence p) (extract-subsequence q)
+  preserves-leq-extract-subsequence =
+    preserves-leq-strict-increasing-sequence-ℕ v
+
+  sequence-subsequence : sequence A
+  sequence-subsequence n = u (extract-subsequence n)
+```
+
+## Properties
+
+### Any sequence is a subsequence of itself
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  refl-subsequence : subsequence u
+  refl-subsequence = strict-increasing-id-ℕ
+
+  compute-refl-subsequence : u ＝ sequence-subsequence u refl-subsequence
+  compute-refl-subsequence = refl
+```
+
+### The subsequence that skips the first term
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  skip-zero-sequence : subsequence u
+  skip-zero-sequence = strict-increasing-succ-ℕ
+
+  compute-skip-zero-sequence :
+    u ∘ succ-ℕ ＝ sequence-subsequence u skip-zero-sequence
+  compute-skip-zero-sequence = refl
+```
+
+### The subsequence that skips the `n + 1` first terms
+
+```agda
+module _
+  {l : Level} {A : UU l} (n : ℕ) (u : sequence A)
+  where
+
+  skip-subsequence : subsequence u
+  skip-subsequence = strict-increasing-skip-ℕ n
+
+  compute-skip-subsequence :
+    u ∘ (succ-ℕ ∘ add-ℕ n) ＝ sequence-subsequence u skip-subsequence
+  compute-skip-subsequence = refl
+```
+
+### A subsequence of a subsequence is a subsequence of the original sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A) (v : subsequence u)
+  (w : subsequence (sequence-subsequence u v))
+  where
+
+  sub-subsequence : subsequence u
+  sub-subsequence = comp-strict-increasing-sequence-ℕ v w
+
+  compute-sub-subsequence :
+    Id
+      (sequence-subsequence u sub-subsequence)
+      (sequence-subsequence (sequence-subsequence u v) w)
+  compute-sub-subsequence = refl
+```
+
+### Subsequences are functorial
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (u : sequence A)
+  where
+
+  map-subsequence : subsequence u → subsequence (map-sequence f u)
+  map-subsequence H = H
+```
+
+### The extracted sequence of the image of a subsequence is the extracted sequence of the image
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (u : sequence A)
+  (v : subsequence u)
+  where
+
+  compute-map-subsequence :
+    Id
+      (map-sequence f (sequence-subsequence u v))
+      (sequence-subsequence (map-sequence f u) (map-subsequence f u v))
+  compute-map-subsequence = refl
+```
+
+### Modulus of a subsequence
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A) (v : subsequence u)
+  where
+
+  modulus-subsequence : ℕ → ℕ
+  modulus-subsequence =
+    modulus-unbounded-strict-increasing-sequence-ℕ v
+
+  is-modulus-subsequence :
+    (N p : ℕ) →
+    leq-ℕ (modulus-subsequence N) p →
+    leq-ℕ N (extract-subsequence u v p)
+  is-modulus-subsequence =
+    is-∞-modulus-unbounded-strict-increasing-sequence-ℕ v
+
+  extract-modulus-subsequence : ℕ → ℕ
+  extract-modulus-subsequence = extract-subsequence u v ∘ modulus-subsequence
+
+  leq-extract-modulus-subsequence :
+    (n : ℕ) → leq-ℕ n (extract-modulus-subsequence n)
+  leq-extract-modulus-subsequence =
+    is-modulus-unbounded-strict-increasing-sequence-ℕ v
+```
+
+### Subsequential type families
+
+```agda
+module _
+  {l l1 : Level} {A : UU l} (P : sequence A → UU l1)
+  where
+
+  Π-subsequence : sequence A → UU l1
+  Π-subsequence u = (v : subsequence u) → P (sequence-subsequence u v)
+
+  sequence-Π-subsequence : (u : sequence A) → Π-subsequence u → P u
+  sequence-Π-subsequence u H = H (refl-subsequence u)
+
+  Σ-subsequence : sequence A → UU l1
+  Σ-subsequence u = Σ (subsequence u) (P ∘ (sequence-subsequence u))
+
+  sequence-Σ-subsequence : (u : sequence A) → P u → Σ-subsequence u
+  sequence-Σ-subsequence u H = (refl-subsequence u , H)
+```
+
+### A dependent sequence is asymptotical if and only if all its subsequences are asymptotical
+
+```agda
+module _
+  {l : Level} (A : ℕ → UU l) (H : asymptotically A)
+  where
+
+  asymptotically-Π-subsequence : Π-subsequence asymptotically A
+  asymptotically-Π-subsequence B =
+    map-Σ
+      ( is-modulus-dependent-sequence (sequence-subsequence A B))
+      ( modulus-subsequence A B)
+      ( λ N K p →
+        ( K (extract-subsequence A B p)) ∘
+        ( is-∞-modulus-unbounded-strict-increasing-sequence-ℕ B N p))
+      ( H)
+```
diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index 1ce9b78699..740a34857c 100644
--- a/src/order-theory.lagda.md
+++ b/src/order-theory.lagda.md
@@ -14,6 +14,7 @@ open import order-theory.closure-operators-large-locales public
 open import order-theory.closure-operators-large-posets public
 open import order-theory.commuting-squares-of-galois-connections-large-posets public
 open import order-theory.commuting-squares-of-order-preserving-maps-large-posets public
+open import order-theory.constant-sequences-posets public
 open import order-theory.coverings-locales public
 open import order-theory.decidable-posets public
 open import order-theory.decidable-preorders public
@@ -21,6 +22,7 @@ open import order-theory.decidable-subposets public
 open import order-theory.decidable-subpreorders public
 open import order-theory.decidable-total-orders public
 open import order-theory.decidable-total-preorders public
+open import order-theory.decreasing-sequences-posets public
 open import order-theory.dependent-products-large-frames public
 open import order-theory.dependent-products-large-locales public
 open import order-theory.dependent-products-large-meet-semilattices public
@@ -49,6 +51,7 @@ open import order-theory.homomorphisms-meet-semilattices public
 open import order-theory.homomorphisms-meet-sup-lattices public
 open import order-theory.homomorphisms-sup-lattices public
 open import order-theory.ideals-preorders public
+open import order-theory.increasing-sequences-posets public
 open import order-theory.inhabited-finite-total-orders public
 open import order-theory.interval-subposets public
 open import order-theory.join-semilattices public
@@ -77,6 +80,7 @@ open import order-theory.maximal-chains-posets public
 open import order-theory.maximal-chains-preorders public
 open import order-theory.meet-semilattices public
 open import order-theory.meet-suplattices public
+open import order-theory.monotonic-sequences-posets public
 open import order-theory.nuclei-large-locales public
 open import order-theory.order-preserving-maps-large-posets public
 open import order-theory.order-preserving-maps-large-preorders public
@@ -94,6 +98,7 @@ open import order-theory.preorders public
 open import order-theory.principal-lower-sets-large-posets public
 open import order-theory.principal-upper-sets-large-posets public
 open import order-theory.reflective-galois-connections-large-posets public
+open import order-theory.sequences-posets public
 open import order-theory.similarity-of-elements-large-posets public
 open import order-theory.similarity-of-elements-large-preorders public
 open import order-theory.similarity-of-order-preserving-maps-large-posets public
diff --git a/src/order-theory/constant-sequences-posets.lagda.md b/src/order-theory/constant-sequences-posets.lagda.md
new file mode 100644
index 0000000000..a49f372a54
--- /dev/null
+++ b/src/order-theory/constant-sequences-posets.lagda.md
@@ -0,0 +1,57 @@
+# Constant sequences in partially ordered sets
+
+```agda
+module order-theory.constant-sequences-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+
+open import foundation.constant-sequences
+open import foundation.coproduct-types
+open import foundation.universe-levels
+
+open import order-theory.decreasing-sequences-posets
+open import order-theory.increasing-sequences-posets
+open import order-theory.posets
+open import order-theory.sequences-posets
+```
+
+</details>
+
+## Idea
+
+A [sequence in a partially ordered set](order-theory.sequences-posets.md) is
+[constant](foundation.constant-sequences.md) if it is both
+[increasing](order-theory.increasing-sequences-posets.md) and
+[decreasing](order-theory.decreasing-sequences-posets.md).
+
+## Properties
+
+### A sequence in a partially ordered set is constant if and only if it is both increasing and decreasing
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u : sequence-poset P}
+  where
+
+  increasing-is-constant-sequence-poset :
+    is-constant-sequence u → is-increasing-sequence-poset P u
+  increasing-is-constant-sequence-poset H p q I = leq-eq-Poset P (H p q)
+
+  decreasing-is-constant-sequence-poset :
+    is-constant-sequence u → is-decreasing-sequence-poset P u
+  decreasing-is-constant-sequence-poset H p q I = leq-eq-Poset P (H q p)
+
+  constant-is-increasing-decreasing-sequence-poset :
+    is-increasing-sequence-poset P u →
+    is-decreasing-sequence-poset P u →
+    is-constant-sequence u
+  constant-is-increasing-decreasing-sequence-poset I J p q =
+    rec-coproduct
+      ( λ H → antisymmetric-leq-Poset P (u p) (u q) (I p q H) (J p q H))
+      ( λ H → antisymmetric-leq-Poset P (u p) (u q) (J q p H) (I q p H))
+      ( linear-leq-ℕ p q)
+```
diff --git a/src/order-theory/decreasing-sequences-posets.lagda.md b/src/order-theory/decreasing-sequences-posets.lagda.md
new file mode 100644
index 0000000000..75b7f92f38
--- /dev/null
+++ b/src/order-theory/decreasing-sequences-posets.lagda.md
@@ -0,0 +1,209 @@
+# Decreasing sequences in partially ordered sets
+
+```agda
+module order-theory.decreasing-sequences-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.based-induction-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strictly-increasing-sequences-natural-numbers
+
+open import foundation.asymptotical-dependent-sequences
+open import foundation.asymptotically-constant-sequences
+open import foundation.constant-sequences
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.subsequences
+open import foundation.universe-levels
+
+open import order-theory.posets
+open import order-theory.sequences-posets
+```
+
+</details>
+
+## Idea
+
+A [sequence in a partially ordered set](order-theory.sequences-posets.md) is
+**decreasing** if it reverses the
+[standard ordering on the natural numbers](elementary-number-theory.inequality-natural-numbers.md).
+
+## Definitions
+
+### Decreasing sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P)
+  where
+
+  is-decreasing-prop-sequence-poset : Prop l2
+  is-decreasing-prop-sequence-poset =
+      Π-Prop ℕ
+      ( λ i →
+        Π-Prop ℕ
+          ( λ j →
+            hom-Prop
+              ( leq-ℕ-Prop i j)
+              ( leq-Poset-Prop P (u j) (u i))))
+
+  is-decreasing-sequence-poset : UU l2
+  is-decreasing-sequence-poset =
+    type-Prop is-decreasing-prop-sequence-poset
+
+  is-prop-is-decreasing-sequence-poset :
+    is-prop is-decreasing-sequence-poset
+  is-prop-is-decreasing-sequence-poset =
+    is-prop-type-Prop is-decreasing-prop-sequence-poset
+```
+
+## Properties
+
+### A sequence in a partially ordered set is decreasing if and only if all its values are decreasing
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u : sequence-poset P}
+  where
+
+  decreasing-sequence-is-decreasing-value-sequence-poset :
+    ((n : ℕ) → is-decreasing-value-sequence-poset P u n) →
+    is-decreasing-sequence-poset P u
+  decreasing-sequence-is-decreasing-value-sequence-poset H p =
+    based-ind-ℕ
+      ( p)
+      ( λ q → leq-Poset P (u q) (u p))
+      ( refl-leq-Poset P (u p))
+      ( λ q I J →
+        transitive-leq-Poset P (u (succ-ℕ q)) (u q) (u p) J (H q))
+
+  decreasing-value-is-decreasing-sequence-poset :
+    is-decreasing-sequence-poset P u →
+    ((n : ℕ) → is-decreasing-value-sequence-poset P u n)
+  decreasing-value-is-decreasing-sequence-poset H n =
+    H n (succ-ℕ n) (succ-leq-ℕ n)
+```
+
+### Any subsequence of a decreasing sequence in a partially ordered set is decreasing
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P)
+  where
+
+  decreasing-Π-subsequence-decreasing-sequence-poset :
+    is-decreasing-sequence-poset P u →
+    Π-subsequence (is-decreasing-sequence-poset P) u
+  decreasing-Π-subsequence-decreasing-sequence-poset H v p q I =
+    H
+      ( extract-subsequence u v p)
+      ( extract-subsequence u v q)
+      ( preserves-leq-extract-subsequence u v p q I)
+```
+
+### A sequence in a partially ordered set is decreasing if and only if it is greater than all its subsequences
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P)
+  where
+
+  decreasing-Π-subsequence-leq-sequence-poset :
+    Π-subsequence (λ v → leq-sequence-poset P v u) u →
+    is-decreasing-sequence-poset P u
+  decreasing-Π-subsequence-leq-sequence-poset H =
+    decreasing-sequence-is-decreasing-value-sequence-poset
+      ( P)
+      ( H (skip-zero-sequence u))
+
+  Π-subsequence-leq-decreasing-sequence-poset :
+    is-decreasing-sequence-poset P u →
+    Π-subsequence (λ v → leq-sequence-poset P v u) u
+  Π-subsequence-leq-decreasing-sequence-poset H v n =
+    H n (extract-subsequence u v n) (leq-id-extract-subsequence u v n)
+```
+
+### A decreasing sequence `u` with `u (p + n) ＝ u n` is constant between `n` and `p + n`
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P)
+  (p n : ℕ) (I : u (p +ℕ n) ＝ u n)
+  where
+
+  constant-value-is-stationnary-interval-decreasing-sequence-poset :
+    is-decreasing-sequence-poset P u →
+    (k : ℕ) (J : leq-ℕ k p) → u (k +ℕ n) ＝ u n
+  constant-value-is-stationnary-interval-decreasing-sequence-poset H k J =
+    antisymmetric-leq-Poset
+      ( P)
+      ( u (k +ℕ n))
+      ( u n)
+      ( H n (k +ℕ n) (leq-add-ℕ' n k))
+      ( concatenate-eq-leq-Poset
+        ( P)
+        ( inv I)
+        ( H (k +ℕ n) (p +ℕ n) (preserves-leq-left-add-ℕ n k p J)))
+```
+
+### A decreasing sequence in a partially ordered set with a constant subsequence is asymptotically constant
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u : sequence-poset P}
+  where
+
+  ∞-constant-Σ-subsequence-constant-decreasing-sequence-poset :
+    is-decreasing-sequence-poset P u →
+    Σ-subsequence is-constant-sequence u →
+    is-∞-constant-sequence u
+  ∞-constant-Σ-subsequence-constant-decreasing-sequence-poset H =
+    rec-Σ
+      ( λ v K →
+        ∞-constant-is-∞-value-sequence
+          ( u (extract-subsequence u v zero-ℕ))
+          ( u)
+          ( ( extract-subsequence u v zero-ℕ) ,
+            ( λ n I →
+              antisymmetric-leq-Poset
+                ( P)
+                ( sequence-subsequence u v zero-ℕ)
+                ( u n)
+                ( concatenate-eq-leq-Poset
+                  ( P)
+                  ( K zero-ℕ (modulus-subsequence u v n))
+                  ( H
+                    ( n)
+                    ( extract-modulus-subsequence u v n)
+                    ( leq-extract-modulus-subsequence u v n)))
+                ( H (extract-subsequence u v zero-ℕ) n I))))
+```
+
+### A decreasing sequence in a partially ordered set with an asymptotically constant subsequence is asymptotically constant
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u : sequence-poset P}
+  where
+
+  ∞-constant-Σ-subsequence-∞-constant-decreasing-sequence-poset :
+    is-decreasing-sequence-poset P u →
+    Σ-subsequence is-∞-constant-sequence u →
+    is-∞-constant-sequence u
+  ∞-constant-Σ-subsequence-∞-constant-decreasing-sequence-poset H =
+    ( ∞-constant-Σ-subsequence-constant-decreasing-sequence-poset P H) ∘
+    ( rec-Σ
+      ( λ v →
+        ( rec-Σ (λ w I → (sub-subsequence u v w , I))) ∘
+        ( constant-subsequence-is-∞-constant-sequence
+          ( sequence-subsequence u v))))
+```
diff --git a/src/order-theory/increasing-sequences-posets.lagda.md b/src/order-theory/increasing-sequences-posets.lagda.md
new file mode 100644
index 0000000000..568c4c23ab
--- /dev/null
+++ b/src/order-theory/increasing-sequences-posets.lagda.md
@@ -0,0 +1,198 @@
+# Increasing sequences in partially ordered sets
+
+```agda
+module order-theory.increasing-sequences-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.based-induction-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strictly-increasing-sequences-natural-numbers
+
+open import foundation.asymptotical-dependent-sequences
+open import foundation.asymptotically-constant-sequences
+open import foundation.constant-sequences
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.subsequences
+open import foundation.universe-levels
+
+open import order-theory.order-preserving-maps-posets
+open import order-theory.posets
+open import order-theory.sequences-posets
+```
+
+</details>
+
+## Idea
+
+A [sequence in a partially ordered set](order-theory.sequences-posets.md) is
+**increasing** if it preserves the
+[standard ordering on the natural numbers](elementary-number-theory.inequality-natural-numbers.md).
+
+## Definitions
+
+### Increasing sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P)
+  where
+
+  is-increasing-prop-sequence-poset : Prop l2
+  is-increasing-prop-sequence-poset =
+    preserves-order-Poset-Prop ℕ-Poset P u
+
+  is-increasing-sequence-poset : UU l2
+  is-increasing-sequence-poset =
+    type-Prop is-increasing-prop-sequence-poset
+```
+
+## Properties
+
+### A sequence in a partially ordered set is increasing if and only if all its values are increasing
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u : sequence-poset P}
+  where
+
+  increasing-sequence-is-increasing-value-sequence-poset :
+    ((n : ℕ) → is-increasing-value-sequence-poset P u n) →
+    is-increasing-sequence-poset P u
+  increasing-sequence-is-increasing-value-sequence-poset H p =
+    based-ind-ℕ
+      ( p)
+      ( λ q → leq-Poset P (u p) (u q))
+      ( refl-leq-Poset P (u p))
+      ( λ q I →
+        transitive-leq-Poset P (u p) (u q) (u (succ-ℕ q)) (H q))
+
+  increasing-value-is-increasing-sequence-poset :
+    is-increasing-sequence-poset P u →
+    ((n : ℕ) → is-increasing-value-sequence-poset P u n)
+  increasing-value-is-increasing-sequence-poset H n =
+    H n (succ-ℕ n) (succ-leq-ℕ n)
+```
+
+### Any subsequence of an increasing sequence in a partially ordered set is increasing
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P)
+  where
+
+  increasing-Π-subsequence-increasing-sequence-poset :
+    is-increasing-sequence-poset P u →
+    Π-subsequence (is-increasing-sequence-poset P) u
+  increasing-Π-subsequence-increasing-sequence-poset H v p q I =
+    H
+      ( extract-subsequence u v p)
+      ( extract-subsequence u v q)
+      ( preserves-leq-extract-subsequence u v p q I)
+```
+
+### A sequence in a partially ordered set is increasing if and only if it is lesser than all its subsequences
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P)
+  where
+
+  increasing-Π-subsequence-leq-sequence-poset :
+    Π-subsequence (λ v → leq-sequence-poset P u v) u →
+    is-increasing-sequence-poset P u
+  increasing-Π-subsequence-leq-sequence-poset H =
+    increasing-sequence-is-increasing-value-sequence-poset
+      ( P)
+      ( H (skip-zero-sequence u))
+
+  Π-subsequence-leq-increasing-sequence-Poset :
+    is-increasing-sequence-poset P u →
+    Π-subsequence (λ v → leq-sequence-poset P u v) u
+  Π-subsequence-leq-increasing-sequence-Poset H v n =
+    H n (extract-subsequence u v n) (leq-id-extract-subsequence u v n)
+```
+
+### An increasing sequence `u` with `u (p + n) ＝ u n` is constant between `n` and `p + n`
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P)
+  (p n : ℕ) (I : u (p +ℕ n) ＝ u n)
+  where
+
+  constant-value-is-stationnary-interval-increasing-sequence-poset :
+    is-increasing-sequence-poset P u →
+    (k : ℕ) (J : leq-ℕ k p) → u (k +ℕ n) ＝ u n
+  constant-value-is-stationnary-interval-increasing-sequence-poset H k J =
+    antisymmetric-leq-Poset
+      ( P)
+      ( u (k +ℕ n))
+      ( u n)
+      ( concatenate-leq-eq-Poset
+        ( P)
+        ( H (k +ℕ n) (p +ℕ n) (preserves-leq-left-add-ℕ n k p J))
+        ( I))
+      ( H n (k +ℕ n) (leq-add-ℕ' n k))
+```
+
+### An increasing sequence in a partially ordered set with a constant subsequence is asymptotically constant
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u : sequence-poset P}
+  where
+
+  ∞-constant-Σ-subsequence-constant-increasing-sequence-poset :
+    is-increasing-sequence-poset P u →
+    Σ-subsequence is-constant-sequence u →
+    is-∞-constant-sequence u
+  ∞-constant-Σ-subsequence-constant-increasing-sequence-poset H =
+    rec-Σ
+      ( λ v K →
+        ∞-constant-is-∞-value-sequence
+          ( u (extract-subsequence u v zero-ℕ))
+          ( u)
+          ( ( extract-subsequence u v zero-ℕ) ,
+            ( λ n I →
+              antisymmetric-leq-Poset
+                ( P)
+                ( sequence-subsequence u v zero-ℕ)
+                ( u n)
+                ( H (extract-subsequence u v zero-ℕ) n I)
+                ( concatenate-leq-eq-Poset
+                  ( P)
+                  ( H
+                    ( n)
+                    ( extract-modulus-subsequence u v n)
+                    ( leq-extract-modulus-subsequence u v n))
+                  ( K (modulus-subsequence u v n) zero-ℕ)))))
+```
+
+### An increasing sequence in a partially ordered set with an asymptotically constant subsequence is asymptotically constant
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u : sequence-poset P}
+  where
+
+  ∞-constant-Σ-subsequence-∞-constant-increasing-sequence-poset :
+    is-increasing-sequence-poset P u →
+    Σ-subsequence is-∞-constant-sequence u →
+    is-∞-constant-sequence u
+  ∞-constant-Σ-subsequence-∞-constant-increasing-sequence-poset H =
+    ( ∞-constant-Σ-subsequence-constant-increasing-sequence-poset P H) ∘
+    ( rec-Σ
+      ( λ v →
+        ( rec-Σ ( λ w I → ( sub-subsequence u v w , I))) ∘
+        ( constant-subsequence-is-∞-constant-sequence
+          ( sequence-subsequence u v))))
+```
diff --git a/src/order-theory/monotonic-sequences-posets.lagda.md b/src/order-theory/monotonic-sequences-posets.lagda.md
new file mode 100644
index 0000000000..0c5a0bc170
--- /dev/null
+++ b/src/order-theory/monotonic-sequences-posets.lagda.md
@@ -0,0 +1,72 @@
+# Monotonic sequences in partially ordered sets
+
+```agda
+module order-theory.monotonic-sequences-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.asymptotically-constant-sequences
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.subsequences
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import order-theory.constant-sequences-posets
+open import order-theory.decreasing-sequences-posets
+open import order-theory.increasing-sequences-posets
+open import order-theory.posets
+open import order-theory.sequences-posets
+```
+
+</details>
+
+## Idea
+
+A [sequence in a partially ordered set](order-theory.sequences-posets.md) is
+**monotonic** if it is [increasing](order-theory.increasing-sequences-posets.md)
+or [decreasing](order-theory.decreasing-sequences-posets.md).
+
+## Properties
+
+### An increasing sequence in a partially ordered set with a decreasing subsequence is asymptotically constant
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u : sequence-poset P}
+  (H : is-increasing-sequence-poset P u)
+  where
+
+  ∞-constant-Σ-subsequence-decreasing-is-increasing-sequence-poset :
+    Σ-subsequence (is-decreasing-sequence-poset P) u →
+    is-∞-constant-sequence u
+  ∞-constant-Σ-subsequence-decreasing-is-increasing-sequence-poset =
+    ( ∞-constant-Σ-subsequence-constant-increasing-sequence-poset P H) ∘
+    ( tot
+      ( (constant-is-increasing-decreasing-sequence-poset P) ∘
+        ( increasing-Π-subsequence-increasing-sequence-poset P u H)))
+```
+
+### A decreasing sequence in a partially ordered set with an increasing subsequence is asymptotically constant
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u : sequence-poset P}
+  (H : is-decreasing-sequence-poset P u)
+  where
+
+  ∞-constant-Σ-subsequence-increasing-is-decreasing-sequence-poset :
+    Σ-subsequence (is-increasing-sequence-poset P) u →
+    is-∞-constant-sequence u
+  ∞-constant-Σ-subsequence-increasing-is-decreasing-sequence-poset =
+    ( ∞-constant-Σ-subsequence-constant-decreasing-sequence-poset P H) ∘
+    ( tot
+      ( λ v K →
+        constant-is-increasing-decreasing-sequence-poset
+          ( P)
+          ( K)
+          ( decreasing-Π-subsequence-decreasing-sequence-poset P u H v)))
+```
diff --git a/src/order-theory/posets.lagda.md b/src/order-theory/posets.lagda.md
index e3e5d5e91b..b17485d73c 100644
--- a/src/order-theory/posets.lagda.md
+++ b/src/order-theory/posets.lagda.md
@@ -74,6 +74,9 @@ module _
   refl-leq-Poset : is-reflexive leq-Poset
   refl-leq-Poset = refl-leq-Preorder preorder-Poset
 
+  leq-eq-Poset : {x y : type-Poset} → x ＝ y → leq-Poset x y
+  leq-eq-Poset {x} {.x} refl = refl-leq-Poset x
+
   transitive-leq-Poset : is-transitive leq-Poset
   transitive-leq-Poset = transitive-leq-Preorder preorder-Poset
 
diff --git a/src/order-theory/sequences-posets.lagda.md b/src/order-theory/sequences-posets.lagda.md
new file mode 100644
index 0000000000..168d1e47ea
--- /dev/null
+++ b/src/order-theory/sequences-posets.lagda.md
@@ -0,0 +1,348 @@
+# Sequences in partially ordered sets
+
+```agda
+module order-theory.sequences-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.asymptotical-dependent-sequences
+open import foundation.asymptotically-constant-sequences
+open import foundation.asymptotically-equal-sequences
+open import foundation.binary-relations
+open import foundation.constant-sequences
+open import foundation.dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.universe-levels
+
+open import order-theory.posets
+```
+
+</details>
+
+## Idea
+
+Sequences in a partially ordered set are sequences in the underlying set. They
+can be partially ordered by pointwise comparison.
+
+## Definitions
+
+### Sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2)
+  where
+
+  sequence-poset : UU l1
+  sequence-poset = sequence (type-Poset P)
+```
+
+### Monotonic values of sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P) (n : ℕ)
+  where
+
+  is-increasing-value-prop-sequence-poset : Prop l2
+  is-increasing-value-prop-sequence-poset =
+    leq-Poset-Prop P (u n) (u (succ-ℕ n))
+
+  is-increasing-value-sequence-poset : UU l2
+  is-increasing-value-sequence-poset =
+    type-Prop is-increasing-value-prop-sequence-poset
+
+  is-prop-is-increasing-value-sequence-poset :
+    is-prop is-increasing-value-sequence-poset
+  is-prop-is-increasing-value-sequence-poset =
+    is-prop-type-Prop is-increasing-value-prop-sequence-poset
+
+  is-decreasing-value-prop-sequence-poset : Prop l2
+  is-decreasing-value-prop-sequence-poset =
+    leq-Poset-Prop P (u (succ-ℕ n)) (u n)
+
+  is-decreasing-value-sequence-poset : UU l2
+  is-decreasing-value-sequence-poset =
+    type-Prop is-decreasing-value-prop-sequence-poset
+
+  is-prop-is-decreasing-value-sequence-poset :
+    is-prop is-decreasing-value-sequence-poset
+  is-prop-is-decreasing-value-sequence-poset =
+    is-prop-type-Prop is-decreasing-value-prop-sequence-poset
+```
+
+### Pointwise comparison on sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u v : sequence-poset P)
+  where
+
+  leq-value-prop-sequence-poset : ℕ → Prop l2
+  leq-value-prop-sequence-poset n = leq-Poset-Prop P (u n) (v n)
+
+  leq-value-sequence-poset : ℕ → UU l2
+  leq-value-sequence-poset = type-Prop ∘ leq-value-prop-sequence-poset
+
+  leq-prop-sequence-poset : Prop l2
+  leq-prop-sequence-poset = Π-Prop ℕ leq-value-prop-sequence-poset
+
+  leq-sequence-poset : UU l2
+  leq-sequence-poset = type-Prop leq-prop-sequence-poset
+
+  is-prop-leq-sequence-poset : is-prop leq-sequence-poset
+  is-prop-leq-sequence-poset = is-prop-type-Prop leq-prop-sequence-poset
+```
+
+### The partially ordered set of sequences in a partially ordered set
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2)
+  where
+
+  poset-sequence-poset : Poset l1 l2
+  pr1 (pr1 poset-sequence-poset) = sequence-poset P
+  pr1 (pr2 (pr1 poset-sequence-poset)) = leq-prop-sequence-poset P
+  pr1 (pr2 (pr2 (pr1 poset-sequence-poset))) u n = refl-leq-Poset P (u n)
+  pr2 (pr2 (pr2 (pr1 poset-sequence-poset))) u v w J I n =
+    transitive-leq-Poset P (u n) (v n) (w n) (J n) (I n)
+  pr2 poset-sequence-poset u v I J =
+    eq-htpy (λ n → antisymmetric-leq-Poset P (u n) (v n) (I n) (J n))
+
+  refl-leq-sequence-poset : is-reflexive (leq-sequence-poset P)
+  refl-leq-sequence-poset = refl-leq-Poset poset-sequence-poset
+
+  transitive-leq-sequence-poset : is-transitive (leq-sequence-poset P)
+  transitive-leq-sequence-poset = transitive-leq-Poset poset-sequence-poset
+
+  antisymmetric-leq-sequence-poset : is-antisymmetric (leq-sequence-poset P)
+  antisymmetric-leq-sequence-poset =
+    antisymmetric-leq-Poset poset-sequence-poset
+```
+
+### Asymptotical inequality of sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2)
+  where
+
+  leq-∞-sequence-poset : (u v : sequence-poset P) → UU l2
+  leq-∞-sequence-poset u v = asymptotically (leq-value-sequence-poset P u v)
+
+  refl-leq-∞-sequence-poset : is-reflexive leq-∞-sequence-poset
+  refl-leq-∞-sequence-poset = asymptotically-Π ∘ (refl-leq-sequence-poset P)
+
+  leq-∞-eq-∞-sequence-poset :
+    {u v : sequence-poset P} → eq-∞-sequence u v → leq-∞-sequence-poset u v
+  leq-∞-eq-∞-sequence-poset {u} {v} =
+    map-asymptotically-Π (λ n → leq-eq-Poset P)
+
+  transitive-leq-∞-sequence-poset : is-transitive leq-∞-sequence-poset
+  transitive-leq-∞-sequence-poset u v w =
+    map-binary-asymptotically-Π (λ n → transitive-leq-Poset P (u n) (v n) (w n))
+
+  antisymmetric-∞-leq-∞-sequence-poset :
+    (u v : sequence-poset P) →
+    leq-∞-sequence-poset u v →
+    leq-∞-sequence-poset v u →
+    eq-∞-sequence u v
+  antisymmetric-∞-leq-∞-sequence-poset u v =
+    map-binary-asymptotically-Π (λ n → antisymmetric-leq-Poset P (u n) (v n))
+
+  leq-∞-leq-sequence-poset :
+    {u v : sequence-poset P} →
+    leq-sequence-poset P u v →
+    leq-∞-sequence-poset u v
+  leq-∞-leq-sequence-poset = asymptotically-Π
+```
+
+### Concatenation of asymptotical inequality and equality of sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u v w : sequence-poset P}
+  where
+
+  concatenate-eq-∞-leq-∞-sequence-poset :
+    eq-∞-sequence u v → leq-∞-sequence-poset P v w → leq-∞-sequence-poset P u w
+  concatenate-eq-∞-leq-∞-sequence-poset =
+    map-binary-asymptotically-Π (λ n → concatenate-eq-leq-Poset P)
+
+  concatenate-leq-∞-eq-∞-sequence-poset :
+    leq-∞-sequence-poset P u v → eq-∞-sequence v w → leq-∞-sequence-poset P u w
+  concatenate-leq-∞-eq-∞-sequence-poset =
+    map-binary-asymptotically-Π (λ n → concatenate-leq-eq-Poset P)
+
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) {u v w z : sequence-poset P}
+  where
+
+  concatenate-eq-∞-leq-∞-eq-∞-sequence-poset :
+    eq-∞-sequence u v →
+    leq-∞-sequence-poset P v w →
+    eq-∞-sequence w z →
+    leq-∞-sequence-poset P u z
+  concatenate-eq-∞-leq-∞-eq-∞-sequence-poset =
+    ( map-binary-asymptotically) ∘
+    ( map-asymptotically-Π
+      ( λ n H J →
+        (concatenate-eq-leq-Poset P H) ∘ (concatenate-leq-eq-Poset P J)))
+```
+
+## Properties
+
+### Any value of a sequence in a partially ordered set is stationnary if and only if it is both increasing and decreasing
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-poset P) (n : ℕ)
+  where
+
+  increasing-value-is-stationnary-value-sequence-poset :
+    is-stationnary-value-sequence u n →
+    is-increasing-value-sequence-poset P u n
+  increasing-value-is-stationnary-value-sequence-poset H =
+    leq-eq-Poset P H
+
+  decreasing-value-is-stationnary-value-sequence-poset :
+    is-stationnary-value-sequence u n →
+    is-decreasing-value-sequence-poset P u n
+  decreasing-value-is-stationnary-value-sequence-poset H =
+    leq-eq-Poset P (inv H)
+
+  stationnary-value-is-increasing-decreasing-value-sequence-poset :
+    is-increasing-value-sequence-poset P u n →
+    is-decreasing-value-sequence-poset P u n →
+    is-stationnary-value-sequence u n
+  stationnary-value-is-increasing-decreasing-value-sequence-poset =
+    antisymmetric-leq-Poset P (u n) (u (succ-ℕ n))
+```
+
+### Asymptotical values preserve asymptotical inequality of sequences in partially ordered sets
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u v : sequence-poset P)
+  (I : leq-∞-sequence-poset P u v)
+  where
+
+  leq-∞-left-leq-∞-constant-sequence-poset :
+    (H : is-∞-constant-sequence u) →
+    leq-∞-sequence-poset P (const-∞-value-∞-constant-sequence H) v
+  leq-∞-left-leq-∞-constant-sequence-poset H =
+    concatenate-eq-∞-leq-∞-sequence-poset
+      ( P)
+      ( eq-∞-value-∞-constant-sequence H)
+      ( I)
+
+  leq-∞-right-leq-∞-constant-sequence-poset :
+    (H : is-∞-constant-sequence v) →
+    leq-∞-sequence-poset P u (const-∞-value-∞-constant-sequence H)
+  leq-∞-right-leq-∞-constant-sequence-poset =
+    ( concatenate-leq-∞-eq-∞-sequence-poset P I) ∘
+    ( eq-∞-value-∞-constant-sequence')
+
+  leq-∞-value-leq-∞-constant-sequence-poset :
+    (H : is-∞-constant-sequence u) →
+    (K : is-∞-constant-sequence v) →
+    leq-∞-sequence-poset P
+      (const-∞-value-∞-constant-sequence H)
+      (const-∞-value-∞-constant-sequence K)
+  leq-∞-value-leq-∞-constant-sequence-poset H K =
+    concatenate-eq-∞-leq-∞-eq-∞-sequence-poset
+      ( P)
+      ( eq-∞-value-∞-constant-sequence H)
+      ( I)
+      ( eq-∞-value-∞-constant-sequence' K)
+
+  leq-value-leq-∞-constant-sequence-poset :
+    (H : is-∞-constant-sequence u) →
+    (K : is-∞-constant-sequence v) →
+    leq-Poset P (∞-value-∞-constant-sequence H) (∞-value-∞-constant-sequence K)
+  leq-value-leq-∞-constant-sequence-poset H K =
+    value-∞-asymptotically (leq-∞-value-leq-∞-constant-sequence-poset H K)
+```
+
+### A sequence in a partially ordered set that asymptotically lies between two asymptotically equal sequences is asymptotically equal to them
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u v w : sequence-poset P)
+  (I : leq-∞-sequence-poset P u v) (J : leq-∞-sequence-poset P v w)
+  (E : eq-∞-sequence w u)
+  where
+
+  left-eq-∞-squeeze-sequence-poset : eq-∞-sequence u v
+  left-eq-∞-squeeze-sequence-poset =
+    antisymmetric-∞-leq-∞-sequence-poset
+      ( P)
+      ( u)
+      ( v)
+      ( I)
+      ( concatenate-leq-∞-eq-∞-sequence-poset P J E)
+
+  right-eq-∞-squeeze-sequence-poset : eq-∞-sequence v w
+  right-eq-∞-squeeze-sequence-poset =
+    antisymmetric-∞-leq-∞-sequence-poset
+      ( P)
+      ( v)
+      ( w)
+      ( J)
+      ( concatenate-eq-∞-leq-∞-sequence-poset P E I)
+```
+
+### A sequence in a partially ordered that asymptotically lies between two asymptotically constant sequences with the same asymptotical value is asymptotically constant
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (u v w : sequence-poset P)
+  (I : leq-∞-sequence-poset P u v) (J : leq-∞-sequence-poset P v w)
+  (H : is-∞-constant-sequence u) (K : is-∞-constant-sequence w)
+  where
+
+  ∞-constant-eq-∞-value-squeeze-sequence-poset :
+    Id
+      (∞-value-∞-constant-sequence K)
+      (∞-value-∞-constant-sequence H) →
+    is-∞-constant-sequence v
+  ∞-constant-eq-∞-value-squeeze-sequence-poset E =
+    preserves-∞-constant-eq-∞-sequence u v
+      ( left-eq-∞-squeeze-sequence-poset P u v w I J
+        ( eq-∞-sequence-eq-∞-value-∞-constant-sequence w u K H E))
+      ( H)
+
+  ∞-constant-leq-∞-value-squeeze-sequence-poset :
+    leq-Poset P
+      (∞-value-∞-constant-sequence K)
+      (∞-value-∞-constant-sequence H) →
+    is-∞-constant-sequence v
+  ∞-constant-leq-∞-value-squeeze-sequence-poset E =
+    ∞-constant-eq-∞-value-squeeze-sequence-poset
+      ( antisymmetric-leq-Poset
+        ( P)
+        ( ∞-value-∞-constant-sequence K)
+        ( ∞-value-∞-constant-sequence H)
+        ( E)
+        ( leq-value-leq-∞-constant-sequence-poset
+          ( P)
+          ( u)
+          ( w)
+          ( transitive-leq-∞-sequence-poset P u v w J I)
+          ( H)
+          ( K)))
+```
+
+## External links
+
+- The [squeeze theorem](https://en.wikipedia.org/wiki/Squeeze_theorem) at
+  Wikipedia