²Note that the source and target operations can equivalently be declared as

     eq source(E ; S) = source(E) .

     eq target(E ; S) = target(S) .