Grothendieck institutions generalize the flattening Grothendieck construction from (indexed) categories, (see Sect. 2.5), to (indexed) institutions. Regarded from a fibration theoretic angle, Grothendieck institutions are just institutions for which their category of signatures is fibred. For example, the actual institutions with many-sorted signatures appear naturally as fibred institutions determined by the fibrations given by the functor mapping each signature to its set of sort symbols. In this sense, fibred institutions can be regarded as the reflection of many-sortedness at the level of abstract institutions.
KeywordsNatural Transformation Satisfaction Condition Interpolation Property Inclusion System Model Amalgamation
Unable to display preview. Download preview PDF.