[Agda] instance functor Sigma

[Dan Licata]

The standard library contains

    record RawFunctor (F : Set -> Set) : Set1 where
      field
	fmap : forall {a b} -> (a -> b) -> f a -> f b

which is a 'typeclass' meaning that F is a functor.  

You can provide congruence 'instances' for various type constructors; e.g.

times : RawFunctor F -> RawFunctor G -> RawFunctor (\ x -> F x * G x)

by implementing 

fmap : forall {A B} -> RawFunctor F -> RawFunctor G -> (A -> B) -> (F A * G A -> F B * G B)
fmap f1 f2 i (x , y) = fmap f1 i x , fmap f2 i y

I'm working on something now that implements a similar congruence rule
for Sigma:

sigma : RawFunctor F -> Something G -> RawFunctor (\ b -> Sigma (y : F b). G b y)

but I have the feeling that someone may have considered this problem
before.  Does anyone knows of previous work that fills in the Something?

-Dan