[Agda] mutual recursion

[Ondrej Rypacek]

Hi All,

Below is a simple example of an inductive recursive definition, which
fails to compile. Does anyone on the list have an idea why? I must be
missing something .

I define a datatype, W, (of arrows) and a pair of function on it , src, tgt,
The idea is that I can compose b . a  in W provided that src b == tgt a.
Src of (b . a) is src of a ; tgt of (b . a) is tgt b (just as in a category).
In addition i define \alpha for any three composable z y x, where the
src of (alpha z y x), to be thought of as (z . y) . x => x . (y . x)
is (z . y) . x, and the tgt of (alpha z y x)  is z . (y . x).

In order to define this I must form the composites (z . y) . x and z .
(y . x) , for which I need to know that src (z . y) = y (but that is
by definition) and that tgt (y . x) = y , also by definition.
But this doesn't seem to work in Agda.

Does anyone have an idea why can't I use k : src y == tgt x for (src
(comp z y h) = tgt x) ?

Thanks in advance for any suggestions.
Ondrej

---

module Xx where

open import Relation.Binary.PropositionalEquality

module W where

  mutual
    data W : Set where
      comp : (β α : W) → (src β) ≡ (tgt α) → W
      alpha : (z y x : W) → src z ≡ tgt y → src y ≡ tgt x → W

    tgt : W → W
    tgt (comp β α y) = tgt β
    tgt (alpha z y x h k) = comp (comp z y h) x {!!}

    src : W → W
    src (comp β α y) = src α
    src (alpha z y x h k) = comp z (comp y x k) h


---