--- a/CCC.agda	Mon Apr 22 02:41:53 2019 +0900
+++ b/CCC.agda	Mon Apr 22 12:43:49 2019 +0900
@@ -52,8 +52,8 @@
         ≈⟨ e3c ⟩
           id1 A (a ∧ b )
         ∎
-     distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ]  ≈  < A [ f o h ] , A [ g o h ] > ]
-     distr {a} {b} {c} {d} {f} {g} {h} = let open  ≈-Reasoning A in begin
+     distr-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ]  ≈  < A [ f o h ] , A [ g o h ] > ]
+     distr-π {a} {b} {c} {d} {f} {g} {h} = let open  ≈-Reasoning A in begin
             < f , g > o h
         ≈↑⟨ e3c ⟩
             < π o  < f , g > o h  , π' o  < f , g > o h  >
@@ -62,8 +62,51 @@
         ≈⟨ π-cong (car e3a ) (car e3b) ⟩
             < f o h ,  g o h  >
         ∎
-     _×_ :  {  a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e )
-     f × g  = λ h →  < A [ f o A [ π o h  ] ] , A [ g o A [ π' o h ] ] >
+     _×_ :  {  a b c d  : Obj A } ( f : Hom A a c ) (g : Hom A b d )  → Hom A (a ∧ b) ( c ∧ d )
+     f × g  = < (A [ f o  π ] ) , (A [ g o π' ])  >
+     distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → A [ A [ h * o k ]  ≈ ( A [ h o < A [ k o π ] , π' > ] ) * ]
+     distr-* {a} {b} {c} {d} {h} {k} = begin
+             h * o k
+        ≈↑⟨ e4b  ⟩
+             (  ε o < (h * o k ) o π  , π' > ) *
+        ≈⟨ *-cong ( begin
+              ε o < (h * o k ) o π  , π' > 
+        ≈↑⟨ cdr ( π-cong assoc refl-hom ) ⟩
+              ε o ( < h * o ( k o π ) , π' > ) 
+        ≈↑⟨ cdr ( π-cong (cdr e3a) e3b ) ⟩
+               ε o ( < h * o ( π o < k o π , π' > ) , π' o < k o π , π' > > ) 
+        ≈⟨ cdr ( π-cong assoc refl-hom) ⟩
+               ε o ( < (h * o π) o < k o π , π' > , π' o < k o π , π' > > ) 
+        ≈↑⟨ cdr ( distr-π ) ⟩
+               ε o ( < h * o π , π' >  o < k o π , π' > )
+        ≈⟨ assoc ⟩
+              ( ε o < h * o π , π' > ) o < k o π , π' > 
+        ≈⟨ car e4a  ⟩
+               h o < k o π , π' > 
+        ∎ ) ⟩
+            ( h o  <  k o π  , π' > ) *
+        ∎ where open  ≈-Reasoning A
+     α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
+     α = < A [ π  o π  ]  , < A [ π'  o π ]  , π'  > >
+     α' : {a b c : Obj A } → Hom A  ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c )
+     α' = < < π , A [ π o π' ] > ,  A [ π'  o π' ]  >
+     β : {a b c d : Obj A } { f : Hom A a b} { g : Hom A a c } { h : Hom A a d } → A [ A [ α o < < f , g > , h > ] ≈  < f , < g , h > > ]
+     β {a} {b} {c} {d} {f} {g} {h} = begin
+             α o < < f , g > , h >
+        ≈⟨⟩
+            ( < ( π o π ) , < ( π' o π ) , π' > > ) o  < < f , g > , h >
+        ≈⟨ distr-π ⟩
+             < ( ( π o π ) o  < < f , g > , h > ) , ( < ( π' o π ) , π' >   o  < < f , g > , h > )  >  
+        ≈⟨ π-cong refl-hom distr-π ⟩
+             < ( ( π o π ) o  < < f , g > , h > ) , ( < ( ( π' o π ) o  < < f , g > , h > ) , ( π'  o  < < f , g > , h > ) > )  >  
+        ≈↑⟨ π-cong assoc ( π-cong assoc refl-hom )  ⟩
+             < (  π o (π  o  < < f , g > , h >) ) , ( < (  π' o ( π  o  < < f , g > , h > ) ) , ( π'  o  < < f , g > , h > ) > )  >  
+        ≈⟨ π-cong (cdr e3a ) ( π-cong (cdr e3a ) e3b )  ⟩
+             < (  π o < f , g >  ) ,  < (  π' o < f , g >  ) , h >   >  
+        ≈⟨ π-cong e3a ( π-cong e3b refl-hom )  ⟩
+            < f , < g , h > >
+         ∎ where open  ≈-Reasoning A
+
 
 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field