--- a/list-nat.agda	Fri Jul 12 11:39:06 2013 +0900
+++ b/list-nat.agda	Fri Jul 12 12:24:29 2013 +0900
@@ -30,72 +30,62 @@
 
 data _==_ {n} {A : Set n} :  List A -> List A -> Set n where
       reflection  : {x : List A} -> x == x
-      eq-cons : {x y : List A} { a : A } -> x ==  y -> ( a :: x ) == ( a :: y )
-      trans-list : {x y z : List A} { a : A } -> x ==  y -> y == z -> x == z
+
+cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
+   ( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
+cong1 f reflection = reflection
+
+eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) -> x ==  y -> ( a :: x ) == ( a :: y )
+eq-cons a z = cong1 ( \x -> ( a :: x) ) z
+
+trans-list :  ∀{n} {A : Set n} {x y z : List A} { a : A } -> x ==  y -> y == z -> x == z
+trans-list reflection reflection = reflection
 
 
-==-to-≡ :  ∀{n} {A : Set n}  {x y : List A} { a : A } -> x ==  y -> x ≡ y
-==-to-≡ = ?
-
---      eq-nil  : [] == []
+==-to-≡ :  ∀{n} {A : Set n}  {x y : List A}  -> x ==  y -> x ≡ y
+==-to-≡ reflection = refl
 
 list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
 list-id-l = reflection
 
 list-id-r : { A : Set } -> ( x : List A ) ->  x ++ [] == x
 list-id-r [] =   reflection
-list-id-r (x :: xs) =  eq-cons ( list-id-r xs )
-
-
--- listAssoc : { A : Set } -> { a b c : List A} ->  ( ( a ++ b ) ++ c ) == ( a ++ ( b ++ c ) )
--- listAssoc   = eq-reflection
+list-id-r (x :: xs) =  eq-cons x ( list-id-r xs )
 
 list-assoc : {A : Set } -> ( xs ys zs : List A ) ->
      ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
 list-assoc  [] ys zs = reflection
-list-assoc  (x :: xs)  ys zs = eq-cons ( list-assoc xs ys zs )
-
-
+list-assoc  (x :: xs)  ys zs = eq-cons x ( list-assoc xs ys zs )
 
 
---open ≡-Reasoning
-
-cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
-   ( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
-cong1 f reflection = reflection
-cong1 f  ( eq-cons c ) = ?
-cong1 f  ( trans-list a b ) = ?
-
 module ==-Reasoning {n} (A : Set n) where
 
-
   infixr  2 _∎
   infixr 2 _==⟨_⟩_
   infix  1 begin_
 
 
-  data _IsRelatedTo_ {a} {A1 : Set a} (x : List A) {b} {B : Set b} (y : List A) :
+  data _IsRelatedTo_ (x y : List A) :
                      Set n where
     relTo : (x≈y : x  == y  ) → x IsRelatedTo y
 
-  begin_ : ∀ {a} {A1 : Set a} {x : List A } {b} {B : Set b} {y : List A} →
+  begin_ : {x : List A } {y : List A} →
            x IsRelatedTo y →  x ==  y 
   begin relTo x≈y = x≈y
 
-  _==⟨_⟩_ : ∀ {a} {A1 : Set a} (x : List A ) {b} {B : Set b} {y : List A}
-             {c} {C : Set c} {z : List A } →
+  _==⟨_⟩_ : (x : List A ) {y z : List A} →
             x == y  → y IsRelatedTo z → x IsRelatedTo z
-  _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list (==-to-≡ x≈y) y≈z)
+  _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)
 
   _∎ : ∀ {a} {A1 : Set a} (x : List A ) → x IsRelatedTo x
   _∎ _ = relTo reflection
 
-lemma11 : {A : Set } ( x : List A ) -> x == x
-lemma11 x = {A : Set } {x : List A } -> let open ==-Reasoning A in
+lemma11 : ∀{n} (A : Set n) ( x : List A ) -> x == x
+lemma11 A x =  let open ==-Reasoning A in
      begin x ∎
       
-++-assoc : {L : Set} ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
-++-assoc [] ys zs = {A : Set} -> let open ==-Reasoning A in
+++-assoc : (L : Set) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
+++-assoc A [] ys zs = let open ==-Reasoning A in
   begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)
    ( [] ++ ys ) ++ zs
   ==⟨ reflection ⟩
@@ -104,14 +94,14 @@
     [] ++ ( ys ++ zs )
   ∎
   
-++-assoc (x :: xs) ys zs = {A : Set} -> let open  ==-Reasoning A in
+++-assoc A (x :: xs) ys zs = let open  ==-Reasoning A in
   begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
     ((x :: xs) ++ ys) ++ zs
   ==⟨ reflection ⟩
      (x :: (xs ++ ys)) ++ zs
   ==⟨ reflection ⟩
     x :: ((xs ++ ys) ++ zs)
-  ==⟨ cong1 (_::_ x) (++-assoc xs ys zs) ⟩ 
+  ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩ 
     x :: (xs ++ (ys ++ zs))
   ==⟨ reflection ⟩
     (x :: xs) ++ (ys ++ zs)

--- a/nat.agda	Fri Jul 12 11:39:06 2013 +0900
+++ b/nat.agda	Fri Jul 12 12:24:29 2013 +0900
@@ -128,12 +128,9 @@
      join c g f = A [ Trans μ c  o A [ FMap T g  o f ] ]
 
 
-open import Relation.Binary.Core  renaming (Trans to Trans1 )
 
 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
-
-  -- The code in Relation.Binary.EqReasoning cannot handle                                                                              
-  -- heterogeneous equalities, hence the code duplication here.                                                                         
+  open import Relation.Binary.Core 
 
   refl-hom :   {a b : Obj A } { x : Hom A a b }  →
         A [ x ≈ x ]