Hostname: page-component-cd9895bd7-lnqnp Total loading time: 0 Render date: 2024-12-22T23:01:34.386Z Has data issue: false hasContentIssue false
  • English
  • Français

Doctrines, modalities and comonads

Published online by Cambridge University Press:  14 September 2021

Francesco Dagnino  and
Giuseppe Rosolini Open the ORCID record for Giuseppe Rosolini [Opens in a new window]
Francesco Dagnino
Affiliation:
DIBRIS, Università di Genova
Giuseppe Rosolini*
Affiliation:
DIMA, Università di Genova
*
*Corresponding author. Email: [email protected]
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Doctrines are categorical structures very apt to study logics of different nature within a unified environment: the 2-category Dtn of doctrines. Modal interior operators are characterised as particular adjoints in the 2-category Dtn. We show that they can be constructed from comonads in Dtn as well as from adjunctions in it, and we compare the two constructions. Finally we show the amount of information lost in the passage from a comonad, or from an adjunction, to the modal interior operator. The basis for the present work is provided by some seminal work of John Power.

Keywords

Modal operatordoctrineadjunctioncomonadtemporal logicslinear logic
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 31 , Special Issue 7: The Power Festschrift , August 2021 , pp. 769 - 798
Check for updates
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re- use, distribution and reproduction, provided the or article is properly cited.
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Aczel, P., Adámek, J., Milius, S. and Velebil, J. (2003). Infinite trees and completely iterative theories: A coalgebraic view. Theoretical Computer Science 300 (1–3) 1–45.CrossRefGoogle Scholar
Awodey, S. and Birkedal, L. (2003). Elementary axioms for local maps of toposes. Journal of Pure and Applied Algebra 177 (3) 215–230.CrossRefGoogle Scholar
Awodey, S., Birkedal, L. and Scott, D. S. (2002). Local realizability toposes and a modal logic for computability. Mathematical Structures in Computer Science 12 (3) 319–334.CrossRefGoogle Scholar
Awodey, S., Kishida, K. and Kotzsch, H.-C. (2014). Topos semantics for higher-order modal logic. Logique & Analyse (N.S.) 226 591–636.Google Scholar
Baier, C. and Katoen, J. (2008). Principles of Model Checking. MIT Press.Google Scholar
Benton, P. N. (1994). A mixed linear and non-linear logic: Proofs, terms and models. In: Pacholski, L. and Tiuryn, J. (eds.) Computer Science Logic, 8th International Workshop, CSL 1994, vol. 933. Lecture Notes in Computer Science. Springer, 121–135.Google Scholar
Betti, R. and Power, A. J. (1988). On local adjointness of distributive bicategories. Bollettino della Unione Matematica Italiana 2 (4) 931–947.Google Scholar
Blackwell, R., Kelly, G. M. and Power, A. J. (1989). Two-dimensional monad theory. J. Pure Appl. Algebra 59 (1) 1–41.CrossRefGoogle Scholar
Braüner, T. and Ghilardi, S. (2007). First-order modal logic. In: Blackburn, P., van Benthem, J. F. A. K. and Wolter, F. (eds.) Handbook of Modal Logic., vol. 3. Studies in Logic and Practical Reasoning. North Holland Publishing Company, 549–620.CrossRefGoogle Scholar
Courcelle, B. (1983). Fundamental properties of infinite trees. Theoretical Computer Science 25, 95–169.CrossRefGoogle Scholar
Emmenegger, J., Pasquali, F., and Rosolini, G. 2020. Elementary doctrines as coalgebras. J. Pure Appl. Algebra 224 (12) 106445, 16.CrossRefGoogle Scholar
Esakia, L. (2004). Intuitionistic logic and modality via topology. Annals of Pure and Applied Logic 127 (1–3) 155–170.CrossRefGoogle Scholar
Ghani, N., Lüth, C., Marchi, F. D. and Power, J. (2001). Algebras, coalgebras, monads and comonads. Electronic Notes in Theoretical Computer Science 44 (1) 128–145.CrossRefGoogle Scholar
Ghilardi, S. and Meloni, G. C. (1988). Modal and tense predicate logic: models in presheaves and categorical conceptualization. In: Categorical Algebra and Its Applications (Louvain-La-Neuve, 1987), vol. 1348. Lecture Notes in Math. Springer, 130–142.CrossRefGoogle Scholar
Hermida, C. (1994). On fibred adjunctions and completeness for fibred categories. In: Recent Trends in Data Type Specification (Caldes de Malavella, 1992), vol. 785. Lecture Notes in Computer Science. Springer, 235–251.CrossRefGoogle Scholar
Hermida, C. (1999). Some properties of fib as a fibred 2-category. Journal of Pure and Applied Algebra 134 (1) 83–109.CrossRefGoogle Scholar
Jacobs, B. (1999). Categorical Logic and Type Theory. North Holland Publishing Company.Google Scholar
Johnstone, P. T. (2002). Sketches of An Elephant: A Topos Theory Compendium, Vol. 1, vol. 43. Oxford Logic Guides. The Clarendon Press, Oxford University Press.Google Scholar
Lawvere, F. W. (1969). Adjointness in foundations. Dialectica 23 281–296. also available as Reprints in Theory and Applications of Categories 16 (2006) 1–16.Google Scholar
Lawvere, F. W. (1970). Equality in hyperdoctrines and comprehension schema as an adjoint functor. In Heller, A. (ed.) Proc. New York Symposium on Application of Categorical Algebra. Amer. Math. Soc, 1–14.CrossRefGoogle Scholar
Mac Lane, S. and Moerdijk, I. (1992). Sheaves in Geometry and Logic a First Introduction to Topos Theory. Springer.Google Scholar
Maietti, M. E. and Rosolini, G. (2013a). Elementary quotient completion. Theory and Applications of Categories 27 445–463.Google Scholar
Maietti, M. E. and Rosolini, G. (2013b). Quotient completion for the foundation of constructive mathematics. Logica Universalis 7 (3) 371–402.CrossRefGoogle Scholar
Maietti, M. E. and Rosolini, G. (2015). Unifying exact completions. Applied Categorical Structures 23 43–52.CrossRefGoogle Scholar
Moeller, J. and Vasilakopoulou, C. (2020). Monoidal Grothendieck Construction. Theory and Applications of Categories 35 (31) 1159–1207.Google Scholar
Power, A. J. and Watanabe, H. (2002). Combining a monad and a comonad. Theoretical Computer Science 280 (1–2) 137–162.CrossRefGoogle Scholar
Reyes, G. E. (1991). A topos-theoretic approach to reference and modality. Notre Dame Journal of Formal Logic 32 (3) 359–391.CrossRefGoogle Scholar
Rosenthal, K. I. (1990). Quantales and Their Applications, vol. 234. Pitman Research Notes in Mathematics Series. Longman Scientific & Technical; copublished in the United States with John Wiley & Sons, Inc.Google Scholar
Street, R. (1972). The Formal Theory of Monads. Journal of Pure and Applied Algebra 2 (2) 149–168.CrossRefGoogle Scholar
Streicher, T. (1991). Semantics of Type Theory. Progress in Theoretical Computer Science. Birkhäuser Boston, Inc. Correctness, completeness and independence results, With a foreword by Martin Wirsing.CrossRefGoogle Scholar