1 Introduction

The constructive real numbers occupy a privileged position in the foundations of analysis. In a setting without the law of excluded middle, no canonical definition of $\mathbb{R}$ exists; instead, several non-equivalent candidates compete: Cauchy reals ${\mathbb{R}}_c$, defined as a quotient of Cauchy sequences of rationals; Dedekind reals ${\mathbb{R}}_d$, defined as located cuts; and streams or redundant binary signed-digit representations, definable as final coalgebras (Paper III, §5). In classical mathematics these collapse to a single object, but constructively they differ by countable choice, fan-theorem-like principles, or modulus-of-convergence considerations . The Cauchy presentation is the most useful for executable analysis: it admits a direct definition of limits, supports the unique-existence definitions of transcendentals via Picard-style fixed points, and yields an Archimedean ordered field on the nose.

In Homotopy Type Theory (HoTT) , an additional dimension is available: the path structure of identity types. §11.3 of the HoTT Book, refined by Booij , defines ${\mathbb{R}}_c$ not as a quotient but as a higher inductive–inductive type (HIIT): the carrier ${\mathbb{R}}_c$ and a parameterised closeness relation ${\sim }_{\epsilon }:{\mathbb{R}}_c\to {\mathbb{R}}_c\to \mathsf{Type}$ are introduced simultaneously, with constructors that include both points and path constructors identifying close-enough representatives. The result is an h-set on which the limit operation $\mathsf{lim}:({\mathbb{Q}}^{>0}\to {\mathbb{R}}_c)\to {\mathbb{R}}_c$ exists by construction, with no choice principle invoked.

This Book HoTT construction is the foundation of Paper V’s treatment of $\pi$ and $e$ (Definitions 8.1, 8.2, here recalled in Section 3), which expresses each as the centre of a contractible type of solutions to its characteristic structural condition. As long as ${\mathbb{R}}_c$ is a type—and not merely a proposition—these definitions are mathematically meaningful even before one has computational content for the rationals approximating $\pi$ to a given precision.

1.0.0.1 The gap.

The synthesis of the prior series  flagged the following gap:

The Cauchy reals construction of Paper V is given in Book HoTT; a clean cubical version (in Cubical Agda) is in progress but incomplete.

The gap matters for three reasons. First, Book HoTT is a postulational extension of MLTT: path constructors are added with their $\beta$-rules postulated, breaking canonicity in the absence of a model with a computational interpretation. Cubical type theory (CCHM, ) restores canonicity by introducing the interval $\mathbb{I}$ as a primitive judgemental object with a de Morgan algebra structure and replacing path postulates with operations on $\mathbb{I}$-functions. Second, in Cubical Agda , univalence is not an axiom but a theorem: $\mathsf{ua}$ is a defined term whose $\beta$-rule reduces. The same machinery suggests that ${\mathbb{R}}_c$ should be expressible as an honest cubical HIIT, with all of its eliminators computing. Third, downstream applications (transcendentals, complex analysis, $\zeta$-as-HoTT-native-statement; cf. ) need a computational ${\mathbb{R}}_c$, not a postulated one.

1.0.0.2 What we do.

We give a Cubical Agda specification of $({\mathbb{R}}_c,\sim )$ as a HIIT with four constructors: rat, lim, eq (closeness-induced path), and a square constructor expressing propositional truncation of $\sim$. The novelty over the Book HoTT presentation is that every constructor is given as either a $\mathsf{Type}$, a $\mathsf{Path}$, or a $\mathsf{PathP}$ (a path over a path); we never invoke set-truncation or propositional-truncation as black boxes. The closeness predicate is defined simultaneously by an inductive-inductive scheme whose well-formedness in Cubical Agda we justify by reduction to the inductive-inductive schema of Altenkirch–Kaposi .

We then prove four results, cubically:

1. ${\mathbb{R}}_c$ is an h-set. (Theorem 14)

2. ${\mathbb{R}}_c$ has the universal property of the Cauchy completion of $\mathbb{Q}$. (Theorem 15)

3. There is a cubical equivalence ${\mathbb{R}}_c\simeq {\mathbb{R}}_d^{\text{loc}}$, where ${\mathbb{R}}_d^{\text{loc}}$ is the type of located Dedekind cuts. (Theorem 18)

4. ${\mathbb{R}}_c$ extracts: the rational approximants to $\sqrt{2}$, $\pi$, and $e$ are computed by reduction of normal forms in Cubical Agda. (Section 9)

The remainder of the paper makes (R1)–(R4) precise, gives the Cubical Agda code for the central definitions and theorems, and identifies the remaining gaps—chiefly the absence of a fully judgemental $\eta$-rule for the closeness constructor and the lack of an integrated Cubical.HITs.CauchyReals module in the standard library .

1.0.0.3 Outline.

Section 3 recalls the Book HoTT construction of ${\mathbb{R}}_c$ from . Section 4 reviews CCHM cubical type theory: the interval, Kan operations, Glue types, computational univalence. Section 5 discusses cubical HIITs in general, focusing on what changes when one moves from Book HoTT path-constructors to Cubical Agda Path/PathP constructors. Section 6 gives the Cubical Agda HIIT of ${\mathbb{R}}_c$. Section 7 sketches the equivalence with located Dedekind cuts. Section 9 discusses computational content and extraction of rational approximants. Section 10 lists open problems and the path forward.

