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.