Skip to main content

Translation Invariance

  • Chapter
  • First Online:
Temporal Type Theory

Part of the book series: Progress in Computer Science and Applied Logic ((PCS,volume 29))

  • 901 Accesses

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 })\).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 59.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The \(\rhd \) symbol used here (e.g., “\(r\rhd [d,u]\)”) to denote a particular \(\mathbb {R}\)-action on \(\mathbb {I\hspace {1.1pt} R}\) is different from the symbol, used in Chap. 2 (e.g., “Vu”) to denote a basic cover in a posite.

References

  1. Bunge, M., Fiore, M.P.: Unique factorisation lifting functors and categories of linearly-controlled processes. Math. Struct. Comput. Sci. 10(2), 137–163 (2000)

    Article  MathSciNet  Google Scholar 

  2. Fiore, M.P.: Fibred models of processes: discrete, continuous, and hybrid systems. In: IFIP TCS, vol. 1872, pp. 457–473. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  3. 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

    Article  MathSciNet  Google Scholar 

  4. 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-6

    Google Scholar 

  5. Johnstone, P.: A note on discrete Conduch’e fibrations. Theory Appl. Categ. 5(1), 1–11 (1999). ISSN:1201-561X

    Google Scholar 

  6. Lawvere F.W.: State categories and response functors. Dedicated to Walter Noll. Preprint (May 1986)

    Google Scholar 

  7. Spivak, D.I., Vasilakopoulou, C., Schultz, P.: Dynamical Systems and Sheaves (2016). eprint: arXiv:1609.08086

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints and permissions

Copyright information

© 2019 The Author(s)

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Schultz, P., Spivak, D.I. (2019). Translation Invariance. 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_3

Download citation

Publish with us

Policies and ethics