1 Introduction

1.1 Two presentations of $R$ , two presentations of $π$

The synthesis paper of our series identified six mutually equivalent presentations of the natural numbers (NNO, Peano, primitive recursion, set-theoretic encoding, Yoneda representable, HoTT inductive type). For the real numbers the analogue narrative produces two presentations rather than six, but each is itself a different universal property:

Inductive (Cauchy/HIIT). Booij’s HoTT Cauchy reals $R_{c}$ , presented as the initial algebra of a signature consisting of $Q$ -coercion, a limit operation taking $(ε \mapsto x_{ε})$ -Cauchy approximations to a point of $R_{c}$ , plus path constructors that quotient. This is the universal Cauchy-complete Archimedean ordered field.
Coinductive (final coalgebra). The cofree object on a digit-stream signature: $R ≅ ν G$ for an endofunctor $G$ which is roughly $G X = D \times X$ (with $D$ a digit alphabet) modulo a carry-bisimulation. Streams come with a coinduction principle (Lambek; Rutten ) rather than a recursion principle.

These two presentations are isomorphic as ordered fields by the standard uniqueness theorem for Dedekind-complete Archimedean fields (Paper III Theorem 4.1). They are however not isomorphic as effective structures: the Type II Turing computability literature establishes that Cauchy realizers and stream realizers are interreducible but not equiprimitive. In the intensional setting of HoTT this distinction shows up in the computation rules: the inductive presentation supports recursors that compute on constructors, while the coinductive presentation supports corecursors that produce streams element by element with guarded productivity.

