# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1431491296 -32400
# Node ID cf9c0f12cec56bc8d9806bb8e3c510e88f295a66
# Parent  71c817f28bc68f2a35f72d95592818a8657840ab
fix

diff -r 71c817f28bc6 -r cf9c0f12cec5 yoneda.agda
--- a/yoneda.agda	Tue May 12 11:17:38 2015 +0900
+++ b/yoneda.agda	Wed May 13 13:28:16 2015 +0900
@@ -68,28 +68,15 @@
         ; identityR = refl
         ; o-resp-≈ =  λ{a b c f g h i } → o-resp-≈      {a} {b} {c} {f} {g} {h} {i}
         ; associative = refl
-        } where
+        } where 
+            open ≈-Reasoning (Sets {c₂}) 
             sym1 : {a b : YObj A } {i j : YHom A a b } → i == j → j == i
-            sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning (Sets {c₂}) in begin
-                 TMap j x
-             ≈⟨ sym eq ⟩
-                 TMap i x
-             ∎ 
+            sym1 {a} {b} {i} {j} eq {x} = sym eq 
             trans1 : {a b : YObj A } {i j k : YHom A a b} → i == j → j == k → i == k
-            trans1 {a} {b} {i} {j} {k} i=j j=k {x} =  let open ≈-Reasoning (Sets {c₂}) in begin
-                 TMap i x
-             ≈⟨ i=j ⟩
-                 TMap j x
-             ≈⟨ j=k ⟩
-                 TMap k x
-             ∎
+            trans1 {a} {b} {i} {j} {k} i=j j=k {x} =  trans-hom i=j j=k
             o-resp-≈ : {A₁ B C : YObj A} {f g : YHom A A₁ B} {h i : YHom A B C} → 
                 f == g → h == i → h + f == i + g
-            o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = let open ≈-Reasoning (Sets {c₂}) in begin
-                 (Sets {c₂}) [ TMap h x  o TMap f x ]
-             ≈⟨ resp f=g h=i ⟩
-                 (Sets {c₂}) [ TMap i x  o TMap g x ]
-             ∎
+            o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = resp  f=g h=i
 
 SetsAop :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  → Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁)
 SetsAop {_} {c₂} {_} A  =