Many indexed inductive families can be "equivalently" defined by recursion over their indices. For instance, the type family of vectors:

data Vec (A : Set) : ℕ → Set where
  nil : Vec A zero
  cons : {n : ℕ) → A → Vec A n → Vec A (suc n)

can equivalently be defined recursively to consist of right-associated product types:

Vec : (A : Set) → ℕ → Set
Vec A zero = ⊤
Vec A (suc n) = A × Vec A n

Similarly, the inequality predicates on natural numbers, like:

data _≤_ : ℕ → ℕ → Set where
  zero≤ : (n : ℕ) → zero ≤ n
  suc≤suc : (m n : ℕ) → (m ≤ n) → (suc m ≤ suc n)

can also be defined recursively on both arguments:

_≤_ : ℕ → ℕ → Set
zero ≤ _ = ⊤
suc m ≤ zero = ⊥
suc m ≤ suc n = m ≤ n

Of course, this is only possible when the indices of the indexed inductive family are themselves inductive types, and the indices of each constructor are constructors of the index. (Which, perhaps coincidentally, is also the case in which indexed inductive families work best -- no "green slime".)

In a situation where both definitions are possible, what are the advantages and disadvantages of the two choices? Why should we choose one over the other?

Many indexed inductive families can be "equivalently" defined by recursion over their indices. For instance, the type family of vectors:

data Vec (A : Set) : ℕ → Set where
  nil : Vec A zero
  cons : {n : ℕ) → A → Vec A n → Vec A (suc n)

can equivalently be defined recursively to consist of right-associated product types:

Vec : (A : Set) → ℕ → Set
Vec A zero = ⊤
Vec A (suc n) = A × Vec A n

Similarly, the inequality predicates on natural numbers, like:

data _≤_ : ℕ → ℕ → Set where
  zero≤ : (n : ℕ) → zero ≤ n
  suc≤suc : (m n : ℕ) → (m ≤ n) → (suc m ≤ suc n)

can also be defined recursively on both arguments:

_≤_ : ℕ → ℕ → Set
zero ≤ _ = ⊤
suc m ≤ zero = ⊥
suc m ≤ suc n = m ≤ n

Of course, this is only possible when the types of indices of the indexed inductive family are themselves inductive types, and the indices of each constructor are constructors of the types of indices. (Which, perhaps coincidentally, is also the case in which indexed inductive families work best -- no "green slime".)

In a situation where both definitions are possible, what are the advantages and disadvantages of the two choices? Why should we choose one over the other?