[Agda] instance functor Sigma

[Dan Licata]

Hi Pierre,

Thanks for taking the time to think about this!

Your answer is basically what I came up with, too, so that's reassuring.
You can think of DepFunctor F as a functor from the category of elements
of F (http://ncatlab.org/nlab/show/category+of+elements) to Set.  I have
some Agda code that plays this story out in a variety of settings (e.g.,
if you take the base category to be isomorphisms, then Pi is a functor
similarly).  Hopefully by the end of the week, I'll have a draft of a
paper about it.

-Dan

On Apr20, Pierre-Evariste Dagand wrote:
> 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 :-)),
>