On Mon, May 28, 2012 at 7:44 PM, Manfred Lotz <manfred.lotz@arcor.de> wrote:
On Mon, 28 May 2012 10:04:33 -0400
Brent Yorgey <byorgey@seas.upenn.edu> wrote:

> On Mon, May 28, 2012 at 02:08:14PM +0200, Manfred Lotz wrote:
> > On Mon, 28 May 2012 13:34:01 +0200
> > Alessandro Pezzoni <alessandro_pezzoni@lavabit.com> wrote:
> >
> > > On Mon, May 28, 2012 at 11:54:11AM +0200, Manfred Lotz wrote:
> > > > In the definition of a (mathematical) category it is said (among
> > > > other things), that for any object A there exists an identity
> > > > morphism:
> > > >
> > > > idA: A -> A and if f: A -> B for two objects A, B then
> > > >
> > > >    idB . f = f and f . idA = f
> > > >
> > > > must hold.
> > > >
> > > > My question: Because I cannot think of any counterexample for
> > > > the last statement I would like to know if I just could omit
> > > > this from the definition and formulate this as a small theorem.
> > > >
> > > > Or does there exist a counterexample where all conditions of a
> > > > category hold but there exist two objects A, and B where we have
> > > > idB . f <> f and/or f .idA <> f?
> > >
> > > When you ask that
> > >   idB . f = f    and    f . idA = f
> > > you are basically defining a left and a right identity,
> > > respectively.
> > >
> > > If I get your question correctly, you are asking if you can drop
> > > the axiom (requirement) of existence of an identity morphism for
> > > every object and deduce it from the other axioms, i.e. that the
> > > composition of morphisms is always well defined and that it is
> > > associative.
> > >
> >
> > No, I do not want to drop the requirement of existence of an
> > identity morphism. I only want to drop the axion that idB .f = f
> > and f . idA = f do hold because IMHO this follows readily from the
> > definition of what an identity morphism is all about.
>
> "Follows readily from the definition of what an identity morphism is
> all about" -- and what exactly is that defintion?
>

For me id: A -> A could be defined by: A morphism id: A -> A is
called identity morphism iff for all x of A we have  id(x) = x.

Well one of the main themes of category theory is to not have that as a necessary definition. Of course many interesting categories will work as you expect.
But some extreme ones dont eg.

Monoid as a category http://planetmath.org/?method=l2h&id=8111&op=getobj&from=objects

Poset as a category
http://en.wikipedia.org/wiki/Partially_ordered_set#In_category_theory

A more haskell oriented answer will (I guess) talk about the virtues of point-free style...