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

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

Definition

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

z:( n: m:isPrime(n)×(m<n))(TT)z:\left(\sum_{n:\mathbb{N}} \sum_{m:\mathbb{N}} isPrime(n) \times (m \lt n)\right) \to (T \to T)
  • a term
ηη 0: n: m:isPrime(n)×(m<n)(z(n,m)(0)=0) \eta: \eta_0: \prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m \lt n) \to (z(n,m)(0) = 0)
  • a term
ηη 1: n: m:isPrime(n)×(m<n)(z(n,m)(1)=1) \eta: \eta_1: \prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m \lt n) \to (z(n,m)(1) = 1)
  • a term
α: n: m:isPrime(n)×(m+1<n) a: T I[(0<z m,n(a))+(z m,n(a)<1)]((0<z(n,m+1)(a))×(z(n,m)(a)<1)) \alpha:\prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} isPrime(n) \times (m + 1 \lt n) \to \prod_{a:T} \prod_{a:I} \left[(0 ((0 \lt z_{m,n}(a)) z(n,m+1)(a)) + \times (z_{m,n}(a) (z(n,m)(a) \lt 1)\right] 1)) \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 19:24:05 by Anonymous?. See the history of this page for a list of all contributions to it.