# I’m dumb

2003-07-29T01:44:00Z

Okay maybe I’m not dumb, but I do suffer from a problem. I tend to implement the first solution to a problem that I think of instead of trying to think of a better solution. For instance, consider the problem of coming up with a structure to implement a category as a type. The first thought I had was that a category was a pair of Objects and Morphisms where Morphisms have a domain and range, etc. So I would implement it as follows in Coq:

```Record Category : Type := category {
Object : Type
Morphism : Type
Domain : Morphism -> Object
Range : Morphism -> Object
Id : Object -> Morphism
Compose : (f:Morphism)(g:Morphism)->(Range g)=(Domain f)->Morphism
rangeId : (a:Object)(Range (Id a))=a
domainId : (a:Object)(Domain (Id a))=a
…
}```

Much more is omitted. However a much better approach which is more along the lines of the definition given, and similar to how they have been implemented in Coq, is to make `Morphism` a function from two objects to a type.

```Record Category : Type := category {
Object : Type
Morphism : Object -> Object -> Type
Id : (A:Object)(Morphism A A)
Compose : (A,B,C:Object)(Morphism B C) -> (Morphism A B) -> (Morphism A C)
idLeft : (A,B:Object)(f:(Morphism A B))(Compose (Id B) f)=f
idRight : (A,B:Object)(f:(Morphism A B))(Compose f (Id A))=f
assoc : (A,B,C,D:Object)(f:(Morphism A B))(g:(Morphism B C))(h:(Morphism C D))
(Compose h (Compose g f))=(Compose (Compose h g) f)
}```

This definition is shorter, cleaner, and for whatever reason, not the first thing I thought of. In this case I probably wouldn’t have gotten very far without correcting myself, but in other cases I can go pretty far before deciding there are better ways of doing things.

Perhaps I should always wait some time before I implement a solution to a problem. I’m not sure that I’d be creative enough after finding a solution to find a better solution. I consider this a big problem.

## Tags

Russell O’Connor: contact me