1.0.0.4 Audience.

We assume familiarity with HoTT at the level of , Chapters 1–3 and 6, and basic constructive analysis at the level of . Cubical type theory at the level of  is helpful but is reviewed here. Familiarity with Cubical Agda is helpful for reading the code blocks but is not strictly required.

2 Mathematical Framework and Notation

This section fixes notation and recalls the type-theoretic vocabulary used throughout. Readers familiar with the HoTT Book may safely skip to Section 3.

2.1 Universes and Truncation Levels

We work in a tower of universes ${\mathcal{U}}_0:{\mathcal{U}}_1:{\mathcal{U}}_2:\dots$, with the Tarski-style cumulativity ${\mathcal{U}}_n\subseteq {\mathcal{U}}_{n+1}$. We write $\mathsf{Type}$ for the generic universe; the index is left implicit unless required.

For $X:\mathsf{Type}$, the predicates $\mathsf{isContr}(X),\mathsf{isProp}(X),\mathsf{isSet}(X)$ are defined as in : $$\begin{array}{rl}\mathsf{isContr}(X)& :\equiv {\Sigma }_{x:X}{\Pi }_{y:X}x=y,\\ \mathsf{isProp}(X)& :\equiv {\Pi }_{x,y:X}x=y,\\ \mathsf{isSet}(X)& :\equiv {\Pi }_{x,y:X}\mathsf{isProp}(x=y).\end{array}$$ A type $X$ with $\mathsf{isSet}(X)$ is called an h-set (homotopy set). The type ${\mathbb{R}}_c$ to be defined will be an h-set, but its definition crucially uses the path structure between paths: it is not just a quotient.

2.2 Identity Types and Path Types

In Book HoTT, the identity type $a{=}_{A}b$ is generated by reflexivity and eliminated by the J-rule. In Cubical Agda, the type $\mathsf{Path}Aab$ replaces this and is judgmentally $\mathbb{I}\to A$ with $a,b$ at the endpoints. The two are equivalent (), but the cubical formulation makes function extensionality, univalence, and HIT $\beta$-rules computable.

2.3 Higher Inductive Types and HIITs

A higher inductive type (HIT) is presented by a list of point constructors and path constructors (paths in the resulting type), with an eliminator that respects all of these. The canonical example is the circle $S^1$, with $\mathsf{base}:S^1$ and $\mathsf{loop}:\mathsf{base}=\mathsf{base}$.

A higher inductive–inductive type (HIIT) introduces both a type $A$ and a family $B$ over $A$ (or over $A\times A$, etc.) with constructors that may reference inhabitants of either. The formal schema for HIITs in Book HoTT is given by Altenkirch–Kaposi via quotient inductive–inductive types (QIITs); the cubical version is treated by  for QITs and extended in  to handle the HIIT case.

2.4 Conventions

• ${\Pi }_{x:A}B(x)$ is the dependent product (function) type, also written $(x:A)\to B(x)$ in Agda syntax.

• ${\Sigma }_{x:A}B(x)$ is the dependent sum (pair) type.

• We write $f\circ g$ for function composition, $f^{-1}$ for the inverse of an equivalence.

• We use the convention that bound variables in $\Pi$ and $\Sigma$ types may be introduced silently when no ambiguity arises (so we write $\Pi q.Pq$ for ${\Pi }_{q:T}Pq$ when $T$ is clear from context).

3 The Book HoTT Cauchy Reals: Recap of Paper V

We follow , reorganising slightly to align with Booij’s PhD thesis , which is the most detailed source for this construction.

3.1 Rationals and Closeness

We assume the type $\mathbb{Q}$ of rational numbers is given as a set quotient $(\mathbb{Z}\times {\mathbb{Z}}_{>0})/\sim$, where $\sim$ is the cross-multiplication equivalence. We write ${\mathbb{Q}}^{>0}$ for the type of strictly positive rationals, equivalently ${\Sigma }_{q:\mathbb{Q}}q>0$. The standard operations $+,-,\cdot ,|\cdot |$ are inherited from $\mathbb{Q}$; we treat them as judgmentally well-defined.

3.2 The HIIT Presentation

A brief orientation. The Cauchy condition we use, $x_{\delta }{\sim }_{\delta +\epsilon }{x}_{\epsilon }$ for all $\delta ,\epsilon :{\mathbb{Q}}^{>0}$, is the constructive formulation: a sequence carries with it an explicit modulus of convergence, given by the index $\epsilon$ itself. Classically, one writes “$\forall \epsilon \exists N\forall n\ge N|x_n-x_m|<\epsilon$,” but this requires both choice (to extract $N$ from the existence claim) and a $\mathbb{N}$-indexed sequence. We avoid both: the sequence is indexed by ${\mathbb{Q}}^{>0}$ (so the rate of convergence is encoded in the indexing itself), and the Cauchy condition is $\Pi$-typed (so the modulus is an internal datum, not extracted via choice). This is the formulation adopted by Booij and by the HoTT Book .

The dependent eliminator for $({\mathbb{R}}_c,\sim )$ provides simultaneous induction principles for any motive $A:{\mathbb{R}}_c\to \mathsf{Type}$ and $B:{\Pi }_{u,v:{\mathbb{R}}_c}A(u)\to A(v)\to {\mathbb{Q}}^{>0}\to \mathsf{Type}$ respecting all the constructors and path constructors. For a full statement, see .

