Abstract
In Chap. 4, we explained a connection between toposes, type theory, and logic. We also discussed modalities and numeric types in an arbitrary topos. In the current chapter, we will lay out the signature—meaning the atomic types, atomic terms, and axioms—for our specific topos, \(\mathcal {B}\). It turns out that our signature consists of no atomic types, one atomic term, and ten axioms.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Gierz, G., et al.: Continuous Lattices and Domains. Encyclopedia of Mathematics and Its Applications, vol. 93, pp. xxxvi+ 591. Cambridge University Press, Cambridge (2003). ISBN:0-521-80338-1. http://dx.doi.org/10.1017/CBO9780511542725
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
Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol. 7, pp. x+ 293. Reprint of the 1986 original. Cambridge University Press, Cambridge (1988). ISBN:0-521-35653-9
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). Axiomatics. 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_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-00704-1_5
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)