Temporal Type Theory pp 39-45 | Cite as
Translation Invariance
Abstract
As discussed in Sect. 1.2.2, the topos \(\mathsf {Shv}(S_{\mathbb {I\hspace {1.1pt} R}})\) of sheaves on the interval domain is slightly unsatisfactory as a model of behaviors. For example, to serve as a compositional model of dynamical systems, we do not want the set of possible behaviors in some behavior type to depend on any global time. In this chapter, we define a topos \(\mathcal {B}\) of “translation-invariant behavior types” by defining a translation-invariant version of the interval domain and a corresponding site, denoted \(\mathbb {I\hspace {1.1pt} R}_{/\rhd }\) and \(S_{\mathbb {I\hspace {1.1pt} R}/\rhd }\), respectively, and letting \(\mathcal {B}\mathrel{\mathop:}= \mathsf {Shv}(S_{\mathbb {I\hspace {1.1pt} R}/\rhd })\).
References
- [BF00]Bunge, M., Fiore, M.P.: Unique factorisation lifting functors and categories of linearly-controlled processes. Math. Struct. Comput. Sci. 10(2), 137–163 (2000)MathSciNetCrossRefGoogle Scholar
- [Fio00]Fiore, M.P.: Fibred models of processes: discrete, continuous, and hybrid systems. In: IFIP TCS, vol. 1872, pp. 457–473. Springer, Heidelberg (2000)CrossRefGoogle Scholar
- [JJ82]Johnstone, P., Joyal, A.: Continuous categories and exponentiable toposes. J. Pure Appl. Algebra 25(3), 255–296 (1982). ISSN:0022-4049. http://dx.doi.org/10.1016/0022-4049(82)90083-4 MathSciNetCrossRefGoogle Scholar
- [Joh02]Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford Logic Guides, vol. 43, pp. xxii+ 468+ 71. New York: The Clarendon Press/Oxford University Press (2002). ISBN:0-19-853425-6Google Scholar
- [Joh99]Johnstone, P.: A note on discrete Conduch’e fibrations. Theory Appl. Categ. 5(1), 1–11 (1999). ISSN:1201-561XGoogle Scholar
- [Law86]Lawvere F.W.: State categories and response functors. Dedicated to Walter Noll. Preprint (May 1986)Google Scholar
- [SVS16]Spivak, D.I., Vasilakopoulou, C., Schultz, P.: Dynamical Systems and Sheaves (2016). eprint: arXiv:1609.08086Google Scholar