Homotopy Type Theory rational interval coalgebra > history (Rev #1)

Definition

A rational interval coalgebra is a type $T$ with a strict order $\lt$ , terms $0$ , $1$ , a term $p: 0 \lt 1$

a function

z:\left(\sum_{n:\mathbb{N}} \sum_{m:\mathbb{N}} isPrime(n) \times (m \lt n)\right) \to (T \to T)

a term

\eta: \prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m \lt n) \to (z(n,m)(0) = 0)

a term

\eta: \prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m \lt n) \to (z(n,m)(1) = 1)

a term

\alpha:\prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m \lt n) \to \prod_{a:T} \left[(0 \lt z_{m,n}(a)) + (z_{m,n}(a) \lt 1)\right] \to \emptyset

Examples

The initial rational interval coalgebra is the unit interval on the rational numbers
The terminal rational interval coalgebra is the real unit interval?

See also

Revision on April 22, 2022 at 18:15:05 by Anonymous?. See the history of this page for a list of all contributions to it.