9. Appendix: the locus calculus
The development recorded in this book is essentially a theory of bigraphs.
The locus calculus was the inspiration that led to it: a term calculus of
typed string diagrams with a lax modality \bigcirc, suggested by the
grammar of British Sign Language. This appendix holds all the material on
the calculus proper: its syntax and equational theory, soundness in a writer
model, three equations that are deliberately absent and proved not derivable,
and the place layer with its term language. Sources: Fairtlough and Mendler,
Propositional Lax Logic (1997); Moggi, Notions of computation and monads
(1991); Kock, Strong functors and monoidal monads (1972); Fox, Coalgebras and
cartesian categories (1976); Milner, The Space and Motion of Communicating
Agents (2009). Everything else is in Locus/: the relational model
(RelModel.lean), the modality as an arbitrary lax monad (Monad.lean),
conservativity of the place layer by erasure (Conservativity.lean),
reaction (Reaction.lean, Steps.lean) and rendering (Render.lean).