# Homotopy Type Theory rational interval coalgebra > history (Rev #2)

## 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?