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

Definition

A dyadic interval coalgebra is a type $T$ with a strict order $\lt$, terms $0$ and $1$, functions $z_0:T \to T$ and $z_1:T \to T$, identities $z_0(0) = 0$, $z_1(0) = 0$, $z_0(1) = 1$, $z_1(1) = 1$, inequality $0 \lt 1$, and terms

This is called simply an interval coalgebra by Peter Freyd, however there exist similarly defined interval coalgebras with $n+1$ terms and $n$ zooming operations.

Examples

• The initial dyadic interval coalgebra is the unit interval on the dyadic rational numbers?

• The terminal dyadic interval coalgebra is the real unit interval?

See also

• rational interval coalgebra
• decimal interval coalgebra
• real unit interval?

References

• Peter Freyd, Algebraic real analysis, Theory and Applications of Categories, Vol. 20, 2008, No. 10, pp 215-306 (tac:20-10)