[Haskell-beginners] Category question

[Brent Yorgey]

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 at 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?

In fact, the definition is precisely that

  idB . f = f and f . idA = f

This is not an "extra" requirement on identity morphisms.  It is
simply the definition.

-Brent