In the last decades much attention has been devoted in Computer Science to extensions of classical or intuitionistic logic obtained adding additional operators besides the usual logical connectives and quantifiers (separation logic, the various flavours of spatial and temporal logics, bunched implication, etc…).

This gives rise to the problem of how to provide models of such kinds of logics. To this end, several researchers have advocated the use categorical structures like fibrations, in line with the way in which category theory provides a semantics for the usual first order logic.

My main aim is to provide an appropriate notion of model for some of this modal logic. Possibly deducing metatheoretic or proof-theoretic results like completeness.