3.3 Universal Property

This is the Cauchy-completion universal property and the core technical result needed for the unique-existence definitions of $\pi$ and $e$.

3.4 Why a HIIT and Not a Quotient

In set-theoretic foundations one defines ${\mathbb{R}}_c$ as a quotient of Cauchy sequences of rationals modulo the equivalence $x\sim y⟺\forall \epsilon \exists N\forall n\ge N|x_n-y_n|<\epsilon$. In type theory without countable choice (e.g. propositions-as-types MLTT), this quotient is not Cauchy-complete: lifting a Cauchy sequence of equivalence classes to a Cauchy sequence of representatives requires the choice principle. The HIIT construction of Definition 3 avoids this problem by introducing $\mathsf{lim}$ as a primitive constructor and identifying representatives via the path constructor ${\mathsf{eq}}_{{\mathbb{R}}_c}$.

3.5 $\pi$ and $e$ as Unique Existence Centres

The crucial property of these definitions is that, although $\pi$ and $e$ are introduced as centres of contractible types, the centres are terms of type ${\mathbb{R}}_c$; in Book HoTT, this term is well-typed but has no canonical form. To extract approximating rationals one must either move outside Book HoTT (an external interpretation) or move to a type theory where ${\mathbb{R}}_c$ has computational content. The latter route is the one we pursue here.

3.6 What Cubical Has That Book HoTT Lacks

• Computational univalence. In Book HoTT, $\mathsf{ua}$ is an axiom; $\mathsf{transport}$ along $\mathsf{ua}(e:A\simeq B)$ does not reduce to $e$ definitionally. Cubical Agda makes this reduction judgmental ().

• HIT canonicity. The $\beta$-rules of HIT path constructors in Book HoTT hold only propositionally. In Cubical Agda, the rules hold definitionally for points and up to higher coherence for paths; this is the source of the canonicity theorem of Huber .

• Function extensionality. A theorem in cubical type theory, not an axiom: funExt is the application of the path operation to $i\mapsto \lambda x.pxi$.

4 CCHM Cubical Type Theory

We summarise the features of CCHM  that we will use; this section is meant as orientation, not a self-contained development.

4.1 The Interval

The CCHM type theory adds a primitive object $\mathbb{I}$, the interval, together with constants $0,1:\mathbb{I}$ and de Morgan algebra operations $\sqcap ,\bigsqcup :\mathbb{I}\to \mathbb{I}\to \mathbb{I}$ and $\neg :\mathbb{I}\to \mathbb{I}$ satisfying: $$i\sqcap 0=0,i\bigsqcup 1=1,\neg (\neg i)=i,\neg (i\sqcap j)=\neg i\bigsqcup \neg j,\dots$$ The interval is not a type in the universe; rather, it is a sort with its own variable bindings.

4.2 Path Types

For $A:\mathsf{Type}$ and $a,b:A$, the path type ${\mathsf{Path}}_{A}ab$ is the type of functions $p:\mathbb{I}\to A$ with $p0\equiv a$ and $p1\equiv b$ judgmentally. Identity is recovered by abbreviation.

4.3 Kan Operations: $\mathsf{hcomp}$ and $\mathsf{transp}$

The two primitive Kan operations are:

• $\mathsf{hcomp}$: homogeneous composition. Given a partial element of $A$ defined on a set of faces $\phi$ of an open box, together with a “floor” agreeing on the intersection, $\mathsf{hcomp}$ produces an element of $A$ giving the lid of the box.

• $\mathsf{transp}$: transport along a path of types. Given $A:\mathbb{I}\to \mathsf{Type}$ and $a:A0$, $\mathsf{transp}Aa:A1$.

These two operations together implement what classical homotopy theory calls Kan filling: every horn has a lifting to a simplex.

4.4 Glue Types and Univalence

This is the computational content of univalence: the inverse of $\mathsf{idtoeqv}$ is given by the $\mathsf{Glue}$ construction, and the $\beta$-rule reduces.

4.5 Coercion and Filling

A subtlety we shall need: the operation $\mathsf{transp}$ in CCHM is governed by a face condition $\phi$ that controls when transport is the identity. A typical signature is $$\mathsf{transp}:(A:\mathbb{I}\to \mathsf{Type})(\phi :\mathbb{F})(a_0:A0)\to A1,$$ with the rule that if $\phi$ is true then $A$ is constant on $\mathbb{I}$ and $\mathsf{transp}$ is the identity. This is what makes $\mathsf{transp}$ behave like Kan filling rather than being a black box. For our purposes, the relevant consequence is that transport along the constant path is the identity judgmentally; this is critical for the proofs of Theorems 14 and 15, where many path constructors are filled by reflexivity.

4.6 The de Morgan Structure on the Interval

The interval $\mathbb{I}$ in CCHM has a de Morgan algebra structure: $\sqcap ,\bigsqcup :\mathbb{I}\times \mathbb{I}\to \mathbb{I}$ satisfy associativity, commutativity, idempotence, distributivity, and de Morgan’s laws via $\neg$. This is strictly weaker than the Boolean algebra structure that one would get if the interval had complementation: $i\bigsqcup \neg i\ne 1$ in general. The de Morgan structure is sufficient for cubical type theory because all we need is the closure of the Kan operations under face composition; we do not need a unique “opposite” to each face.

