konn/category-agda — pull request #2 by shinji-kono (2013-07-14 07:10:43+00:00)
Title: add Reasoning on Hom

≡-Reasoning does not work for A [ x ≈ y ], so I add ≈-Reasoning. It also contains Natural transformation.