# Rules for consistency with mutual inductive families?

I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other:

Vec : (a : Type) -> (n : Nat) -> Type0
Rel : (a : Type) -> a -> a -> Type

data Vec : (a : Type) -> (n : Nat) -> Type0 where
Nil : Rel Nat n 0 -> Vec a n
Cons : a -> Vec a n' -> Rel Nat (S n') n -> Vec a n

data Rel : (a : Type) -> a -> a -> Type0 where
RRefl : (a : Type) -> (x : a) -> Rel a x x
RSucc : (m n : Nat) -> Rel Nat m n -> Rel Nat (S m) (S n)
RCons : (e : Type) -> (m n: Nat) -> (h1 h2 : e) -> (t1 t2 : Vec e m) ->
Rel e h1 h2 -> Rel (Vec e m) t1 t2 ->
(rn : Rel Nat (S m) n) ->
Rel (Vec e n) (Cons h1 t1 rn) (Cons h2 t2 rn)


Right now, both Agda and Idris reject this definition, since Rel refers not only to Vec, but to Cons, a constructor of Vec.

I'm wondering:

• Is this restriction an implementation detail, or is it critical for ensuring consistency of a type theory? i.e. if we allow this kind of mutual reference, can we prove False?
• Are there standard techniques to get around this? Possibly using induction-induction or induction-recursion?

One idea I had is to define a sort of PreVec that takes a parameter of type (rel : Nat -> Nat -> Type). But will this cause problems with predicativity?

• What is the motivation for this definition? I fail to see any use case. Rel seems to be a type-casing version of propositional equality which adds redundant equality proofs. – András Kovács Nov 19 at 11:14
• @AndrásKovács This is just meant to be a minimal example, what I have is different, and has additional cases that make it more than propositional equality – jmite Nov 19 at 16:13
• could you add the example which you actually want to use? Just from this, I cannot comment on how to meaningfully reformulate. – András Kovács Nov 19 at 16:34