Bill Page <bill.p...@newsynthesis.org> writes: | One clarification. Actually despite what Gaby wrote in an earlier | email, I still don't think it is quite correct to claim that a functor | such as List is an endofunctor, at least not in the category-theoretic | sense.
Unless, you have a very exotic definition of endofunctor, List(S) satisfies Type for all S that satisfies Type. How less "endofunctor" can that be? | The reason is that it is defined as follows: | | List(R:Type): Join(ListAggregate(R), ... ) | | The source category of List, i.e. Type, is not the same as the target | category of List, i.e. Join(ListAggregate(R), ... ). The target is included in Type, and that is all that is needed to satisfy the notion `endofunctor'. Being an endofunctor does not require surjectivity! ------------------------------------------------------------------------------ RSA(R) Conference 2012 Save $700 by Nov 18 Register now http://p.sf.net/sfu/rsa-sfdev2dev1 _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
