Sylvester's sequence

src/elementary-number-theory.lagda.md

@@ -149,6 +149,7 @@ open import elementary-number-theory.strict-inequality-rational-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
+open import elementary-number-theory.sylvesters-sequence public
 open import elementary-number-theory.taxicab-numbers public
 open import elementary-number-theory.telephone-numbers public
 open import elementary-number-theory.triangular-numbers public

src/elementary-number-theory/sylvesters-sequence.lagda.md

@@ -0,0 +1,51 @@
+# Sylvester's sequence
+
+```agda
+module elementary-number-theory.sylvesters-sequence where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.ordinal-induction-natural-numbers
+open import elementary-number-theory.products-of-natural-numbers
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+{{#concept "Sylvester's sequence" WD="Sylvester's sequence" WDID=Q2293800 Agda=sylvesters-sequence-ℕ}}
+is the [sequence](foundation.sequences.md) `s` of
+[natural numbers](elementary-number-theory.natural-numbers.md) in which `s n` is
+the successor of the
+[product](elementary-number-theory.products-of-natural-numbers.md) of all the
+numbers `s i` for `i < n`, i.e.,
+
+$$
+  s_n := 1+\left(\prod_{i<n}s_i\right).
+$$
+
+The first few entries in this sequence are `s 0 = 2`, `s 1 = 3`, `s 2 = 7`, and
+`s 3 = 43`.
+
+Sylvester's sequence is listed as [A000058](https://oeis.org/A000058) in the
+[OEIS](literature.oeis.md) {{#cite oeis}}.
+
+## Definitions
+
+```agda
+sylvesters-sequence-ℕ : ℕ → ℕ
+sylvesters-sequence-ℕ =
+  ordinal-ind-ℕ
+    ( λ _ → ℕ)
+    ( λ n f →
+      succ-ℕ (Π-ℕ n (λ i → f (nat-Fin n i) (strict-upper-bound-nat-Fin n i))))
+```
+
+## References
+
+{{#bibliography}}

src/foundation/sequences.lagda.md

@@ -17,7 +17,14 @@ open import foundation-core.function-types
 
 ## Idea
 
-A **sequence** of elements in a type `A` is a map `ℕ → A`.
+A {{#concept "sequence" Agda=sequence}} of elements of type `A` is a map `ℕ → A`
+from the [natural numbers](elementary-number-theory.natural-numbers.md) into
+`A`.
+
+For a list of sequences from the
+[On-Line Encyclopedia of Integer Sequences](https://oeis.org) {{#cite oeis}}
+that are formalized in agda-unimath, see the page
+[`literature.oeis`](literature.oeis.md).
 
 ## Definition
 
@@ -35,3 +42,7 @@ map-sequence :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → sequence A → sequence B
 map-sequence f a = f ∘ a
 ```
+
+## References
+
+{{#bibliography}}

src/literature/oeis.lagda.md

@@ -84,6 +84,13 @@ open import elementary-number-theory.fibonacci-sequence using
   ( Fibonacci-ℕ)
 ```
 
+### [A000058](https://oeis.org/A000058) Sylvester's sequence
+
+```agda
+open import elementary-number-theory.sylvesters-sequence using
+  ( sylvesters-sequence-ℕ)
+```
+
 ### [A000079](https://oeis.org/A000079) Powers of `2`
 
 ```agda