A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine

DOI10.1145/2933575.2934525MaRDI QIDQ4635915zbMATH OpenOpenAlexFDO

Authors Paul-André Melliès, Noam Zeilberger

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1601.06098

zbMATH Keywords

Lawvere's presheaf hyperdoctrinelinear logicmonoidal closed bifibrationsmonoidal closed chiralitiestype refinement systems

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical logic, topoi (03G30) Fibered categories (18D30) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20)

Abstract: Combining insights from the study of type refinement systems and of monoidal closed chiralities, we show how to reconstruct Lawvere's hyperdoctrine of presheaves using a full and faithful embedding into a monoidal closed bifibration living now over the compact closed category of small categories and distributors. Besides revealing dualities which are not immediately apparent in the traditional presentation of the presheaf hyperdoctrine, this reconstruction leads us to an axiomatic treatment of directed equality predicates (modelled by hom presheaves), realizing a vision initially set out by Lawvere (1970). It also leads to a simple calculus of string diagrams (representing presheaves) that is highly reminiscent of C. S. Peirce's existential graphs for predicate logic, refining an earlier interpretation of existential graphs in terms of Boolean hyperdoctrines by Brady and Trimble. Finally, we illustrate how this work extends to a bifibrational setting a number of fundamental ideas of linear logic.

Recommendations

• An Isbell duality theorem for type refinement systems
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Full Lambek Hyperdoctrine: Categorical Semantics for First-Order Substructural Logics
• scientific article; zbMATH DE number 4002342
• Fibred algebraic semantics for a variety of non-classical first-order logics and topological logical translation

Cited in

(13)

• Bifibrations of polycategories and classical linear logic
• An Isbell duality theorem for type refinement systems
• Proof nets, coends and the Yoneda isomorphism
• Graphical Conjunctive Queries.
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• A fibrational tale of operational logical relations: pure, effectful and differential
• A functorial excursion between algebraic geometry and linear logic
• Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem
• The categorical contours of the Chomsky-Schützenberger representation theorem
• Diagrammatic algebra of first order logic
• When Lawvere meets Peirce: an equational presentation of Boolean hyperdoctrines
• The calculus of neo-Peircean relations
• On Boolean hyperdoctrines and peircean bicategories

This page was built for publication: A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635915)