Homotopy Type Theory dyadic interval coalgebra > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

A dyadic interval coalgebra is a type $\mathrm{<span><del\; class="diffmod">\; T</del><ins\; class="diffmod">\; I</ins></span>}$ T I with a strict order $\lt$, terms $0:I$ 0 0:I and $1:I$ 1 1:I, functions $z_0:\mathrm{<span><del\; class="diffmod">\; T</del><ins\; class="diffmod">\; I</ins></span>}\to \mathrm{<span><del\; class="diffmod">\; T</del><ins\; class="diffmod">\; I</ins></span>}$ z_0:T z_0:I \to T I and $z_1:\mathrm{<span><del\; class="diffmod">\; T</del><ins\; class="diffmod">\; I</ins></span>}\to \mathrm{<span><del\; class="diffmod">\; T</del><ins\; class="diffmod">\; I</ins></span>}$ z_1:T z_1:I \to T I, 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. operations, such as thedecimal interval coalgebra.

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)