  Motivated by applications in modelling quantum systems using coalgebraic
techniques, we introduce a fibred coalgebraic logic. Our approach extends the
conventional predicate lifting semantics with additional modalities relating
conditions on different fibres. As this fibred setting will typically involve
multiple signature functors, the logic incorporates a calculus of modalities
enabling the construction of new modalities using various composition
operations. We extend the semantics of coalgebraic logic to this setting, and
prove that this extension respects behavioural equivalence.
  We show how properties of the semantics of modalities are preserved under
composition operations, and then apply the calculational aspect of our logic to
produce an expressive set of modalities for reasoning about quantum systems,
building these modalities up from simpler components. We then demonstrate how
these modalities can describe some standard quantum protocols. The novel
features of our logic are shown to allow for a uniform description of unitary
evolution, and support local reasoning such as "Alice's qubit satisfies
condition" as is common when discussing quantum protocols.
