Comments on A Neighborhood of Infinity: Dinatural Transformations and Coends

I think what you call a difunctor is what everyone...

2011-06-27T16:17:04.865-07:00

I think what you call a difunctor is what everyone else calls a profunctor.

Also, this concept of a morphism that factors anot...

2009-04-17T15:26:00.000-07:00

Also, this concept of a morphism that factors another class of morphisms uniquely reminds me of fibred categories: is i :: s a a -> Y cartesian with respect to some fibration?

You say: "if s is a dinatural then if there i...

2009-04-17T14:59:00.000-07:00

You say: "if s is a dinatural then if there is a single Y, and function i :: s a a -> Y, such that every function f :: s a a -> X, for any X, can be factored as f = h . i, then Y is said to be the coend of s."

I'm not sure, but I think you mean: "if s is a difunctor then if there is a single Y, and function i :: s a a -> Y, such that every dinatural function f :: s a a -> X, for any X, can be factored as f = h . i, then Y is said to be the coend of s."

I'm pretty sure, but have not proven, that fre...

2009-03-14T11:27:00.000-07:00

I'm pretty sure, but have not proven, that free theorems are equivalent to the (general) dinaturality conditions (plus some general properties of dinatural transformations.) I believe this has always been the case for any examples that correspond to natural transformations and for the examples that wouldn't correspond to natural transformations, the free theorems have at least implied the dinaturality condition.

Another interesting example of a dinatural transformation is (a -> a) -> a.

uncurry bind is also dinatural.

Your counit...

2009-03-10T13:50:00.000-07:00

uncurry bind is also dinatural.

Your counit isn't.

The signature of a dinatural transformation (the kind we're talking about anyway) is

f :: forall a . (s a a -> X)

for some X.

I've put in parentheses to make the quantification clear. f is actually a family of functions, one for each a, mapping form s a a to X, as per the textbook definition of dinatural.

Your counit is of the form

counit :: A -> B

where A = forall a.(a->x,a)
(forgetting about the quantification over x for now). The quantification over a is contained completely in the domain.

In other words counit isn't a family of functions, it's a single function from an existential type. So it's a completely different kind of entity.

If uncurry cobind is dinatural, why wouldn't u...

2009-03-10T12:15:00.000-07:00

If uncurry cobind is dinatural, why wouldn't uncurry bind also be so?

uncurry bind :: (a -> m b, m a) -> m b

As for the context comonad, I'm thinking of this:

counit :: (forall a. (a->x,a)) -> x

which is basically your

iso :: Coend (Ex1 t) -> t.

By definition, the counit is natural. 'cobind&...

2009-03-10T10:22:00.000-07:00

By definition, the counit is natural. 'cobind', or whatever you want to call it, is (probably) dinatural though.

uncurry cobind :: (w a -> b,w a) -> w b

I don't know how to prove uniformly that everything of this type is dinatural, but the free theorem for every example I've tried says it is.

Is there a result of the form: every counit of a c...

2009-03-10T10:12:00.000-07:00

Is there a result of the form: every counit of a comonad is dinatural?

I'm thinking of generalizations of the counit of the context comonad.