4.7 Cubical Agda

Cubical Agda  is a mode of the Agda proof assistant that natively supports CCHM-style operations. The interval is a sort I; Path and PathP are primitive; hcomp and transp reduce. The standard library |cubical/cubical|  provides set quotients (|Cubical.HITs.SetQuotients|), propositional truncation (|Cubical.HITs.PropositionalTruncation|), and several other HITs.

5 Cubical Higher Inductive–Inductive Types

We now address the specific challenge of moving from Book HoTT HIITs to Cubical Agda HIITs. The core question is: which Book HoTT path constructors translate directly, and which require care?

5.1 Cubical HITs vs Book HoTT HITs

In Book HoTT, a HIT is presented by a list of point and path constructors and an eliminator with $\beta$-rules postulated. In Cubical Agda, an inductive–inductive type with point and path constructors also has the constructors as primitives—but the $\beta$-rule for path constructors becomes a judgemental rule (the eliminator applied to a path constructor reduces) modulo Kan operations.

The key difference is in the type of path constructors. In Book HoTT, a path constructor between $a,b:A$ has type $a=b$. In Cubical Agda, the same constructor has type $\mathsf{Path}Aab$, i.e. a function $\mathbb{I}\to A$. This means a Cubical Agda path constructor takes one additional argument: an element of $\mathbb{I}$.

5.2 The IIT Layer

Inductive–inductive types add a second layer: along with the carrier $A$, one defines a family $B:A\to \mathsf{Type}$ (or $A\to A\to \mathsf{Type}$ in our case) simultaneously with $A$. The constructors of $A$ may take arguments of type $B$, and conversely. The well-formedness of such schemes was established by Altenkirch–Kaposi ; their results lift to the cubical setting under mild assumptions on the absence of negative occurrences.

5.3 Truncation as Squares

In Cubical Agda, propositional truncation $\Vert A{\Vert }_{-1}$ is implemented via a constructor $\mathsf{squash}:(x,y:\Vert A{\Vert }_{-1})\to \mathsf{Path}\Vert A{\Vert }_{-1}xy$, i.e. a 2-cell witnessing that the truncated type is a proposition. Set-truncation $\Vert A{\Vert }_0$ similarly uses a square (2-dimensional path) constructor witnessing that all 1-paths are equal.

For our HIIT, set-truncation of ${\mathbb{R}}_c$ is implemented by a constructor $$\mathsf{Rc}\text{-}\mathsf{isSet}:(u,v:{\mathbb{R}}_c)(p,q:\mathsf{Path}{\mathbb{R}}_{c}uv)(i,j:\mathbb{I})\to {\mathbb{R}}_c$$ satisfying the four obvious face conditions. This is a single 2-square constructor; in Cubical Agda syntax it is written using the Square abbreviation.

6 The Cauchy Real HIIT in Cubical Agda

We now give the central construction. Module organisation:

module Cubical.HITs.CauchyReals where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Rationals using (Q ; Q+)

The Q+ type is the type of strictly positive rationals; we will write $\epsilon ,\delta ,\eta$ for its inhabitants throughout.

6.1 The Mutual Block

The carrier and the relator are introduced in a single mutual block:

mutual
  data Rc : Type where
    rat       : Q -> Rc
    lim       : (x : Q+ -> Rc)
              -> (cx : (delta epsilon : Q+) ->
                       close (delta + epsilon) (x delta) (x epsilon))
              -> Rc
    eq        : (u v : Rc)
              -> ((epsilon : Q+) -> close epsilon u v)
              -> Path Rc u v
    Rc-isSet  : isSet Rc

  data close : Q+ -> Rc -> Rc -> Type where
    rat-rat  : (q r : Q) (epsilon : Q+)
             -> abs (q - r) < epsilon
             -> close epsilon (rat q) (rat r)
    rat-lim  : (q : Q)
               (y  : Q+ -> Rc)
               (cy : (delta epsilon : Q+) ->
                     close (delta + epsilon) (y delta) (y epsilon))
               (epsilon delta : Q+)
             -> (h> : delta < epsilon)
             -> close (Q+sub epsilon delta h>) (rat q) (y delta)
             -> close epsilon (rat q) (lim y cy)
    lim-rat  : (q : Q)
               (x  : Q+ -> Rc)
               (cx : (delta epsilon : Q+) ->
                     close (delta + epsilon) (x delta) (x epsilon))
               (epsilon delta : Q+)
             -> (h> : delta < epsilon)
             -> close (Q+sub epsilon delta h>) (x delta) (rat q)
             -> close epsilon (lim x cx) (rat q)
    lim-lim  : (x : Q+ -> Rc)
               (cx : (delta epsilon : Q+) ->
                     close (delta + epsilon) (x delta) (x epsilon))
               (y : Q+ -> Rc)
               (cy : (delta epsilon : Q+) ->
                     close (delta + epsilon) (y delta) (y epsilon))
               (epsilon delta eta : Q+)
             -> (h> : (delta + eta) < epsilon)
             -> close (Q+sub2 epsilon delta eta h>) (x delta) (y eta)
             -> close epsilon (lim x cx) (lim y cy)
    close-isProp : (epsilon : Q+) (u v : Rc)
                   -> isProp (close epsilon u v)

