Abstract
In Sect. 4.3 we introduced ten Dedekind j-numeric types for an arbitrary modality j. Namely, we have the j-local lower and upper reals, improper and proper intervals, and real numbers, as well as their unbounded counterparts. They are denoted
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In fact, the type C is dependent on q 1; see Sect. 4.1.4.
- 2.
We are suppressing the time context for readability. To be explicit, this example takes place in the context of a time interval \((d_t,u_t)\in [\hspace{-0.17em}[ \mathtt {Time} ]\hspace{-0.17em}] (\ell )\), where d t ≤ d ≤ u ≤ u t.
- 3.
Technically, the semantics of the term-in-context
is a sheaf homomorphism 
, and we are denoting the image of (g, r) under the â„“-component of that map.
is a sheaf homomorphism 
, and we are denoting the image of (g, r) under the â„“-component of that map.Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2019 The Author(s)
About this chapter
Cite this chapter
Schultz, P., Spivak, D.I. (2019). Local Numeric Types and Derivatives. In: Temporal Type Theory. Progress in Computer Science and Applied Logic, vol 29. Birkhäuser, Cham. https://doi.org/10.1007/978-3-030-00704-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-00704-1_7
Published:
Publisher Name: Birkhäuser, Cham
Print ISBN: 978-3-030-00703-4
Online ISBN: 978-3-030-00704-1
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)