--- a/CCC.agda	Sun Apr 21 18:11:14 2019 +0900
+++ b/CCC.agda	Mon Apr 22 02:41:53 2019 +0900
@@ -22,7 +22,7 @@
              :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field
        -- cartesian
-       e2  : {a : Obj A} → ∀ ( f : Hom A a １ ) →  A [ f ≈ ○ a ]
+       e2  : {a : Obj A} → ∀ { f : Hom A a １ } →  A [ f ≈ ○ a ]
        e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o < f , g > ] ≈ f ]
        e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π' o < f , g > ] ≈ g ]
        e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } →  A [ < A [ π o h ] , A [ π' o h  ] >  ≈ h ]
@@ -35,13 +35,13 @@
      e'2 : A [ ○ １ ≈ id1 A １ ]
      e'2 = let open  ≈-Reasoning A in begin
             ○ １
-        ≈↑⟨ e2 (id1 A １ ) ⟩
+        ≈↑⟨ e2  ⟩
            id1 A １
         ∎
      e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [  ○ b o f ] ≈ ○ a ]
      e''2 {a} {b} {f} = let open  ≈-Reasoning A in begin
            ○ b o f
-        ≈⟨ e2 (○ b o f) ⟩
+        ≈⟨ e2  ⟩
            ○ a
         ∎
      π-id : {a b : Obj A} → A [ < π ,  π' >  ≈ id1 A (a ∧ b ) ]