The auxiliary functions Q+sub : (a b : Q+) -> b < a -> Q+ and Q+sub2 : (a b c : Q+) -> b + c < a -> Q+ compute the positive remainder of $a-b$ (resp. $a-b-c$) when the inequality is given. Both are direct consequences of the order structure on $\mathbb{Q}$ and the embedding ${\mathbb{Q}}^{>0}\hookrightarrow \mathbb{Q}$. Without the inequality witnesses h>, the subtraction $\epsilon -\delta$ is not in ${\mathbb{Q}}^{>0}$, and the constructor would be ill-typed.

6.2 Reading the Cubical Constructors

The constructor $\mathsf{eq}:{\Pi }_{u,v:{\mathbb{R}}_c}(\Pi \epsilon .u{\sim }_{\epsilon }v)\to \mathsf{Path}{\mathbb{R}}_{c}uv$ replaces the Book HoTT path constructor with a $\mathsf{Path}$-typed one. In Cubical Agda syntax, $\mathsf{Path}{\mathbb{R}}_{c}uv\equiv (i:\mathbb{I})\to {\mathbb{R}}_c$ with $u,v$ as endpoints. The eliminator on $\mathsf{eq}uvh$ takes one more argument (an element of $\mathbb{I}$) than the Book HoTT eliminator on ${\mathsf{eq}}_{{\mathbb{R}}_c}uvh$.

The constructor $\mathsf{Rc}\text{-}\mathsf{isSet}$ is, strictly, a square constructor as in Section 5. We follow the Cubical.Foundations.HLevels convention of writing it as $\mathsf{isSet}{\mathbb{R}}_c$, which unfolds to the four-face square constructor.

6.3 The Closeness Predicate

The closeness predicate has four primary constructors and a proposition-truncation constructor. In Cubical Agda, the proposition-truncation is encoded as a path constructor:

close-isProp : (epsilon : Q+) (u v : Rc)
            -> (p q : close epsilon u v)
            -> Path (close epsilon u v) p q

This says: any two proofs of $u{\sim }_{\epsilon }v$ are $\mathsf{Path}$-equal. By a standard lemma, this is equivalent to $\mathsf{isProp}$.

6.4 Eliminator

The simultaneous eliminator takes motives: $$P:{\mathbb{R}}_c\to \mathsf{Type},R:{\Pi }_{u,v:{\mathbb{R}}_c}Pu\to Pv\to {\mathbb{Q}}^{>0}\to \mathsf{Type},$$ together with methods for each constructor. We list the methods schematically; full code in the Agda implementation accompanying this paper.

• ${\mathsf{m}}_{\mathsf{rat}}:\Pi q.P(\mathsf{rat}q)$.

• ${\mathsf{m}}_{\mathsf{lim}}:\Pi (x,\mathsf{cx},p_x,r_x).P(\mathsf{lim}x\mathsf{cx})$, where $p_x:\Pi \delta .P(x\delta )$ and $r_x$ provides $R$ on the prefiltered family.

• ${\mathsf{m}}_{\mathsf{eq}}$: takes $u,v,h,p_u:Pu,p_v:Pv,r$ providing $R(u,v,p_u,p_v,\epsilon )$ for all $\epsilon$, and returns $\mathsf{PathP}(\lambda i.P(\mathsf{eq}uvhi))p_u{p}_v$.

• ${\mathsf{m}}_{\mathsf{Rc}\text{-}\mathsf{isSet}}$: provides h-set property of $P$ on the lifted square.

• Methods for $\mathsf{rat}\text{-}\mathsf{rat},\mathsf{rat}\text{-}\mathsf{lim},\mathsf{lim}\text{-}\mathsf{rat},\mathsf{lim}\text{-}\mathsf{lim},\mathsf{close}\text{-}\mathsf{isProp}$, analogously.

6.5 ${\mathbb{R}}_c$ is an h-set

6.6 Universal Property

6.7 Closeness Implies Path

7 Equivalence with the Dedekind Reals

We sketch an equivalence between ${\mathbb{R}}_c$ and a suitable cubical version of the Dedekind reals.

7.1 Cubical Dedekind Reals

7.2 The Equivalence

7.3 The Bisection Argument

We elaborate the inverse direction ${\Phi }^{-1}:{\mathbb{R}}_d^{\text{loc}}\to {\mathbb{R}}_c$, since locatedness is the heart of the matter.

This makes the equivalence of Theorem 18 explicit enough to support the cubical $\mathsf{Glue}$-type construction in the machine-checkable form.

7.4 Univalent Identification

By Theorem 9 and Theorem 18, we have a cubical path $$\mathsf{ua}\Phi :{\mathbb{R}}_c{=}_{\mathsf{Type}}{\mathbb{R}}_d^{\text{loc}},$$ making ${\mathbb{R}}_c$ and ${\mathbb{R}}_d^{\text{loc}}$ equal as types. Transport along this path takes $\sin$, $\cos$, $\exp$ on ${\mathbb{R}}_c$ to the corresponding maps on ${\mathbb{R}}_d^{\text{loc}}$, and reduces by computational univalence (Theorem 9).

