A Monoidal Bifibrational View of Directed Equality Predestries
A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine
Combining insights from the study of type refinement systems and of monoidalclosed 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.This reconstruction leads 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 a simple calculus of existential graphs for predicatelogic, refining an earlier interpretation of existential graphs in terms of boolean hyperdoctrines by brady and trimble.
