Grothendieck Institutions (abstract)

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.

---