Re: abstraction of notation from sets.

[Paul Levy <pbl@cs.bham.ac.uk>]

On 26 Feb 2010, at 18:53, Richard Garner wrote:
>
> I think it is more perspicuous to treat this, not as an
> overloading of \in, but as an "implicit conversion"
> associated to the notion of category; that is, we allow the
> forgetful functor Cat->Set to be applied silently in contexts
> which otherwise would not type-check. In fact the vast
> majority of "abuses of notation" are of this character, when
> applied to, for example, any forgetful functor from an
> Eilenberg-Moore category; the discrete category functor
> Set->Cat; the Yoneda embedding C -> [C^op, Set]; the
> forgetful functor from universal cones to their vertex, etc,
> etc. In principle this becomes problematic as soon as the
> category generated by all such implicit conversions has
> non-identity idempotents;

Why restrict this to idempotents?  Surely the category needs to be a
preorder for the usage to be unambiguous?

Paul


> in practice, this category is free
> on a graph and we hope to identify a shortest path between
> two vertices!
>
> Richard
>


--
Paul Blain Levy
School of Computer Science, University of Birmingham
+44 (0)121 414 4792
http://www.cs.bham.ac.uk/~pbl











[For admin and other information see: http://www.mta.ca/~cat-dist/ ]