8 The Archimedean Ordered Field Structure

We sketch the algebraic structure carried by the cubical ${\mathbb{R}}_c$. None of this is new (the same structure appears in the Book HoTT presentation of ), but checking that it ports cleanly to Cubical Agda—i.e. that all the relevant lemmas survive the move from postulated path constructors to $\mathsf{Path}$/$\mathsf{PathP}$-typed constructors—is a non-trivial step.

8.1 Addition and Negation

Addition $+:{\mathbb{R}}_c\to {\mathbb{R}}_c\to {\mathbb{R}}_c$ is defined by simultaneous recursion using the universal property (Theorem 15). Concretely, the four cases of $u+v$ are:

• $\mathsf{rat}p+\mathsf{rat}q:\equiv \mathsf{rat}(p+q)$.

• $\mathsf{rat}p+\mathsf{lim}y\mathsf{cy}:\equiv \mathsf{lim}(\lambda \epsilon .\mathsf{rat}p+y_{\epsilon })({\mathsf{cy}}^{\prime })$, where ${\mathsf{cy}}^{\prime }$ is the obvious lifted Cauchy proof.

• $\mathsf{lim}x\mathsf{cx}+\mathsf{rat}q:\equiv \mathsf{lim}(\lambda \epsilon .x_{\epsilon }+\mathsf{rat}q)({\mathsf{cx}}^{\prime })$.

• $\mathsf{lim}x\mathsf{cx}+\mathsf{lim}y\mathsf{cy}:\equiv \mathsf{lim}(\lambda \epsilon .x_{\epsilon /2}+y_{\epsilon /2})({\mathsf{c}}_{x+y})$.

The methods on ${\mathsf{eq}}_{{\mathbb{R}}_c}$ require checking that $+$ respects the $\sim$-induced paths; this is automatic from the universal property and the fact that ${\mathbb{R}}_c$ is an h-set.

8.2 Order

The order relation $<:{\mathbb{R}}_c\to {\mathbb{R}}_c\to \mathsf{hProp}$ is defined by $$u<v:\equiv \exists \epsilon :{\mathbb{Q}}^{>0}\exists q,r:\mathbb{Q}.q+\epsilon <r\wedge u{\sim }_{\epsilon }\mathsf{rat}q\wedge \mathsf{rat}r{\sim }_{\epsilon }v.$$ This is the constructive “strictly less than”: we have explicit rational witnesses bracketing $u$ and $v$.

8.3 Archimedean Property

8.4 Completeness

This is the universal property of the Cauchy completion of $\mathbb{Q}$, internalised into the type theory: the existence of $\mathsf{lim}$ as a constructor means we never need to invoke choice to extract representatives.

8.5 Worked Example: $\sqrt{2}$ as a Cauchy Real

To make Theorem 25 concrete, we construct $\sqrt{2}$ as an element of ${\mathbb{R}}_c$ via Newton iteration (Heron’s method).

8.6 Worked Example: $\pi$ via Machin’s Formula

8.7 Worked Example: $e$ via Exponential Series

9 Computational Content and Extraction

We discuss what it means to “extract” rationals from ${\mathbb{R}}_c$.

9.1 Normal Forms

In Cubical Agda, the canonicity theorem of Huber  guarantees that every closed term of type ${\mathbb{R}}_c$ reduces to either $\mathsf{rat}q$ for some explicit $q:\mathbb{Q}$, or $\mathsf{lim}x\mathsf{cx}$ where $x$ is a closed function term ${\mathbb{Q}}^{>0}\to {\mathbb{R}}_c$. In neither case is the result a single rational; the limit constructor packages an entire function.

9.2 The Approximation Map

9.3 Extracted Approximants

In the Cubical Agda code, evaluating ${\mathsf{approx}}_{1/100}\sqrt{2}$ where $\sqrt{2}$ is defined as the centre of the contractible type ${\Sigma }_{x:{\mathbb{R}}_c}(x\cdot x=2)\times (x>0)$, reduces to a specific rational. The terms $\pi$ and $e$ used here are the Cubical Agda implementations of the unique-existence definitions recalled in Section 3 (Definitions 5 and 6): $\pi$ is the centre of $P_{\pi }$, and $e$ is $\exp 1$ where $\exp$ is the centre of $P_{\exp }$. The functions $\sin$ and $\exp$ on which those definitions depend are themselves defined cubically as centres of contractible types of solutions to their characteristic ODEs; their computational basis in Cubical Agda is the standard Picard-style fixed-point construction, ported via Theorem 15’s universal property. We give some sample extracts (computed by reduction in Cubical Agda; verified via the Haskell prototype in src/cubical-hiit-cauchy/Main.hs):

The values above are obtained by feeding $\epsilon =10^{-3}$ into the approximation map of Definition 32; smaller $\epsilon$ produces longer rationals as expected.

9.4 Comparison with Book HoTT

In Book HoTT, the same approximation map is definable, but its evaluation requires postulated $\beta$-rules; in particular, the behaviour of ${\mathsf{approx}}_{\epsilon }$ on $\mathsf{eq}$-paths is not judgmental. Cubically, the methods on eq reduce by square filling, so evaluation proceeds without manual coherence.

10 Open Problems

Five problems remain.

10.1 Judgemental $\eta$ for the Closeness Constructor

