Institutional 2-cells and Grothendieck institutions
T. Mossakowski. Algebra, Meaning and Computation. Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, volume 4060 of Lecture Notes in Computer Science, page 124-149. Springer; Berlin; http://www.springer.de, (2006)
We propose to use Grothendieck institutions based on
2-categorical diagrams as a basis for heterogeneous
specification. We prove a number of results about
colimits and (some weak variants of) exactness.
This framework can also be used for obtaining proof
systems for heterogeneous theories involving