Grothendieck Institutions

We extend indexed categories, fibred categories, and Grothendieck constructions to institutions. We show that the 2-category of institutions admits Grothendieck constructions (in a general 2-categorical sense) and that any split fibred institution is equivalent to a Grothendieck institution of an indexed institution. We use Grothendieck institutions as the underlying mathematical structure for the semantics of multi-paradigm (heterogenous) algebraic specification. We recuperate the so-called extra theory morphisms as ordinary theory morphisms in a Grothendieck institution. We investigate the basic mathematical properties of Grothendieck institutions, such as theory colimits, liberality (free constructions), exactness (model amalgamation), and inclusion systems by globalisation from the local level of the indexed institution to the level of the Grothendieck institution.