## Definition ## A **decimal interval coalgebra** is a type $I$ with a [[strict order]] $\lt$, terms $0:I$, $1:I$, a term $p: 0 \lt 1$ * a [[partial function]] from $\mathbb{N}$ $$z:\left(\sum_{m:\mathbb{N}} (m \lt 10)\right) \to (I \to I)$$ * a term $$\eta_0: \prod_{m:\mathbb{N}} (m \lt 10) \to (z(m)(0) = 0)$$ * a term $$\eta_1: \prod_{m:\mathbb{N}} (m \lt 10) \to (z(m)(1) = 1)$$ * a term $$\alpha:\prod_{m:\mathbb{N}} (m + 1 \lt 10) \to \prod_{a:I} ((0 \lt z(m+1)(a)) \times (z(m)(a) \lt 1)) \to \emptyset$$ A ***decimal interval coalgebra homomorphism*** between two decimal interval coalgebras $I$ and $J$ is a function $f:I \to J$ with terms $p_0: f(0) = 0$, $p_1: f(1) = 1$ and $$p_z: \prod_{a:I} \prod_{m:\mathbb{N}} (m \lt 10) \to (f(z(m)(i)) = z(m)(f(i))$$ we define the type of decimal interval coalgebra homomorphisms between decimal interval coalgebras $I$ and $J$ to be $$IntCoAlgHom_{10}(I, J) \coloneqq \sum_{f:I \to J} (f(0) = 0) \times (f(1) = 1) \times \prod_{a:I} \prod_{m:\mathbb{N}} (m \lt 10) \to (f(z(m)(i)) = z(m)(f(i))$$ A decimal inter coalgebra $I$ is **initial** if the type of decimal interval colagebras from $I$ to any decimal interval coalgebra $J$ in a universe $\mathcal{U}$ is contractible: $$isInitial(I) \coloneqq \prod_{J:\mathcal{U}} isContr(IntCoAlgHom_{10}(I, J))$$ A decimal inter coalgebra $\mathbb{I}$ is **terminal** if the type of decimal interval colagebras from any decimal interval coalgebra $J$ in a universe $\mathcal{U}$ to $\mathbb{I}$ is contractible: $$isTerminal(\mathbb{I}) \coloneqq \prod_{J:\mathcal{U}} isIntCoAlg(J) \times isContr(IntCoAlgHom_{10}(J, \mathbb{I}))$$ ## Examples ## * The initial decimal interval coalgebra is the [[unit interval]] on the [[decimal numbers]] * The terminal decimal interval coalgebra is the [[real unit interval]] ## See also ## * [[dyadic interval coalgebra]] * [[rational interval coalgebra]] * [[real unit interval]]