Grothendieck Institutions (abstract)
back to Selected Publications
- 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.