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
- 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?