tag:blogger.com,1999:blog-11295132.post6987168894740966011..comments2014-04-16T10:57:46.206-07:00Comments on A Neighborhood of Infinity: Dinatural Transformations and CoendsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-11295132.post-58638751161683061552011-06-27T16:17:04.865-07:002011-06-27T16:17:04.865-07:00I think what you call a difunctor is what everyone...I think what you call a difunctor is what everyone else calls a profunctor.mikehttp://www.blogger.com/profile/03408641732412584050noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-77040892756115832142009-04-17T15:26:00.000-07:002009-04-17T15:26:00.000-07:00Also, this concept of a morphism that factors anot...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?Peter Berryhttp://www.blogger.com/profile/08770230331776974807noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-15158690413819683072009-04-17T14:59:00.000-07:002009-04-17T14:59:00.000-07:00You say: "if s is a dinatural then if there i...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."<br /><br />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."Peter Berryhttp://www.blogger.com/profile/08770230331776974807noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-16061663024613199212009-03-14T11:27:00.000-07:002009-03-14T11:27:00.000-07:00I'm pretty sure, but have not proven, that fre...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.<BR/><BR/>Another interesting example of a dinatural transformation is (a -> a) -> a.Derek Elkinsnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-45343833845135930292009-03-10T13:50:00.000-07:002009-03-10T13:50:00.000-07:00uncurry bind is also dinatural.Your counit isn'...uncurry bind is also dinatural.<BR/><BR/>Your counit isn't.<BR/><BR/>The signature of a dinatural transformation (the kind we're talking about anyway) is<BR/><BR/>f :: forall a . (s a a -> X)<BR/><BR/>for some X.<BR/><BR/>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.<BR/><BR/>Your counit is of the form<BR/><BR/>counit :: A -> B<BR/><BR/>where A = forall a.(a->x,a)<BR/>(forgetting about the quantification over x for now). The quantification over a is contained completely in the domain.<BR/><BR/>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.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-17758494995513749212009-03-10T12:15:00.000-07:002009-03-10T12:15:00.000-07:00If uncurry cobind is dinatural, why wouldn't u...If uncurry cobind is dinatural, why wouldn't uncurry bind also be so?<BR/><BR/>uncurry bind :: (a -> m b, m a) -> m b<BR/><BR/>As for the context comonad, I'm thinking of this:<BR/><BR/>counit :: (forall a. (a->x,a)) -> x<BR/><BR/>which is basically your<BR/><BR/>iso :: Coend (Ex1 t) -> t.Kefernoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-52076401495553117252009-03-10T10:22:00.000-07:002009-03-10T10:22:00.000-07:00By definition, the counit is natural. 'cobind&...By definition, the counit is natural. 'cobind', or whatever you want to call it, is (probably) dinatural though.<BR/><BR/>uncurry cobind :: (w a -> b,w a) -> w b<BR/><BR/>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.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-73678496445091066902009-03-10T10:12:00.000-07:002009-03-10T10:12:00.000-07:00Is there a result of the form: every counit of a c...Is there a result of the form: every counit of a comonad is dinatural?<BR/><BR/>I'm thinking of generalizations of the counit of the context comonad.Kefernoreply@blogger.com