--- a/HomReasoning.agda	Thu Mar 02 20:22:42 2017 +0900
+++ b/HomReasoning.agda	Fri Mar 03 12:12:06 2017 +0900
@@ -124,6 +124,12 @@
       →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
   nat η  =  IsNTrans.commute ( isNTrans η  )
 
+  nat1 : { c₁ c₂ ℓ : Level}  {A : Category c₁ c₂ ℓ}  { c₁′ c₂′ ℓ′ : Level}  {D : Category c₁′ c₂′ ℓ′} 
+         {a b : Obj D}   {F G : Functor D A }
+      →  (η : NTrans D A F G ) → (f : Hom D a b)
+      →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
+  nat1 η f =  IsNTrans.commute ( isNTrans η  )
+
   infixr  2 _∎
   infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
   infixr 2 _≈↑⟨_⟩_