[Agda] dependent catch all?

[Thorsten Altenkirch]

I was quite pleased to note that I could write

   EQ : SET -> SET -> SET
   EQ set set = one
   EQ zero zero = one
   EQ one one = one
   EQ (Sigma A B) (Sigma A' B') = Sigma (EQ A A') (\ p -> Pi A (\ x ->  
EQ (B x) (B' (coe p x))))
   EQ _ _ = zero

i.e. I dodn't have to list the n^2 off diagonal case. However, my joy  
was short-lived when I tried to implement

   coe : {A A' : SET} -> El (EQ A A') -> El A -> El A'
   coe {set} {set} _ A = A
   coe {zero} {zero} _ ()
   coe {one} {one} _ x = x
   coe {Sigma A B} {Sigma A' B'} (p , q) (a , b) = (coe p a , coe (q  
a) b)
   coe {_} {_} () _

I realize that a way out of this is to implement both components at  
the same time (using a record or a sigma type). Is there another way?   
It seems not completely unreasonable to expect a dependently typed  
programming language to be able to do this sort of thing. One way  
would be to internally expand the cases covered by the catch-all.

Cheers,
Thorsten


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.