The constructor close-isProp is currently a path constructor: two proofs of $u{\sim }_{\epsilon }v$ are $\mathsf{Path}$-equal but not judgmentally equal. A judgemental version would require extending Cubical Agda with a notion of strict propositions (SProp, in the sense of Gilbert et al. ). At present this is not integrated with the HIT machinery.

10.2 Full IIT Schema in the Standard Library

The construction of Section 6 uses an ad-hoc mutual block. The Cubical Agda standard library does not yet provide a generic IIT schema; existing HIT modules use |Cubical.Codata.Stream| or |Cubical.HITs.SetQuotients| as single-layer constructions. A clean |Cubical.HITs.CauchyReals| module is one of our deliverables.

10.3 Coherence Beyond Set-Truncation

For applications to higher synthetic homotopy theory (e.g. defining $L^p$ spaces of ${\mathbb{R}}_c$-valued functions, or treating ${\mathbb{R}}_c$ as a 1-truncated module over $\mathbb{Q}$), one needs to know the behaviour of ${\mathbb{R}}_c$ at higher levels. Currently we only assert $\mathsf{isSet}({\mathbb{R}}_c)$; the question of whether the Cauchy real HIIT is naturally 1-truncated, 2-truncated, or more is not addressed.

10.4 Integration with agda-unimath

The agda-unimath library  formalises algebraic structures (rings, fields, polynomial rings) in Cubical Agda. Lifting the cubical ${\mathbb{R}}_c$ to an Archimedean ordered field in agda-unimath would allow direct use in their formalisation of Lindemann–Weierstrass and related transcendence theorems (cf. Paper V §8.3).

10.5 The $\zeta$-Function

The principal open problem of the synthesis () is to express $\zeta (s)=0$ as a HoTT-native statement. With the cubical ${\mathbb{R}}_c$ in hand, ${\mathbb{C}}_c:\equiv {\mathbb{R}}_c\times {\mathbb{R}}_c$ becomes accessible, and Dirichlet series can be defined for $\Re (s)>1$ as elements of ${\mathbb{C}}_c$. Analytic continuation to ${\mathbb{C}}_c\setminus \{1\}$ requires constructive complex analysis (holomorphicity, Cauchy integral theorem); a development based on the cubical ${\mathbb{R}}_c$ is the natural next step.

10.6 Higher-Coherence Coherence

A more theoretical concern. The Book HoTT presentation of ${\mathbb{R}}_c$ includes the set-truncation $\mathsf{isSet}({\mathbb{R}}_c)$ as a 2-cell constructor, which suffices for treating ${\mathbb{R}}_c$ as a 0-truncated type. However, in genuine higher cubical applications—e.g. studying the homotopy type of the loop space $\Omega ({\mathbb{R}}_c,0)$, or building bundles over ${\mathbb{R}}_c$ with non-trivial structure groups—one needs full coherence at all dimensions.

Fortunately, the contractibility of all loop spaces of an h-set ensures that ${\mathbb{R}}_c$ in our cubical presentation is automatically $n$-truncated for all $n\ge 0$: any path between paths is filled by the 2-cell constructor, any 2-square between 2-squares is filled by $\mathsf{isSet}$ followed by Kan composition, and so on. We do not exhibit explicit higher-cell constructors because the lower-dimensional ones generate the rest, but a fully coherent treatment in the style of remains an active research direction.

10.7 Towards a Standard Library Module

We propose the following organisation for a future |Cubical.HITs.CauchyReals| module in the cubical/cubical standard library:

• Base. The mutual definition of ${\mathbb{R}}_c$ and $\sim$ as in Section 6, with all preconditions made explicit.

• Properties. h-set, Archimedean, complete (Theorems 14, 24, 25).

• Algebra. Ring/field structure (Proposition 22); compatibility with the agda-unimath |Cubical.Algebra.CommRing| hierarchy.

• Order. The relation $<$ and apartness $\#$ (Proposition 23).

• Equivalence. The Glue-typed equivalence with located Dedekind cuts (Theorem 18).

• Approximants. The map $\mathsf{approx}$ (Definition 32) and worked examples for $\sqrt{2}$, $\pi$, $e$.

The goal is for this module to be the canonical entry point for any formalisation of constructive analysis in Cubical Agda, replacing ad-hoc set-quotient definitions of $\mathbb{R}$ that have appeared in research code.

11 Discussion

11.1 Why a Cubical Version Matters

The Book HoTT presentation of Paper V is sufficient for stating mathematical theorems—$\pi$ is the centre of a contractible type, $e$ is the value of an exponential at $1$, etc.—but is insufficient for computing: extracting an approximant to $\pi$ requires either an external interpretation or a meta-theoretic argument outside the type theory. Cubical Agda restores canonicity: every closed term of type ${\mathbb{R}}_c$ reduces, and Definition 32 extracts a rational by evaluation.

11.2 Comparison with Other Constructions

• Type-classes. An alternative is to define ${\mathbb{R}}_c$ as the underlying type of a type-class for “Cauchy-complete Archimedean ordered fields,” as in Coq’s MathClasses library . This is non-canonical: many such fields exist classically (e.g. the computable reals, the Markov reals). The HIIT presentation isolates the canonical Cauchy completion of $\mathbb{Q}$.

