×

zbMATH — the first resource for mathematics

Grothendieck institutions. (English) Zbl 1008.68078
Summary: 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 (heterogeneous) 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.

MSC:
68Q65 Abstract data types; algebraic specification
18C10 Theories (e.g., algebraic theories), structure, and semantics
03G30 Categorical logic, topoi
08A70 Applications of universal algebra in computer science
Software:
CafeOBJ
PDF BibTeX XML Cite
Full Text: DOI