For the transcendentals $π$ and $e$ , the inductive side is well-understood: Paper V Definitions 8.1–8.2 present $π$ as the centre of the contractible type $Σ_{p : R_{c}} (sin p = 0) \times (p > 0) \times (\forall x \in (0, p), sin x > 0)$ and $e$ as $exp (1)$ via the universal property of $exp$ as the unique smooth $f : R_{c} \to R_{c}$ with $f^{'} = f$ and $f (0) = 1$ . The coinductive side has, prior to this paper, been left implicit: the generic statement “ $π$ and $e$ are computable hence have canonical digit streams” is true but does not constitute a HoTT-internal characterisation.

1.2 The principal contribution

The principal contribution of this paper is to write down such an internal characterisation. Concretely, we construct:

A functor $F_{b} : U \to U$ , $F_{b} X = D_{b} \times X$ , with $D_{b} = Fin (b)$ the alphabet on $b$ digits, and prove that its final coalgebra $ν F_{b}$ in cubical HoTT is the M-type of streams $D_{b}^{N}$ .
A bisimulation $\sim_{b}$ on $ν F_{b}$ , the carry-bisimulation, which makes $ν F_{b} / \sim_{b}$ an ordered Archimedean field equipped with a continuous map to $[0, 1]$ .
Two bisimulation-closed observable predicates $P_{π}, P_{e}$ on $ν F_{b}$ , expressed entirely in the internal language of the coalgebra (head/tail/observation), which uniquely identify (up to bisimulation) the Bailey–Borwein–Plouffe digits of $π$ in base $16$ and the Euler-series digits of $e$ in any base.
A coinductive proof, via coinduction up-to-context, that the unique-existence statement is contractible: the type $Σ_{s : ν F_{b}} P_{π} (s)$ is contractible.

This separates the question “what does $π$ name?” into a foundational layer (the final coalgebra structure) and a content layer (the BBP series). The final-coalgebra layer is internal to HoTT and uses no HIIT path constructors. The content layer translates a classical analytic identity into a guarded corecursive equation, whose validity is checked by coinduction.

1.3 Why coinduction matters in HoTT

In Martin-Löf type theory the coinductive types of Coquand and the M-types of Ahrens–Capriotti–Spadotti are treated by dualising the W-type construction. In cubical HoTT M-types satisfy a strong coinduction principle, namely that bisimulation implies path-equality. This is Theorem 5.3 of Paper III in our series, which we recall and refine here as Theorem 13.

Crucially, coinduction allows us to exhibit equalities between streams produced by a priori different corecursive schemes. For instance, the digit stream produced by Machin’s formula $π = 16 arctan (1/5) - 4 arctan (1/239)$ is not, as a sequence of base-10 digits, definitionally equal to the digit stream produced by the Leibniz series $π = 4 n = 0 \sum \infty \frac{( - 1 ) ^{n}}{2 n + 1} .$ Their equality must be proven, and coinduction up-to is the natural tool. Once equality is established, both schemes name the same $π : ν F_{10} / \sim_{10}$ . Our characterisation factors through this identification.

1.4 Outline

2 fixes the type-theoretic framework: cubical HoTT, polynomial endofunctors, M-types, and the construction of final coalgebras. 3 states and proves a HoTT-internal Lambek lemma and the resulting coinduction principle. 4 develops the stream coalgebra in detail, including the carry-bisimulation. 5 introduces bisimulation-closed predicates and the up-to technique. 6 contains the main results: the coalgebraic characterisations of $π$ and $e$ . 7 sketches the cubical M-type realisation. 8 compares to the Cauchy HIIT of Paper V. 9 states the $ζ$ -prerequisite chain and the $ζ (s) = 0$ -internal-to-coalgebra problem. 10 closes with open problems.

2 Mathematical framework

2.1 Cubical HoTT and polynomial endofunctors

We work in cubical type theory à la Cohen–Coquand–Huber–Mörtberg (CCHM) , with universes $U_{0} : U_{1} : \dots$ closed under the usual type formers, and with the univalence axiom provable from the path-cube structure. We write $a =_{A} b$ for the path type, $refl_{a}$ for the constant path, and $Σ$ , $Π$ for the dependent types. Truncation levels follow Voevodsky’s conventions: a type is a proposition if it has at most one inhabitant up to path equality, a set if its identity types are propositions, and so on.

Definition 1 (Polynomial endofunctor). A polynomial endofunctor on $U$ is a functor $F : U \to U$ of the form $F X = Σ_{a : A} X^{B (a)}$ for some $A : U$ and $B : A \to U$ . The pair $(A, B)$ is called a container or signature.

The action of $F$ on a function $f : X \to Y$ is $F f (a, h) = (a, f \circ h)$ .

Example 2. The stream functor on alphabet $A$ is $F_{A} X = A \times X$ . This is polynomial with $A$ -many shapes (one per letter) and a single position per shape: $F_{A} X = Σ_{a : A} X^{1}$ , where $1$ is the unit type.

Example 3. For $b \geq 2$ , the base- $b$ digit functor is $F_{b} X = Fin (b) \times X$ , the special case of 2 with $A = Fin (b)$ .

Definition 4 (Coalgebra). An $F$ -coalgebra is a pair $(C, γ)$ with $γ : C \to F C$ . A morphism of coalgebras $(C, γ) \to (D, δ)$ is a function $f : C \to D$ such that $δ \circ f = F f \circ γ$ . The category of $F$ -coalgebras is denoted $Coalg (F)$ .

Definition 5 (Final coalgebra). $(ν F, out)$ is a final $F$ -coalgebra if for every $F$ -coalgebra $(C, γ)$ there is a unique morphism $unfold_{γ} : (C, γ) \to (ν F, out)$ .

Remark 6 (Final = terminal in $Coalg (F)$ ). “Final” here is the standard terminology of Rutten . In categorical language final coalgebras are terminal objects of $Coalg (F)$ , dual to initial algebras (Lambek).

2.2 M-types as final coalgebras

In MLTT the coinductive analogue of W-types is the M-type construction. The M-type for container $(A, B)$ is $M A B = Σ_{u : Tree^{\infty} (A, B)} Wf (u),$ where $Tree^{\infty} (A, B)$ is the type of (potentially infinite) trees and $Wf$ is the productivity (well-formedness) predicate. In cubical HoTT, Ahrens–Capriotti–Spadotti prove:

Theorem 7 (ACS, M-type final coalgebra). For any container $(A, B)$ , the M-type $M A B$ carries a coalgebra structure $out : M A B \to F_{(A, B)} (M A B)$ which is final.

For our applications the relevant case is the stream functor $F_{A} X = A \times X$ , where the M-type specialises to streams $Stream A ≅ A^{N}$ .

Definition 8 (Stream coalgebra). $Stream A := M A (λ - . 1)$ . The destructor $out : Stream A \to A \times Stream A$ decomposes into the two component maps $hd : Stream A \to A, tl : Stream A \to Stream A .$

Remark 9 (Cubical realisation). In cubical HoTT, $Stream A$ admits a definition by guarded recursion using the modality $⊳$ of Birkedal et al. : $Stream A ≅ A \times ⊳ Stream A$ . The fixed point exists because $⊳$ is a contractive functor and the guarded recursion theorem applies.

3 Lambek’s lemma and coinduction

We recall Lambek’s lemma in its dual coalgebraic form, which is the cornerstone of all coinductive characterisations.

Lemma 10 (Dual Lambek). If $(ν F, out)$ is a final $F$ -coalgebra, then $out : ν F \to F (ν F)$ is a path-equivalence.

Proof. Consider the coalgebra $(F (ν F), F out)$ . Finality yields a unique map $θ : F (ν F) \to ν F$ with $out \circ θ = F (F out) \circ F out = F (out \circ θ)$ . Then $θ \circ out : ν F \to ν F$ is a coalgebra morphism, and so is $id_{ν F}$ , so by uniqueness $θ \circ out = id$ . Symmetrically, $out \circ θ$ is a coalgebra morphism on $(F (ν F), F out)$ to itself, equal to the identity. Hence $out$ is a path-equivalence with inverse $θ$ . ◻

Remark 11. 10 is conceptually crucial: it says the final coalgebra is a fixed point of $F$ up to path equivalence, the coinductive dual of Lambek’s algebraic “ $μ F ≅ F (μ F)$ ”. In cubical HoTT this equivalence is strict (definitional after path-application) at base types, which is what makes $hd, tl$ definable.

Definition 12 (Bisimulation). A relation $R : C \times C \to U$ on the carrier of an $F$ -coalgebra $(C, γ)$ is an $F$ -bisimulation if there exists a coalgebra structure $\overset{γ}{ˉ} : Σ_{(x, y) : C \times C} R (x, y) \to F (Σ \dots R)$ making the two projections coalgebra morphisms. Concretely, for the stream functor $F_{A} X = A \times X$ , the unfolded definition is: a relation $R$ on $Stream A$ is a bisimulation iff for all $(x, y)$ with $R (x, y)$ , we have $hd (x) = hd (y)$ and $R (tl (x), tl (y))$ .

Theorem 13 (Coinduction principle). Let $(ν F, out)$ be a final $F$ -coalgebra. For any $F$ -bisimulation $R$ and any $x, y : ν F$ , if $R (x, y)$ holds, then $x = y$ in $ν F$ .

Proof. By 12 the projections $π_{1}, π_{2} : Σ_{(x, y)} R (x, y) \to ν F$ are coalgebra morphisms into the final coalgebra. By uniqueness of mediating maps, $π_{1} = π_{2}$ as coalgebra morphisms, hence as functions, hence pointwise. So if $(x, y, p) : Σ_{(x, y)} R (x, y)$ then $π_{1} (x, y, p) = π_{2} (x, y, p)$ , i.e. $x = y$ . ◻

This is the fundamental coinductive proof principle: to exhibit a path between two elements of a final coalgebra it suffices to exhibit a bisimulation containing them.

4 Stream coalgebras and digit streams

4.1 The stream functor and its final coalgebra

Theorem 14 (Streams as final coalgebra). For any type $A$ , the M-type $Stream A$ together with $out = ⟨ hd, tl ⟩$ is the final coalgebra of $F_{A} = A \times (-)$ .

Proof sketch. For coalgebra $(C, γ : C \to A \times C)$ , define $unfold_{γ} : C \to Stream A$ by guarded corecursion: $hd (unfold_{γ} (c)) tl (unfold_{γ} (c)) := π_{1} (γ (c)), := unfold_{γ} (π_{2} (γ (c))) .$ The morphism property $out \circ unfold_{γ} = F_{A} unfold_{γ} \circ γ$ is judgmental. Uniqueness follows from coinduction (13) applied to the relation $R (s, t) := Σ_{c : C} (s = unfold_{γ} (c)) \times (t = unfold_{γ} (c))$ . ◻

Example 15 (Constant stream). For $a : A$ , $const_{a} := unfold_{γ}$ where $C = 1$ and $γ (⋆) = (a, ⋆)$ , so $hd (const_{a}) = a$ and $tl (const_{a}) = const_{a}$ .

Example 16 (Naturals as stream). $nats := unfold_{γ}$ where $C = N$ and $γ (n) = (n, n + 1)$ . Yields $nats = 0, 1, 2, 3, \dots$

4.2 Base- $b$ digit streams and approximation maps

Fix $b \geq 2$ . We work with digit streams of $Fin (b)$ .

Definition 17 (Approximation map). The base- $b$ approximation map $α_{b} : Stream Fin (b) \to R_{c}$ takes a stream $d_{0} d_{1} d_{2} \dots$ to the Cauchy real $α_{b} (d) := n \to \infty lim k = 0 \sum n - 1 \frac{d _{k}}{b ^{k + 1}},$ which exists because the partial sums form a $b^{- n}$ -Cauchy approximation in Booij’s sense: for $m \geq n$ the difference $\sum_{k = 0}^{m - 1} d_{k} / b^{k + 1} - \sum_{k = 0}^{n - 1} d_{k} / b^{k + 1} = \sum_{k = n}^{m - 1} d_{k} / b^{k + 1} \leq \sum_{k = n}^{\infty} (b - 1) / b^{k + 1} = b^{- n}$ , so the partial sums are uniformly Cauchy with modulus $b^{- n}$ and Booij’s $lim$ -constructor applies.

Lemma 18 (Approximation surjects onto $[0, 1]$ ). $α_{b} : Stream Fin (b) \to R_{c}$ has image $[0, 1] \subset R_{c}$ .

Proof. Surjection onto $[0, 1]$ is the standard digit-expansion: given $x \in [0, 1] \cap R_{c}$ , define $d_{k} = ⌊ b^{k + 1} x ⌋ mod b$ using the floor function on Cauchy reals. The sum converges to $x$ by the standard estimate. Existence of floor on $R_{c}$ uses Booij’s order. (Note that floor is not constant on bisimulation classes; this is the source of the carry equivalence.) ◻

Definition 19 (Carry-bisimulation). The relation $\sim_{b}$ on $Stream Fin (b)$ is the smallest equivalence such that $α_{b} (s) = α_{b} (t)$ implies $s \sim_{b} t$ . Concretely, for any $n$ and any $d \in Fin (b - 1)$ , $d_{0} \dots d_{n - 1} d (b - 1) (b - 1) \dots \sim_{b} d_{0} \dots d_{n - 1} (d + 1) 00 \dots$ This is exactly the “ $0.999 \dots = 1.000 \dots$ ” identification.

Theorem 20 ( $[0, 1]$ as quotient final coalgebra). The set-quotient $Stream Fin (b) / \sim_{b}$ is in HoTT-equivalence with $[0, 1] \subset R_{c}$ via $α_{b}$ .

Proof. $α_{b}$ factors through the quotient by definition of $\sim_{b}$ . The induced map is injective by the kernel of $α_{b}$ being $\sim_{b}$ , and surjective by 18. Both maps are set-functions (between h-sets), hence the resulting bijection is an equivalence by univalence-for-sets. ◻

Remark 21 ( $R$ from $[0, 1]$ ). The whole real line $R$ is recovered as $Z \times [0, 1] / \sim$ with the obvious carrying identifications, or equivalently as the final coalgebra of the functor $G X = Z \times Stream Fin (b) X$ modulo the appropriate bisimulation.

5 Bisimulation-closed predicates and coinduction up-to

To characterise $π$ and $e$ internally to the final coalgebra, we need predicates that respect $\sim_{b}$ . We formalise this notion and develop the up-to technique.

Definition 22 (Bisimulation-closed predicate). A predicate $P : Stream Fin (b) \to Prop$ is $\sim_{b}$ -closed (or simply closed) if $s \sim_{b} t \to P (s) \leftrightarrow P (t)$ . Equivalently, $P$ factors through the quotient $Stream Fin (b) / \sim_{b}$ .

Example 23. The predicate $P (s) := (α_{b} (s) < 1/2)$ is closed; the predicate $P (s) := (hd (s) = 4)$ in base $10$ is not closed: the stream $0.4 999 \dots$ has $hd = 4$ but is bisimilar to $0.5 00 \dots$ which has $hd = 5$ .

Definition 24 (Observable predicate). A predicate $P$ is observable if it is determined by the function $α_{b}$ , i.e. $P (s) = Q (α_{b} (s))$ for some $Q : R_{c} \to Prop$ . Every observable predicate is closed, but not conversely.

Lemma 25. A predicate is closed iff it factors through $α_{b}$ .

Proof. $(\Rightarrow)$ A closed predicate factors through $Stream / \sim_{b}$ , and $α_{b}$ induces an equivalence between $Stream / \sim_{b}$ and $im (α_{b}) \subseteq R_{c}$ (20). Composition with the inverse equivalence gives the factorisation. $(\Leftarrow)$ Immediate: factoring through $α_{b}$ implies $α_{b} (s) = α_{b} (t) \Rightarrow P (s) \leftrightarrow P (t)$ , which is the definition of closure under the kernel of $α_{b}$ . ◻

5.1 Coinduction up-to-context

The plain coinduction principle (13) requires exhibiting a strict bisimulation. In practice this is often inconvenient: one wants to prove $s = t$ by exhibiting a relation $R$ such that $R (s, t)$ implies that the heads agree and the tails are related by $R$ after some closure operations. Sangiorgi–Rutten formalised this via the up-to technique.

Definition 26 ( $Φ$ -up-to). Let $Φ$ be a monotone operator on relations on $Stream A$ . A relation $R$ is a bisimulation up-to $Φ$ if for every $(s, t) \in R$ , $hd (s) = hd (t)$ and $(tl (s), tl (t)) \in Φ (R)$ .

Theorem 27 (Up-to-context soundness). If $Φ$ is compatible (i.e. $Φ$ preserves bisimulations in the sense of Pous–Sangiorgi ), then any bisimulation up-to $Φ$ is contained in $\sim$ .

Proof sketch. Define $R^{*} := ⋃_{n \geq 0} Φ^{n} (R)$ . Show by induction that $R^{*}$ is a (plain) bisimulation: heads agree because $Φ$ preserves head-equality, and tails of $R^{*}$ -related pairs remain in $R^{*}$ because $Φ^{n} (R) \subseteq Φ^{n + 1} (R)$ by monotonicity and the bisimulation-up-to- $Φ$ condition. ◻

Example 28 (Equivalence-closure up-to). $Φ (R) := {(s, t) : \exists s^{'}, t^{'} R (s^{'}, t^{'}) \land s = s^{'} \land t = t^{'}}$ is compatible. So one may freely substitute path-equal streams inside coinductive proofs.

Example 29 (Arithmetic up-to). For arithmetic operations on base- $b$ digit streams (addition, multiplication, division, exponentiation by digit), the operators $Φ_{+} (R) := {(s + u, t + u) : R (s, t)}, Φ_{\cdot} (R) := {(s \cdot u, t \cdot u) : R (s, t)}$ are compatible (their compatibility reduces to verifying that each operation is itself definable as coalgebra morphisms, which is ).

6 Coalgebraic characterisations of $π$ and $e$

We now state the main results of the paper.

6.1 The case of $e$

Definition 30 (Series coalgebra for $e$ ). Define a coalgebra $(C_{e}, γ_{e})$ on $C_{e} := N \times N \times N \times N \times N$ (state: $(n, k, num, den, outdig)$ representing partial summation of $\sum_{k} 1/ k!$ in base $b$ ), with transition $γ_{e}$ implementing the streaming factorial-series algorithm of Sale (refined to spigot form by Rabinowitz–Wagon and Gibbons ) for streaming the digits of $e$ in base $b$ . Concretely, $γ_{e} (s) = (d (s), s^{'})$ where $d (s) \in Fin (b)$ is the next emitted digit and $s^{'}$ is the updated state.

Theorem 31 ( $e$ as final-coalgebra unfold). $unfold_{γ_{e}} (s_{0}) = s_{e} \in Stream Fin (b)$ where $s_{0}$ is the initial state and $α_{b} (s_{e}) = e - 2 \in [0, 1]$ . Equivalently, the digit stream of $e$ (after subtracting the integer part) is the unique solution of the corecursive equation $s_{e} = streamingFraction (⟨ 1/ k! ⟩_{k \geq 0}) .$

Proof. Existence is by guarded corecursion using the productivity of the streaming-factorial algorithm: the state-evolution is structurally decreasing on a measure (the rational interval bounding the unprocessed tail shrinks geometrically), so each output digit is produced after finitely many state transitions. The image under $α_{b}$ equals $e - 2$ by the algorithm’s correctness theorem (a classical fact; see Sale and the spigot-algorithm analysis in ). ◻

Definition 32 (Predicate $P_{e}$ ). $P_{e} : Stream Fin (b) \to Prop$ is the predicate $P_{e} (s) := α_{b} (s) = e - 2$ . It is observable (24) hence closed (25).

Theorem 33 (Coalgebraic characterisation of $e$ ). The type $Σ_{s : Stream Fin (b)} P_{e} (s)$ quotiented by $\sim_{b}$ is contractible. Equivalently: $e - 2$ is the unique element of $ν F_{b} / \sim_{b}$ satisfying $P_{e}$ .

Proof. Existence: 31 gives an inhabitant. Uniqueness: if $s_{1}, s_{2}$ both satisfy $P_{e}$ then $α_{b} (s_{1}) = e - 2 = α_{b} (s_{2})$ , so $s_{1} \sim_{b} s_{2}$ by definition of $\sim_{b}$ . Hence after quotient they coincide. Since the fibres of the quotient map are propositions (a consequence of working with h-sets), the total space is a proposition. Combined with inhabitation, this proves contractibility. ◻

Remark 34. 33 is internal in the sense that $P_{e}$ is expressed in terms of $α_{b}$ , which is itself definable by guarded corecursion. The HIIT path constructors of Booij’s $R_{c}$ enter only inside $α_{b}$ . If one is willing to take $α_{b}$ as the basic “observation”, the characterisation is purely coalgebraic. We discuss this point further in 8.

6.2 The case of $π$

For $π$ the situation is more subtle because no finite-state streaming algorithm is known. We use Bailey–Borwein–Plouffe (BBP) in base 16, which is streamable digit-by-digit although the state grows linearly.

Definition 35 (BBP coalgebra). The Bailey–Borwein–Plouffe identity (1995): $π = k = 0 \sum \infty \frac{1}{1 6 ^{k}} (\frac{4}{8 k + 1} - \frac{2}{8 k + 4} - \frac{1}{8 k + 5} - \frac{1}{8 k + 6}) .$ This induces a coalgebra $(C_{π}, γ_{π})$ with $C_{π}$ encoding partial summation state, and $γ_{π}$ implementing the BBP digit extraction algorithm in base 16.

Theorem 36 ( $π$ as final-coalgebra unfold). $unfold_{γ_{π}} (s_{0}) = s_{π} \in Stream Fin (16)$ satisfies $α_{16} (s_{π}) = π - 3$ .

Proof. By the BBP correctness theorem (which is constructively valid; see ), the partial sums $\sum_{k = 0}^{n - 1}$ approximate $π$ to within $O (1 6^{- n})$ . The hexadecimal digit-extraction state evolves productively, so guarded corecursion yields a stream whose image under $α_{16}$ equals $π - 3$ . ◻

Definition 37 (Predicate $P_{π}$ ). $P_{π} : Stream Fin (16) \to Prop$ is $P_{π} (s) := α_{16} (s) = π - 3$ . Closed by 25.

Theorem 38 (Coalgebraic characterisation of $π$ ). The type $Σ_{s : Stream Fin (16)} P_{π} (s)$ quotiented by $\sim_{16}$ is contractible.

Proof. Same structure as 33, using 36. ◻

6.3 Internalisation: removing the reference to $R_{c}$

33 and 38 reference $e - 2$ and $π - 3$ as elements of $R_{c}$ , hence implicitly the HIIT. We now upgrade these to characterisations expressed purely in terms of bisimulations between streams.

Theorem 39 (Internal characterisation of $e$ ). There is a stream $s^{*} \in Stream Fin (b)$ defined by guarded corecursion (no use of $R_{c}$ or HIIT) such that:

$s_{e} \sim_{b} s^{*}$ , where $s_{e}$ is from 31.
For any stream $t$ , if $t$ satisfies the corecursive equation $out (t) = γ_{e} (state (t))$ for the (no- $R_{c}$ ) state projection $state : Stream \to N^{5}$ (a partial function defined on the image of $unfold_{γ_{e}}$ , see 13), then $s^{*} \sim_{b} t$ .

The unique-existence is proved by coinduction up-to-context.

Proof. Take $s^{*} := unfold_{γ_{e}} (s_{0})$ where $γ_{e}$ from 30 is purely combinatorial (state in $N^{5}$ , no real numbers; the explicit transition rules are spelled out in 13). Existence: 31.

Uniqueness is the substantive part. Suppose $t \in Stream Fin (b)$ satisfies the equation $out (t) = γ_{e} (state (t))$ for some state-projection function $state : Stream \to N^{5}$ that agrees with $s_{0}$ at $t$ . Define the relation $R (u_{1}, u_{2}) := Σ_{c : N^{5}} (u_{1} = unfold_{γ_{e}} (c)) \times (u_{2} = unfold_{γ_{e}} (c)) .$ This is reflexive on the image of $unfold_{γ_{e}}$ . We claim $R$ is a bisimulation up-to the closure $Φ$ defined by $Φ (R) (v_{1}, v_{2}) := Σ_{c} R (unfold_{γ_{e}} (c), unfold_{γ_{e}} (c))$ (equivalently, $Φ$ is the equivalence-closure under $unfold_{γ_{e}}$ -substitution; this is compatible by the example following 27). To verify the bisimulation-up-to property: given $R (u_{1}, u_{2})$ with witness $c$ , both heads equal $π_{1} (γ_{e} (c))$ and both tails equal $unfold_{γ_{e}} (π_{2} (γ_{e} (c)))$ , so heads agree and tails are again related (with the new witness $π_{2} (γ_{e} (c))$ ). By 27 $R \subseteq \sim$ , and by 13 $R (s^{*}, t)$ implies $s^{*} = t$ .

Now apply this with $u_{1} := s^{*} = unfold_{γ_{e}} (s_{0})$ and $u_{2} := t$ : we need to exhibit a $c$ with $t = unfold_{γ_{e}} (c)$ . Such a $c$ is provided by $state (t) = s_{0}$ together with the corecursive equation, by another application of coinduction (using $R^{'} (v_{1}, v_{2}) := \exists c . v_{2} = unfold_{γ_{e}} (c) \land state (v_{1}) = c \land v_{1} satisfies the equation$ ). Hence $s^{*} = t$ .

Therefore $s^{*}$ is the unique stream satisfying the corecursive equation, and the bisimulation class $[s^{*}] \in Stream / \sim_{b}$ is uniquely identified by an internal predicate. ◻

Theorem 40 (Internal characterisation of $π$ ). There is a stream $s_{π}^{*} \in Stream Fin (16)$ defined by guarded corecursion (no use of $R_{c}$ ) such that $s_{π}^{*} \sim_{16} s_{π}$ uniquely up to bisimulation, characterised by the recursion: $out (s_{π}^{*}) = γ_{π}^{combinatorial} (state_{0}) .$

Proof. The argument is structurally identical to that of 39. Concretely, replace $γ_{e}$ by the combinatorial BBP transition function $γ_{π}^{combinatorial}$ : its state space is $N^{k}$ (with $k = 4$ corresponding to the four sub-series in BBP, plus a position counter; see ) holding the integer numerators and denominators of the modular partial sums. The relation $R (u_{1}, u_{2}) := Σ_{c : N^{k}} (u_{1} = unfold_{γ_{π}^{combinatorial}} (c)) \times (u_{2} = unfold_{γ_{π}^{combinatorial}} (c))$ is a bisimulation up-to the substitution-closure $Φ$ , by the same head/tail computation as in 39, and the BBP modular-arithmetic update of $c$ ensures the up-to-context operator is compatible (as in the arithmetic example following 27). By [thm:upto-sound,thm:coinduction] $s_{π}^{*}$ is the unique stream up to $\sim_{16}$ satisfying the BBP corecursive equation. ◻

Remark 41 (What 39 and 40 do and do not say). The key advance of 39 and 40 over 33 and 38 is that the characterising predicate is now of the form “satisfies the corecursive equation $out (s) = γ (state (s))$ ”, expressed purely in terms of $out$ , $hd$ , $tl$ , and combinatorial operations on $N$ . No reference to $R_{c}$ or its path constructors is needed. This realises programmes (a)–(c) of with $F = F_{b}$ and $P = P_{π}$ resp. $P_{e}$ .

We are however candid about a limitation: the predicate “ $s$ satisfies the corecursive equation $out (s) = γ (state (s))$ ” is, in a sense, exactly the description of being the unfold of $γ$ , and the state projection $state$ is canonically defined only on the image of $unfold_{γ}$ (see 13). Read externally, the theorem says: “the unique stream satisfying the corecursive equation for algorithm $X$ is the stream generated by algorithm $X$ .” This is not yet a characterisation of $π$ or $e$ as classical reals without reference to any external structure. Such a fully external characterisation would require either (a) an internal proof that two distinct combinatorial algorithms (e.g. Leibniz and BBP) are bisimilar, or (b) an internal axiomatisation of which streams are “transcendental”.

What [thm:e-internal,thm:pi-internal] do establish is that the bisimulation classes $[s_{e}]_{\sim_{b}} \in Stream / \sim_{b} and [s_{π}]_{\sim_{16}} \in Stream / \sim_{16}$ are the unique fixed points of combinatorial corecursive equations, with no path-constructor data (HIIT-data) needed to express the predicate. This is a strict logical advance over the inductive characterisation of Paper V Definition 8.1, which uses sin-zero data internal to $R_{c}$ . The remaining “gap” is exactly 52 below.

6.4 Comparison: Leibniz, Machin, BBP all name the same $π$

To illustrate the strength of bisimulation as an equality principle in HoTT, we show how three distinct corecursive definitions of $π$ -as-stream are proved equal by coinduction.

Definition 42 (Three coalgebras for $π$ ). Let $γ_{L}$ (Leibniz), $γ_{M}$ (Machin), $γ_{B}$ (BBP) be three coalgebras whose unfolds in base 10 (resp. 10, 16) yield streams $s_{L}, s_{M}, s_{B}$ . Each algorithm is a corecursive streaming version of the corresponding analytic identity for $π$ .

Proposition 43. $s_{L} \sim_{10} s_{M}$ , and $s_{L} \sim_{10} base - conversion (s_{B})$ .

Proof. $α_{10} (s_{L}) = α_{10} (s_{M}) = π - 3 = α_{10} (conv (s_{B}))$ by classical analytic identities (Leibniz, Machin, BBP all sum to $π$ ). Bisimulation follows from 25 and the definition of $\sim_{b}$ as the kernel of $α_{b}$ . ◻

Remark 44 (Limitation: external vs. internal equivalence). 43 factors through the approximation map $α_{10}$ , hence through $R_{c}$ . This is therefore not yet a fully internal proof of bisimilarity: the equality of streams is established by mapping to the inductive $R_{c}$ , computing the values, and pulling back along the kernel of $α_{10}$ .

A truly internal proof would establish a direct stream-level bisimulation between the Leibniz, Machin, and BBP state machines (after base conversion). Schematically, one might construct a product coalgebra on $C_{L} \times C_{M} \times C_{B}^{'}$ (running all three algorithms in parallel, with $C_{B}^{'}$ the base-converted BBP state), together with an invariant $I \subseteq C_{L} \times C_{M} \times C_{B}^{'}$ asserting that the three running partial sums agree to within a shrinking $1 0^{- n}$ window. The bisimulation $R (u_{L}, u_{M}, u_{B}) := \exists (c_{L}, c_{M}, c_{B}) \in I . ⋀ u_{X} = unfold_{γ_{X}} (c_{X})$ would then be coinductively a bisimulation, and 13 would conclude. The technical obstacle is constructing the invariant $I$ in HoTT without circular reference to the value of $π$ . This is precisely the form 52 would take and we do not claim a solution.

The conceptual picture is striking even in the weaker “factor-through- $R_{c}$ ” form: in HoTT, algorithm equivalence on streams becomes path-equality on the final coalgebra, and coinduction is the proof method.

7 Cubical M-types and stream realisation

We sketch the cubical-HoTT realisation of the M-type used above, following ACS .

7.1 The M-type construction

Definition 45 (M-type). For container $(A, B)$ , define $M A B := n lim W_{n}$ where $W_{0} = 1$ , $W_{n + 1} = Σ_{a : A} (B (a) \to W_{n})$ , and the limit is taken along the projections induced by the unique map $W_{1} \to W_{0} = 1$ .

Theorem 46 (Cubical M-type, ACS). In cubical HoTT (CCHM), the limit 45 exists and $M A B$ is the carrier of the final $F_{(A, B)}$ -coalgebra. The destructor $out : M A B \to F_{(A, B)} (M A B)$ is the projection onto the first level.

Remark 47 (Why cubical, not just MLTT). In plain MLTT one cannot prove that $out$ is an equivalence (10) without function extensionality and $η$ -rules. Cubical HoTT provides function extensionality judgmentally (via path-application) and treats M-types coherently with the path structure, which is what we need for the coinduction principle to compute.

7.2 Productivity and guarded recursion

In cubical HoTT, the topos of trees provides a guarded modality $⊳$ (read “later”). Streams are then a fixed point $Stream A ≅ A \times ⊳ Stream A$ , and corecursion is just guarded recursion: the recursive call is hidden under $⊳$ , ensuring productivity at the type level. This is what makes our $unfold_{γ}$ judgmentally well-defined.

8 Comparison with the Cauchy HIIT

8.1 Side-by-side

Inductive (Booij/HoTT Cauchy)	Coinductive (final coalgebra)
HIIT $R_{c}$ with rat, lim, path-constr	M-type $Stream Fin (b)$ + $\sim_{b}$
Recursor: $f (rat q), f (lim x), f (path \dots)$	Corecursor: $hd (unfold (c)), tl (unfold (c))$
$π :=$ centre of contractible sin-zero type (Paper V Def. 8.1)	$π :=$ centre of contractible BBP unfold type (40)
Equality by computation rule + truncation	Equality by bisimulation
Computational content: Cauchy realiser	Computational content: digit stream
$R_{c}$ has join-semilattice + lim-axioms	$Stream / \sim_{b}$ has digit-shift action

8.2 Equivalence theorem

Theorem 48 (Inductive–Coinductive equivalence). There is a HoTT equivalence $β_{b} : Stream Fin (b) / \sim_{b} ≃ [0, 1] \subset R_{c}$ sending the bisimulation class of $s$ to $α_{b} (s)$ .

Proof. Forward direction by 20. Inverse: given $x \in [0, 1] \cap R_{c}$ , produce its base- $b$ digit stream by the floor algorithm of 18; the resulting class $[s] \in Stream / \sim_{b}$ is well-defined because two different digit-expansion choices for the same $x$ differ only at carry boundaries (the $0.999 \dots = 1$ identifications), which is exactly $\sim_{b}$ . ◻

Corollary 49. Under $β_{b}$ , the inductive $π$ (Paper V Definition 8.1) and the coinductive $π$ (40) coincide.

8.3 Why the duality matters

48 says the two presentations describe the same mathematical object. But computationally they differ:

The inductive presentation supports recursion: to define $f : R_{c} \to X$ specify $f (rat q)$ , $f (lim x)$ , and verify path coherence.
The coinductive presentation supports corecursion: to define $g : X \to Stream$ specify $hd (g (c))$ and $tl (g (c))$ in terms of head/tail of an evolving state.

For the transcendentals, the natural definitions are corecursive: $e$ and $π$ are typically given by streaming-digit algorithms (Sale, BBP, spigot algorithms in general). The coinductive presentation matches these algorithms judgmentally; the inductive presentation requires a layer of approximation-and-quotient.

9 Connection to the $ζ$ -prerequisite chain

9.1 The principal open problem

The synthesis paper identifies “ $ζ (s) = 0$ as a HoTT-native statement” as the principal open problem. Loeffler–Stoll formalised $ζ$ in classical Lean/Mathlib (3300 lines for the analytic continuation alone), but no HoTT-native formalisation of the Riemann zeta function is known.

The coalgebraic toolkit developed here suggests an attack route:

Conjecture 50 (Coalgebraic $ζ$ ). There is a polynomial endofunctor $H : U \to U$ with $ν H$ modelling the Riemann zeta function as a stream of digits in some base parametrised by the complex argument $s \in C_{c}$ , such that:

For $s$ with $ℜ (s) > 1$ , $unfold_{γ_{ζ} (s)}$ produces the stream of digits of $ζ (s)$ via the Dirichlet series.
For $s$ in the analytic continuation domain $C_{c} ∖ {1}$ , $unfold_{γ_{ζ}^{'} (s)}$ produces digits via Hurwitz formula.
There is a bisimulation-closed predicate $P_{ζ = 0} : ν H \to Prop$ such that $ζ (s) = 0$ in $C_{c}$ iff the unique unfold satisfies $P_{ζ = 0}$ .

This conjecture is open. We make some progress in 51 below.

9.2 Dirichlet series as stream

Proposition 51 (Dirichlet partial-sum stream). For $s \in C_{c}$ with $ℜ (s) > 1$ , define a coalgebra $(C_{s}, γ_{s})$ on $C_{s} := N \times C_{c}$ with $γ_{s} (n, z) = (digit (z^{'}), (n + 1, z^{'}))$ where $z^{'} = z + n^{- s}$ (the next partial-sum). Then $α_{b} (unfold_{γ_{s}} (0, 0)) = ζ (s)$ , modulo the carry-bisimulation.

Proof sketch. The partial sums $\sum_{n = 1}^{N} n^{- s}$ form a Cauchy approximation to $ζ (s)$ for $ℜ (s) > 1$ (standard fact, constructive proof in Booij’s framework). Streaming digits is then 17 applied to that Cauchy approximation. ◻

51 only handles the convergence half-plane. The hard part is analytic continuation (steps 2 and 3 of 50). The classical Mellin-transform approach (Loeffler–Stoll) does not obviously translate to the coalgebraic setting because contour integration along non-trivial paths in $C_{c}$ is itself a non-trivial constructive issue. We mark this as the principal open problem of the present series.

9.3 Toward analytic continuation coalgebraically

A possible attack: use the functional equation of $ζ$ , $ζ (s) = 2^{s} π^{s - 1} sin (\frac{π s}{2}) Γ (1 - s) ζ (1 - s),$ to define $ζ$ on $ℜ (s) < 0$ by reflection. This is a recursive definition (refer $ζ (s)$ to $ζ (1 - s)$ ), which corresponds in our framework to a morphism between two coalgebras for the same functor $H$ , with the morphism implementing the $s \leftrightarrow 1 - s$ symmetry. A construction of such a morphism in HoTT requires:

A coalgebraic $sin$ and $Γ$ in $C_{c}$ (the former is approachable via the universal property of $exp$ from Paper III §4.3; the latter is significantly harder).
A coalgebraic $z^{s}$ (complex exponentiation), again via $exp$ and $lo g$ .

This is a substantial programme; we leave it as a long-term goal of the YonedaAI HoTT mathematics initiative.

10 Open problems and future work

10.1 The internalisation gap

39 and 40 characterise $π, e$ via combinatorial corecursive equations. But the correctness theorems (that the unfold equals $π - 3$ resp. $e - 2$ ) still reference $R_{c}$ via $α_{b}$ .

Open Problem 52 (Fully internal correctness). Find a HoTT statement $Φ (s)$ in the language of streams alone (no $R_{c}$ , no $α_{b}$ ) such that $Φ (s_{π}) \leftrightarrow ChurchRosserlikeProperty (s_{π})$ , where the property captures $α_{16} (s_{π}) = π - 3$ via a purely stream-theoretic invariant.

A candidate: stream-bisimulation between $s_{π}$ and the unfold of an alternative coalgebra (Machin, Leibniz after base conversion). This makes the correctness theorem a bisimulation-only statement, but at the cost of relating distinct combinatorial algorithms via coinduction.

10.2 The carry-bisimulation as HIT vs. propositional truncation

The quotient $Stream / \sim_{b}$ in 20 can be presented as either (i) a set-quotient HIT, or (ii) a Voevodsky propositional truncation of the equivalence relation. The two are HoTT-equal by univalence-for-sets but differ in computation.

Open Problem 53. Compare the cubical realisation of $Stream / \sim_{b}$ as set-HIT vs. propositional truncation. Which presentation makes $β_{b} : Stream / \sim_{b} ≃ [0, 1]$ computational (i.e. $β_{b} \circ β_{b}^{- 1} \equiv id$ judgmentally)?

10.3 Productivity and the totality of $unfold$

In MLTT-without-cubical, the totality of $unfold$ requires a guardedness check on the coalgebra. In our case the BBP and Sale algorithms are guarded by construction (each step emits exactly one digit and modifies state), but a fully formal proof of guardedness is currently absent in our Lean artefact.

Open Problem 54. Formalise productivity of the BBP and Sale digit-extraction algorithms in Lean 4/Mathlib using the Stream’ API and the Coinductive machinery.

10.4 Higher transcendentals

The methods of this paper apply (with the obvious modifications) to other transcendentals with known spigot/streaming algorithms:

Catalan’s constant $G = \sum_{n = 0}^{\infty} (- 1)^{n} / (2 n + 1)^{2}$
Apéry’s constant $ζ (3)$ (Apéry’s series gives a streaming algorithm)
Euler–Mascheroni $γ$ (no known streaming algorithm of state $poly (n)$ , an open problem in itself)

Open Problem 55. Extend the coalgebraic characterisation to $ζ (3)$ , Catalan’s constant, and (failing that) prove that $γ$ has no finite-state stream coalgebra unfold-equal to it.

10.5 Coalgebraic transcendence proofs

The Lindemann–Weierstrass theorem proves the algebraic independence of $e^{α_{1}}, \dots, e^{α_{n}}$ for $Q$ -linearly independent algebraic $α_{i}$ . Paper V §8.3–8.4 marks this as “partially formalisable” in $R_{c}$ . A coalgebraic proof would require:

A coalgebraic structure on the algebraic numbers $\overline{Q}$ (perhaps as a final coalgebra of an “algebraic-extension” functor).
A coalgebraic $exp$ as the unique coalgebra morphism $R_{c} \to Stream Fin (b)$ from the ODE $f^{'} = f$ universal property.

Open Problem 56. Formulate a coalgebraic Lindemann–Weierstrass theorem in HoTT.

11 Conclusion

We have given a coinductive characterisation of $π$ and $e$ in homotopy type theory, completing the programme sketched in Paper III §5 of the prior series. The principal new results are:

A clean statement of the coinduction principle in cubical HoTT (13).
Stream coalgebras realising digit expansions (14, 20).
Coalgebraic characterisations of $π$ and $e$ as unique unfolds satisfying bisimulation-closed observable predicates (33, 38, 39, 40).
An equivalence theorem (48) showing the coinductive presentation matches Booij’s HIIT $R_{c}$ on $[0, 1]$ .
A Dirichlet-series stream coalgebra (51) giving partial progress towards a coalgebraic $ζ$ .

An accompanying executable framework is provided in Haskell: the stream functor, unfold/corecursion, the carry-bisimulation, and the spigot algorithms for $π$ (Leibniz, Machin) and $e$ (factorial series), together with QuickCheck properties for stream operations and approximation round-trips. The Lean 4 companion file (using Mathlib’s Stream’ API) formalises the basic coalgebra structure, the corecursive unfold, and a (classical, set-level) coinduction principle; it does not include a formal proof of the productivity of the Sale or BBP transitions, which is left as 54. The Lean component should be read as a partial certification of the type-theoretic infrastructure, not as a complete formalisation of the main theorems. The full formalisation effort is substantial: the main open problem (50) is the construction of a HoTT-native coalgebraic Riemann zeta function with $ζ (s) = 0$ as a bisimulation-closed predicate; this remains far from solved.

Coinductively, the picture has unified beauty: $π$ is a stream, namely the unique stream produced by the BBP corecursive equation; $e$ is a stream, namely the unique stream produced by the factorial-series corecursive equation; $[0, 1]$ is the type of streams modulo carry; and equality of streams is exactly bisimulation. The HIIT route of Booij is one face of these objects; the final-coalgebra route is the other. Univalence binds them.

12 Prerequisites from the prior series, made explicit

To make the present paper self-contained, we restate (without re-proving) the prior results on which our arguments rely. Each is either a textbook fact found in the standard references on HoTT and coalgebra (see ), or a routine adaptation of a textbook fact to the cubical setting. Where we cite the prior series , the citation is to a particular textbook-style adaptation, and the underlying proofs are the standard ones.

Theorem 57 (A.1; cf. Paper III Theorem 5.2). For any type $A : U$ , the M-type $M (A, λ - . 1) ≅ A^{N}$ together with $out := ⟨ hd, tl ⟩$ is a final coalgebra of the endofunctor $F_{A} X = A \times X$ .

This is the cubical-HoTT version of Rutten §2 combined with ACS Theorem 3.5. We use it in the form proved by ACS.

Theorem 58 (A.2; cf. Paper III Theorem 5.3). For final coalgebra $(ν F, out)$ of polynomial endofunctor $F$ , two elements $x, y : ν F$ satisfy a path equality $x = y$ iff there exists an $F$ -bisimulation $R$ with $R (x, y)$ .

This is restated as our 13 and proved internally to the present paper.

Theorem 59 (A.3; cf. Paper III Theorem 4.1). There is, up to unique order-preserving HoTT-equivalence, a unique Dedekind-complete Archimedean ordered field $R$ . Booij’s Cauchy HIIT $R_{c}$ is one such; the quotient $(Z \times (Stream Fin (b))) / \sim_{b}^{'}$ for the natural extension of $\sim_{b}$ to $Z$ -shifted streams is another.

We use this in the form: the two presentations agree on $[0, 1]$ , which is 48.

Theorem 60 (A.4; cf. Paper V Definition 8.1, Theorem 5.7). In Booij’s HIIT $R_{c}$ , the type $Σ_{p : R_{c}} (sin p = 0) \times (p > 0) \times (\forall x \in (0, p), sin x > 0)$ is contractible. Its centre is by definition $π$ .

Theorem 61 (A.5; cf. Paper V Definition 8.2, Theorem 4.3). In Booij’s HIIT $R_{c}$ , the type $Σ_{f : R_{c} \to R_{c}} Σ_{x : R_{c}} (f^{'} = f) \times (f (0) = 1) \times (x = f (1))$ is contractible (the universal-property of $exp$ ). Its centre’s $x$ -component is by definition $e$ .

These five statements are the only places where the prior series enters our arguments. Reader who prefers to take them as assumptions of the present paper may do so; the rest of the paper then becomes a self-contained development atop these five axioms together with the standard cubical-HoTT infrastructure of .

13 Detailed state-space layout for the proof of Theorem 39

We expand the state-space promise of 39. The streaming-factorial spigot algorithm of maintains a state in $N^{5}$ : $(n, k, p, q, d)$ where $n$ is the digit position emitted so far, $k$ is the next factorial index ready to be summed, and $(p, q, d)$ are the bookkeeping triple of (current scaled remainder numerator, current scaled denominator, current digit-out).

The transition $γ_{e} : N^{5} \to Fin (b) \times N^{5}$ is:

Multiply $(p, q)$ by $b$ : $(p^{'}, q^{'}) := (b \cdot p, q)$ .
Extract the integer part: $d^{'} := p^{'} \div q^{'}$ , $p^{''} := p^{'} mod q^{'}$ . (In the cubical implementation $\div$ and $\mod$ are total constructive operations on $N$ .)
Update the position: $n^{'} := n + 1$ , $k^{'} := k$ (unchanged).
If the remainder $p^{''} / q^{'}$ is below the precision threshold $1/ q^{'}$ , advance the factorial: $q^{''} := q^{'} \cdot k^{'}$ , $k^{''} := k^{'} + 1$ , and re-normalise $p^{''}$ by adding the new term’s contribution.
Output: $(d^{'}, (n^{'}, k^{''}, p_{new}, q^{''}))$ , where $p_{new}$ is the renormalised remainder.

The state projection function $state : Stream Fin (b) \to N^{5}$ of 39 is the canonical retraction: $state (s) =$ the unique $c$ such that $s = unfold_{γ_{e}} (c)$ , when such $c$ exists. This is a partial function in general, but defined on the image of $unfold_{γ_{e}}$ , which is the only place it is used.

Compatibility of the up-to operator. The up-to operator $Φ$ used in the proof of 39 is $Φ (R) := {(u_{1}, u_{2}) : \exists c, c^{'} . R (unfold_{γ_{e}} (c), unfold_{γ_{e}} (c^{'})) \land u_{1} = unfold_{γ_{e}} (c) \land u_{2} = unfold_{γ_{e}} (c^{'})} .$ By , an up-to operator is compatible iff it preserves the evolution structure of the coalgebra. For our $γ_{e}$ this reduces to the observation that $unfold_{γ_{e}}$ is a coalgebra morphism: heads commute with $Φ$ by definition (they are determined by the first projection of $γ_{e}$ ), and tails commute by the recursive call. Hence $Φ$ is compatible and 27 applies.

Long, M. (2026). Universal Properties of Real Numbers and Transcendentals. Paper III, YonedaAI HoTT Foundations Series.

Long, M. (2026). The HoTT Perspective: Numbers as Inductive Types up to Path Equivalence. Paper V, YonedaAI HoTT Foundations Series.

Long, M. (2026). The Univalent Correspondence: How Six Perspectives on Number Become One. Synthesis Paper, YonedaAI HoTT Foundations Series.

Booij, A. (2020). Analysis in Univalent Type Theory. Ph.D. Thesis, University of Birmingham.

Rutten, J.J.M.M. (2000). Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1):3–80.

Jacobs, B. (2016). Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science.

Ahrens, B., Capriotti, P., & Spadotti, R. (2015). Non-wellfounded trees in homotopy type theory. Proc. TLCA.

Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2018). Cubical Type Theory: a constructive interpretation of the univalence axiom. IfCoLog Journal of Logics.

Birkedal, L., Møgelberg, R.E., Schwinghammer, J., & Støvring, K. (2012). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8.

Pous, D., & Sangiorgi, D. (2012). Enhancements of the bisimulation proof method, in Advanced Topics in Bisimulation and Coinduction, CUP.

Ghani, N., Hancock, P., & Pattinson, D. (2009). Continuous functions on final coalgebras. ENTCS 249:3–18.

Sale, A.H.J. (1968). The calculation of $e$ to many significant digits. The Computer Journal 11(2):229–230.

Rabinowitz, S., & Wagon, S. (1995). A spigot algorithm for the digits of $π$ . American Math. Monthly 102:195–203.

Gibbons, J. (2006). Unbounded spigot algorithms for the digits of pi. American Math. Monthly 113:318–328.

Bailey, D.H., Borwein, P., & Plouffe, S. (1997). On the rapid computation of various polylogarithmic constants. Mathematics of Computation 66:903–913.

Weihrauch, K. (2000). Computable Analysis: An Introduction. Springer.

Loeffler, D., & Stoll, M. (2025). Formalizing zeta and $L$ -functions in Lean. Annals of Formalized Mathematics 1. arXiv:2503.00959.

The Univalent Foundations Program. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.

Voevodsky, V. (2010). The univalence axiom and the foundations of mathematics. Lecture series, IAS.

Licata, D.R., & Shulman, M. (2013). Calculating the fundamental group of the circle in homotopy type theory. Proc. LICS.

Coquand, T. (1994). Infinite objects in type theory. Types for Proofs and Programs, Springer LNCS.

Rutten, J.J.M.M. (2003). Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science 308:1–53.

Aczel, P. (1988). Non-Well-Founded Sets. CSLI Lecture Notes 14.

Bordg, A., & Paulson, L. (2024). Coinductive proofs in Isabelle: streams revisited. Journal of Automated Reasoning.

Kleene, S.C. (1952). Introduction to Metamathematics. North-Holland.

Turing, A.M. (1937). On computable numbers, with an application to the Entscheidungsproblem. Proc. London Math. Soc. 42:230–265.

Kapulkin, K., & Lumsdaine, P.L. (2021). The simplicial model of univalent foundations (after Voevodsky). Journal of the European Mathematical Society 23:2071–2126.

Shulman, M. (2018). Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Math. Structures Comp. Sci. 28:856–941.

Sangiorgi, D. (2012). Introduction to Bisimulation and Coinduction. Cambridge University Press.

Abbott, M., Altenkirch, T., & Ghani, N. (2005). Containers: Constructing Strictly Positive Types. Theoretical Computer Science 342:3–27.