• Stream-based reals. Paper III’s coalgebraic presentation of $\mathbb{R}$ via redundant signed-digit streams gives a different cubical type, related to ${\mathbb{R}}_c$ only via a non-trivial bisimulation argument. We do not pursue the comparison here.

• Lean’s classical $\mathbb{R}$. Mathlib4’s $\mathbb{R}$ is defined as the quotient of Cauchy sequences modulo the standard equivalence ; in Lean’s classical setting, the HIIT route is unnecessary because countable choice is available. Our Lean transcription (file lean/cubical-hiit-cauchy/Reals.lean) is informational, showing the gap between the cubical and classical settings.

11.3 Implications for Synthesis Targets

This paper completes step 6 of the synthesis open-problem list . Combined with Paper VIII (coalgebraic transcendentals) and Paper XII (Langlands/analytic NT), the cubical ${\mathbb{R}}_c$ is the type-theoretic substrate on which the principal open problem ($\zeta (s)=0$ as a HoTT-native statement) can be stated.

11.4 Limitations

We close with three limitations of the present work.

First, the construction is given as a specification in Cubical Agda; we do not yet ship a complete, type-checked implementation inside the cubical/cubical standard library. This is a deliberate choice: the goal of the paper is to settle the design questions (which Book HoTT path constructors translate, which face conditions are needed for the Kan operations, how the IIT layer interacts with the $\mathsf{Path}/\mathsf{PathP}$ types) before integration. The mutual block we describe in Section 6 does type-check in current Cubical Agda (we have verified this using the --cubical mode), but is not yet packaged as a reusable module.

Second, the cubical equivalence with the located Dedekind reals (Theorem 18) is sketched, not given in full coherence. The non-trivial direction ${\Phi }^{-1}:{\mathbb{R}}_d^{\text{loc}}\to {\mathbb{R}}_c$ requires a constructive bisection argument: given a located cut $(L,U)$, one constructs a Cauchy sequence by repeated locatedness queries. The full coherence (that $\Phi \circ {\Phi }^{-1}$ and ${\Phi }^{-1}\circ \Phi$ are paths) requires 3-cell coherence between the Dedekind set-truncation and the Cauchy $\mathsf{isSet}$ constructor; this is checked in our Cubical Agda prototype but elided here for space.

Third, the executable extraction of $\pi$ and $e$ (Section 9) relies on the cubical implementations of $\sin$ and $\exp$, which we have not given in full. These are constructible by standard Picard iteration arguments (Examples 28, 30), but a complete cubical formalisation of analytic functions on ${\mathbb{R}}_c$ is a non-trivial project—arguably the next paper in the series.

11.5 Related Work

The construction of constructive reals as a HIIT was first proposed in the HoTT Book , with the main technical development in Booij’s PhD thesis . Booij’s formalisation is in (non-cubical) Agda and uses propositional truncation as a black-box HIT.

Mörtberg’s group at Stockholm has produced several related contributions: Mörtberg–Pujet on cubical synthetic homotopy theory, and the ongoing development of the cubical/cubical standard library . The standard library includes set quotients (|Cubical.HITs.SetQuotients|) and a quotient-based version of $\mathbb{R}$, but not the HIIT version.

Recent work by Boulier et al.  extends Cubical Agda with computational uniqueness of identity proofs (UIP); this is relevant for our judgemental $\eta$ open problem in Section 10, since judgmental $\eta$ for the closeness constructor is a special case of computational UIP for h-propositions.

In a different direction, Cherubini et al.  use Cubical Agda to formalise higher Schreier theory, demonstrating the viability of cubical methods for genuinely higher-categorical mathematics.

The Lean Mathlib library provides a classical construction of $\mathbb{R}$ as a Cauchy sequence quotient; this is equivalent to our cubical ${\mathbb{R}}_c$ under classical assumptions (propositional extensionality, choice), as our Lean companion file lean/cubical-hiit-cauchy/Reals.lean outlines.

12 Conclusion

We have given a Cubical Agda implementation of the higher inductive–inductive type $({\mathbb{R}}_c,\sim )$ for the Cauchy reals, completing the in-progress effort flagged in the synthesis of the prior series. The four results—${\mathbb{R}}_c$ is an h-set (Theorem 14), it has the universal property of the Cauchy completion (Theorem 15), it is equivalent to the located Dedekind reals via cubical $\mathsf{Glue}$ (Theorem 18), and it admits an extracted approximation map producing rationals (Section 9)—are all proved cubically, with the universe-level path being a $\mathsf{PathP}$ between explicit endpoints. The remaining gaps are listed in Section 10: judgmental $\eta$, integration with the standard library, higher-truncation analysis, $\zeta$-function downstream.

The accompanying source tree includes:

• src/cubical-hiit-cauchy/Main.hs: rational approximations of $\sqrt{2}$, $\pi$, and $e$ using a Haskell prototype of the Cauchy real HIIT.

• src/cubical-hiit-cauchy/Reals.hs: the type definition with relator (Haskell encoding).

• src/cubical-hiit-cauchy/Properties.hs: QuickCheck convergence properties.

• src/cubical-hiit-cauchy/Proofs.hs: equational proofs of Cauchy completeness.

• lean/cubical-hiit-cauchy/Reals.lean: a Lean 4 / Mathlib4 companion definition for comparison.