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

Definition

A decimal interval coalgebra is a type II with a strict order <\lt, terms 0:I0:I, 1:I1:I, a term p:0<1p: 0 \lt 1

z:( m:(m<10))(II)z:\left(\sum_{m:\mathbb{N}} (m \lt 10)\right) \to (I \to I)
  • a term
η 0: m:(m<10)(z(m)(0)=0)\eta_0: \prod_{m:\mathbb{N}} (m \lt 10) \to (z(m)(0) = 0)
  • a term
η 1: m:(m<10)(z(m)(1)=1)\eta_1: \prod_{m:\mathbb{N}} (m \lt 10) \to (z(m)(1) = 1)
  • a term
α: m:(m+1<10) a:I((0<z(m+1)(a))×(z(m)(a)<1))\alpha:\prod_{m:\mathbb{N}} (m + 1 \lt 10) \to \prod_{a:I} ((0 \lt z(m+1)(a)) \times (z(m)(a) \lt 1)) \to \emptyset

A decimal interval coalgebra homomorphism between two decimal interval coalgebras II and JJ is a function f:IJf:I \to J with terms p 0:f(0)=0p_0: f(0) = 0, p 1:f(1)=1p_1: f(1) = 1 and

p z: a:I m:(m<10)(f(z(m)(i))=z(m)(f(i))p_z: \prod_{a:I} \prod_{m:\mathbb{N}} (m \lt 10) \to (f(z(m)(i)) = z(m)(f(i))

we define the type of decimal interval coalgebra homomorphisms between decimal interval coalgebras II and JJ to be

IntCoAlgHom 10(I,J) f:IJ(f(0)=0)×(f(1)=1)× a:I m:(m<10)(f(z(m)(i))=z(m)(f(i))IntCoAlgHom_{10}(I, J) \coloneqq \sum_{f:I \to J} (f(0) = 0) \times (f(1) = 1) \times \prod_{a:I} \prod_{m:\mathbb{N}} (m \lt 10) \to (f(z(m)(i)) = z(m)(f(i))

A decimal inter coalgebra II is initial if the type of decimal interval colagebras from II to any decimal interval coalgebra JJ in a universe 𝒰\mathcal{U} is contractible:

isInitial(I) J:𝒰isContr(IntCoAlgHom 10(I,J))isInitial(I) \coloneqq \prod_{J:\mathcal{U}} isContr(IntCoAlgHom_{10}(I, J))

A decimal inter coalgebra 𝕀\mathbb{I} is terminal if the type of decimal interval colagebras from any decimal interval coalgebra JJ in a universe 𝒰\mathcal{U} to 𝕀\mathbb{I} is contractible:

isTerminal(𝕀) J:𝒰isIntCoAlg(J)×isContr(IntCoAlgHom 10(J,𝕀))isTerminal(\mathbb{I}) \coloneqq \prod_{J:\mathcal{U}} isIntCoAlg(J) \times isContr(IntCoAlgHom_{10}(J, \mathbb{I}))

Examples

  • The initial decimal interval coalgebra is the unit interval on the decimal numbers

  • The terminal decimal interval coalgebra is the real unit interval?

See also

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