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

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

Definition

< dyadic interval coalgebra

A

dyadic interval coalgebra is a type II with a strict order <\lt, terms 0:I0:I and 1:I1:I, functions z 0:IIz_0:I \to I and z 1:IIz_1:I \to I, identities z 0(0)=0z_0(0) = 0, z 1(0)=0z_1(0) = 0, z 0(1)=1z_0(1) = 1, z 1(1)=1z_1(1) = 1, inequality 0<10 \lt 1, and terms

α: a:I((0<z 0(a))×(z 1(a)<1))\alpha:\prod_{a:I} ((0 \lt z_0(a)) \times (z_1(a) \lt 1)) \to \emptyset

This is called simply an interval coalgebra by Peter Freyd, however there exist similarly defined interval coalgebras with n+1n+1 terms and nn zooming operations, such as the decimal 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

References

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

Revision on June 10, 2022 at 03:30:48 by Anonymous?. See the history of this page for a list of all contributions to it.