Yoneda was Re: [Agda] Associativity for free!

[Thorsten Altenkirch]

P.S. Just remembered that I forgot one thing:

On 3 Nov 2011, at 09:39, Thorsten Altenkirch wrote:

> On 28 Oct 2011, at 16:26, Andreas Abel wrote:
> 
>> On 10/27/11 3:47 PM, James Chapman wrote:
>>> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>>> 
>>> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
>>> Y {C} f = λ Z g → comp C g f
>>> 
>>> and we can convert back again:
>>> 
>>> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
>>> Y-1 {C}{A}{B} α = α B (iden C)
>> 
>> Is that the glorious Yoneda lemma?  Trivial in the language of types. Just subtract the categorical waffle and every programmer understands it...
> 
> Indeed, I have been pushing this for a while. Actually given F : Set -> Set a functor, Yoneda just says for any A : Set:
> 
> ((X : Set) -> (A -> X) -> F X) ~ F A
> 
> where ~ is isomorphism (or equality f we accept univalence). And yes this is a consequence of parametricity or more precisely of the assumption that (X : Set) -> H X X is a coend (where H : Set^op -> Set -> Set is a bifunctor).
> 
> One interesting aspect of this equation is that the left hand side is actually large (in Set_1) while the right hand side is small. So it is a "resizing axiom" which enables to make big things small.
> 
> There are many nice applications of the Yoneda lemma. One of my favourites is the derivation of the exponential of endofunctors (i.e. the function space in Set -> Set) which is actually a categorical generalisation of Kripke semantics.
> 
> Given F,G : Set -> Set (functors) and exponential F=>G if it exists must satisfy
> 
> 	((X : Set) -> (H x F) X -> G X) ~ ((X : Set) -> H X -> (F => G) X)		(1)
> 
> and it is easy to see that (H x F) X = H X x F X (products are constructed pointwise).
> 
> Hence we can calculate
> 
> 	(F => G) A
> 	~ (X : Set) (A -> X) -> (F => G) X		(Yoneda)
> 	~ (X : Set) (A -> X) x F X -> G X			(1)
> 	~ (X : Set) (A -> X) -> F X -> G X		(currying)
> 
> The relation to Kripke semantics becomes clear if we read (A -> X) as X is a future of A. Actually we should really use the contravariant version then we can read -> as implication.

Don't forget that I said *if* it exists the exponential looks like this. However, we have no reason to assume that in general 
(X : Set) (A -> X) -> F X -> G X : Set. It is the case if we assume that F and G are containers (see our CIE paper from last year). 

> 
> It is a generalisation because it is an isomorphism as opposed to a logical equivalence.
> 
> So, yes, functional programmers should be aware of the Yoneda lemma. Ralph Hinze recently wrote a nice paper expressing the same sentiment (after I showed him the little proof above).
> 
> Obviously, Yoneda is much more general than what I wrote above. As indicated it also works for covariant functors and there also is a version with SIgma types instead of Pi types.
> 
> Cheers,
> Thorsten
> 
> 
> 
> 
>> 
>> Cheers,
>> Andreas
>> 
>> -- 
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>> 
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>> 
>> andreas.abel at ifi.lmu.de
>> http://www2.tcs.ifi.lmu.de/~abel/
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda