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

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

Definition

A dyadic interval coalgebra is a type $T$ with a strict order $\lt$, terms $0$ , and$1$ , and functions${\mathrm{<span><del\; class="diffmod">\; c</del><ins\; class="diffmod">\; z</ins></span>}}_{0,1}:T\to T$ c_{0,1} z_0:T \to T , functions and$z_{\mathrm{<span><del\; class="diffmod">\; 0</del><ins\; class="diffmod">\; 1</ins></span>}}:T\to T$ z_0:T z_1:T \to T , and identities$z_{\mathrm{<span><del\; class="diffmod">\; 1</del><ins\; class="diffmod">\; 0</ins></span>}}<span><del\; class="diffmod">\; :</del><ins\; class="diffmod">\; (</ins></span>T0<span><del\; class="diffmod">\; \to </del><ins\; class="diffmod">\; )</ins></span>T=0$ z_1:T z_0(0) \to = T 0 , identities$z_{\mathrm{<span><del\; class="diffmod">\; 0</del><ins\; class="diffmod">\; 1</ins></span>}}(0)=0$ z_0(0) z_1(0) = 0, $z_{\mathrm{<span><del\; class="diffmod">\; 1</del><ins\; class="diffmod">\; 0</ins></span>}}(\mathrm{<span><del\; class="diffmod">\; 0</del><ins\; class="diffmod">\; 1</ins></span>})=\mathrm{<span><del\; class="diffmod">\; 0</del><ins\; class="diffmod">\; 1</ins></span>}$ z_1(0) z_0(1) = 0 1, $z_{\mathrm{<span><del\; class="diffmod">\; 0</del><ins\; class="diffmod">\; 1</ins></span>}}(1)=1$ z_0(1) z_1(1) = 1 , inequality$z_{1}0<span><del\; class="diffmod">\; (</del><ins\; class="diffmod">\; <</ins></span>1)=1$ z_1(1) 0 = \lt 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.

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)