nLab applications of double category theory

A list of works and resources about applications of double category theory.

See there for introductory material.

Theory

Equipments

• David Jaz Myers, String diagrams for double categories and (virtual) equipments, (arXiv), 2016
• Mike Shulman, Equipments, (n-Café), 2009
• Mike Shulman, Framed bicategories and monoidal fibrations, (arXiv), 2009
• Max New, Dan Licata, A Formal Logic for Formal Category Theory, (arXiv), 2022

Grothendieck constructions

• Evan Patterson, Grothendieck construction for double categories, (Topos Institute), 2022
• Cruttwell, Lambert, Pronk, Szyld, Double Fibrations, (arXiv), 2022

Applications

Lenses & optics

• Bryce Clarke, The double category of lenses, (online), 2022
• Capucci, Seeing double through dependent optics, (arXiv), 2022
• Guillaume Boisseau, Chad Nester, Mario Roman, Cornering optics,(arXiv), 2022

Open systems theory

• Jared Culbertson, Paul Gustafson, Daniel E. Koditschek, Peter F. Stiller, Formal composition of hybrid systems, (arXiv)
• Kenny Courser, Open systems: a double categorical perspective, (arXiv), 2020 See also structured cospans and decorated cospans
• Chad Nester, Situated Transition Systems, (arXiv), 2021
• David Jaz Myers, Categorical systems theory, (online), 2021
• Evan Patterson, Decorated cospans via the double Grothendieck construction, (Topos Institute), 2022
• Evan Patterson, Structured cospans as a cocartesian equipment, (Topos Institute), 2023
• John Baez, Kenny Courser, Christina Vasilakopoulou, Structured versus Decorated Cospans, (Compositionality), 2022
• Chad Nester, Concurrent Process Histories and Resource Transducers, (arXiv), 2022

Theory of programming languagues

• Pierre-Evariste Dagand, Conor McBride, A Categorical Treatment of Ornaments, (acm), 2013
• Max New, Dan Licata, Call-by-name Gradual Type Theory, (arXiv), 2018
• Max New, Dan Licata, A Formal Logic for Formal Category Theory, (arXiv), 2022
• Clovis Eberhart, Tom Hirschowitz, Fibred Pseudo Double Categories for Game Semantics, TAC 34(19), 2019. Beware, “fibred” is use there to mean that the codomain functor is a fibration.