[Agda] dependent mutually inductive types

[Michael Shulman]

Hi,

In Agda, it appears to be possible to mutually-inductively define two
types A and B, such that B is dependent on A:

mutual
  data A : Set where
    ...

  data B : A -> Set where
    ...

Is there a mathematical theory of models or consistency for such
dependent mutually inductive families?

Thanks,
Mike