[Agda] instance functor Sigma

[Pierre-Evariste Dagand]

Hi Dan,

> 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)

So, I just had a look at your problem, because it has a strong smell
of Container (http://www.citeulike.org/user/pedagand/tag/container-theory).
While I could not link it with the containers I'm working with
nowadays, a colleague and I got to the following Something:

record DepFunctor (F : Set -> Set)
                            (mapF : RawFunctor F)
                            (G : (B : Set) -> F B -> Set) : Set1 where
     field
       dmap : {a b : Set} -> (f : a -> b) ->
                  {x : F a} -> G a x -> G b (fmap mapF f x)

That captures the "dependent functor" you need on the right of the
Sigma. Hence, we obtain this definition for sigma:

sigma : {F : Set -> Set}{G : (B : Set) -> F B -> Set} ->
           (mapF : RawFunctor F) -> DepFunctor F mapF G ->
           RawFunctor (\x -> Sigma (F x) (G x))
sigma F G = record { fmap = fmapSigma F G }
  where fmapSigma : forall {A B} ->
                    {F : Set -> Set}
                    {G : (B : Set) -> F B -> Set} ->
                    (mapF : RawFunctor F) ->
                    DepFunctor F mapF G ->
                    (A -> B) ->
                    Sigma (F A) (G A) -> Sigma (F B) (G B)
           fmapSigma f1 f2 i = map (fmap f1 i) (dmap f2 i)

Where 'map' is defined in the standard library (Data.Product).

According to my colleague, DepFunctor ought to be generalizable, he
even used the F. word (fibration). When he starts being rude like
that, I've to close emacs before he writes commuting diagrams all over
the place.


Hope this help (I doubt it does, tho :-)),

-- 
Pierre