Institutional 2-cells and grothendieck institutions

Till Mossakowski

pp. 124-149

in: Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer (eds), Algebra, meaning, and computation, Berlin, Springer, 2006

Abstract

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 institution semi-morphisms.