## Definition ## A **rational interval coalgebra** is a type $I$ with a [[strict order]] $\lt$, terms $0:$, $1:I$, a term $p: 0 \lt 1$ * a [[partial function]] from $\mathbb{N} \times \mathbb{N}$ $$z:\left(\sum_{n:\mathbb{N}} \sum_{m:\mathbb{N}} isPrime(n) \times (m \lt n)\right) \to (T \to T)$$ * a term $$\eta_0: \prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m \lt n) \to (z(n,m)(0) = 0)$$ * a term $$\eta_1: \prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m \lt n) \to (z(n,m)(1) = 1)$$ * a term $$\alpha:\prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m + 1 \lt n) \to \prod_{a:I} ((0 \lt z(n,m+1)(a)) \times (z(n,m)(a) \lt 1)) \to \emptyset$$ ## Examples ## * The initial rational interval coalgebra is the [[unit interval]] on the [[rational numbers]] * The terminal rational interval coalgebra is the [[real unit interval]] ## See also ## * [[dyadic interval coalgebra]] * [[decimal interval coalgebra]] * [[real unit interval]]