copumpkin/categories — pull request #2 by JasonGross (2013-05-11 19:59:07+00:00)
Title: Implement composition of adjunctions

Perhaps composition should be moved to a separate file; this proof takes
up about 1.5 GB RAM and takes around 10-30 minutes to typecheck, on my
machine. The construction was copied from AdjointComposition.v at
https://bitbucket.org/JasonGross/catdb.

I'd appreciate any comments/criticism/suggestions, on style, or otherwise; this is the first agda code I've written which is more than ~10 lines long.