add Reasoning on Hom

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