## Definition ## A **rational interval coalgebra** is a type $T$ with a [[strict order]] $\lt$, terms $0$, $1$, a term $p: 0 \lt 1$ * a function $$z:\left(\sum_{n:\mathbb{N}} \sum_{m:\mathbb{N}} isPrime(n) \times (m \lt n)\right) \to (T \to T)$$ * a term $$\eta: \prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m \lt n) \to (z(n,m)(0) = 0)$$ * a term $$\eta: \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 \lt n) \to \prod_{a:T} \left[(0 \lt z_{m,n}(a)) + (z_{m,n}(a) \lt 1)\right] \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]]