Homotopy Type Theory rational interval coalgebra > history (changes)

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

Definition

< rational interval coalgebra

A

rational interval coalgebra is a type II with a strict order <\lt, terms 0:0:, 1:I1: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_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_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:I((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:I} ((0 \lt z(n,m+1)(a)) \times (z(n,m)(a) \lt 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

Last revised on June 10, 2022 at 03:29:38. See the history of this page for a list of all contributions to it.