[Simplified the definition of equality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091127194056
 Ignore-this: 7a7f0f8816cb548ff2574b46d062d453
] hunk ./ReverseComposition.agda 53
-_≈_ : ∀ {As₁ As₂ B₁ B₂} → As₁ ⇨ B₁ → As₂ ⇨ B₂ → Set
-_≈_ {[]}       {[]}       x y = x ≅ y
-_≈_ {[]}       {A₂ ∷ As₂} f g = ⊥
-_≈_ {A₁ ∷ As₁} {[]}       f g = ⊥
-_≈_ {A₁ ∷ As₁} {A₂ ∷ As₂} f g =
-  A₁ ≡ A₂ × (∀ {x y} → x ≅ y → f · x ≈ g · y)
+data _≈_ : ∀ {As₁ As₂ B₁ B₂} → As₁ ⇨ B₁ → As₂ ⇨ B₂ → Set₁ where
+  val : ∀ {B} {x : [] ⇨ B} → x ≈ x
+  fun : ∀ {A As₁ B₁ As₂ B₂} {f₁ : A ∷ As₁ ⇨ B₁} {f₂ : A ∷ As₂ ⇨ B₂}
+        (f₁≈f₂ : ∀ x → f₁ · x ≈ f₂ · x) → f₁ ≈ f₂
hunk ./ReverseComposition.agda 58
-  -- If A₁ and A₂ were not required to be equal, then the equality
-  -- would not be transitive.
+refl : ∀ {As B} {f : As ⇨ B} → f ≈ f
+refl {[]}     = val
+refl {A ∷ As} = fun (λ _ → refl)
hunk ./ReverseComposition.agda 62
-refl : ∀ {As B} (f : As ⇨ B) → f ≈ f
-refl {[]}     f = H.refl
-refl {A ∷ As} f = (P.refl , λ {x} x≅y →
-  H.subst (λ z → f · x ≈ f · z) x≅y (refl (f · x)))
-
-sym : ∀ {As₁ As₂ B₁ B₂} (f : As₁ ⇨ B₁) {g : As₂ ⇨ B₂} →
+sym : ∀ {As₁ As₂ B₁ B₂} {f : As₁ ⇨ B₁} {g : As₂ ⇨ B₂} →
hunk ./ReverseComposition.agda 64
-sym {[]}    {[]}     f           f≅g  = H.sym f≅g
-sym {A ∷ _} {.A ∷ _} f (P.refl , f≈g) =
-  (P.refl , λ {_ y} → sym (f · y) ∘ f≈g ∘ H.sym)
-
-sym {[]}    {_ ∷ _}  _ ()
-sym {_ ∷ _} {[]}     _ ()
+sym val       = val
+sym (fun f≈g) = fun (sym ∘ f≈g)
hunk ./ReverseComposition.agda 68
-          (f : As₁ ⇨ B₁) {g : As₂ ⇨ B₂} {h : As₃ ⇨ B₃} →
+          {f : As₁ ⇨ B₁} {g : As₂ ⇨ B₂} {h : As₃ ⇨ B₃} →
hunk ./ReverseComposition.agda 70
-trans {[]}    {[]}     {[]}     f           f≅g            g≅h  =
-  H.trans f≅g g≅h
-trans {A ∷ _} {.A ∷ _} {.A ∷ _} f (P.refl , f≈g) (P.refl , g≈h) =
-  (P.refl , λ {x} x≅z → trans (f · x) (f≈g x≅z) (g≈h H.refl))
-
-trans {_}     {[]}     {_ ∷ _} _ _   ()
-trans {[]}    {_ ∷ _}          _ ()  _
-trans {_ ∷ _} {[]}             _ ()  _
-trans {_}     {_ ∷ _}  {[]}    _ _   ()
+trans val       val       = val
+trans (fun f≈g) (fun g≈h) = fun (λ x → trans (f≈g x) (g≈h x))
hunk ./ReverseComposition.agda 81
-                     : Set where
+                     : Set₁ where
hunk ./ReverseComposition.agda 91
-  f ≈⟨ f≈g ⟩ relTo g≈h = relTo (trans f f≈g g≈h)
+  _ ≈⟨ f≈g ⟩ relTo g≈h = relTo (trans f≈g g≈h)
hunk ./ReverseComposition.agda 98
-  f ∎ = relTo (refl f)
+  _ ∎ = relTo refl
hunk ./ReverseComposition.agda 129
-  left-identity : ∀ {A As B} (f : A → As ⇨ B) x → return x >>= f ≈ f x
-  left-identity f x = refl (f x)
+  left-identity : ∀ {A As B} (f : A → As ⇨ B) x →
+                  return x >>= f ≈ f x
+  left-identity f x = refl
hunk ./ReverseComposition.agda 134
-  right-identity {[]}     x = refl x
-  right-identity {A ∷ As} f = (P.refl , λ {x} x≅y →
-    H.subst (λ z → f · x >>= return ≈ f · z) x≅y
-            (right-identity (f · x)))
+  right-identity {[]}     x = refl
+  right-identity {A ∷ As} f = fun (λ x → right-identity (f · x))
hunk ./ReverseComposition.agda 140
-  assoc {[]}     x g h = refl (x >>= g >>= h)
-  assoc {A ∷ As} f g h = (P.refl , λ {x} x≅y →
-    H.subst (λ z → (f · x >>= g) >>= h ≈
-                       f · z >>= (λ x → g x >>= h))
-            x≅y
-            (assoc (f · x) g h))
+  assoc {[]}     x g h = refl
+  assoc {A ∷ As} f g h = fun (λ x → assoc (f · x) g h)
hunk ./ReverseComposition.agda 190
-  f₁≈f₂ ·-cong x₁≅x₂ = proj₂ f₁≈f₂ x₁≅x₂
+  fun f₁≈f₂ ·-cong H.refl = f₁≈f₂ _
hunk ./ReverseComposition.agda 196
-  Λ-cong A₁≡A₂ f₁≈f₂ = (A₁≡A₂ , λ {_} → f₁≈f₂)
-
-  >>=-cong : ∀ {As₁ B₁ Bs₁ C₁} (f₁ : As₁ ⇨ B₁) {g₁ : B₁ → Bs₁ ⇨ C₁}
-               {As₂ B₂ Bs₂ C₂} {f₂ : As₂ ⇨ B₂} {g₂ : B₂ → Bs₂ ⇨ C₂} →
-             f₁ ≈ f₂ → (∀ {x₁ x₂} → x₁ ≅ x₂ → g₁ x₁ ≈ g₂ x₂) →
-             f₁ >>= g₁ ≈ f₂ >>= g₂
-  >>=-cong {As₁ = []}    _  {As₂ = []}     H.refl           g₁≈g₂ =
-    g₁≈g₂ H.refl
-  >>=-cong {As₁ = A ∷ _} f₁ {As₂ = .A ∷ _} (P.refl , f₁≈f₂) g₁≈g₂ =
-    (P.refl , λ {x} x≅y → >>=-cong (f₁ · x) (f₁≈f₂ x≅y) g₁≈g₂)
+  Λ-cong P.refl f₁≈f₂ = fun (λ _ → f₁≈f₂ H.refl)
hunk ./ReverseComposition.agda 198
-  >>=-cong {As₁ = []}    _ {As₂ = _ ∷ _} () _
-  >>=-cong {As₁ = _ ∷ _} _ {As₂ = []}    () _
+  _>>=-cong_ : ∀ {As₁ B₁ Bs₁ C₁} {f₁ : As₁ ⇨ B₁} {g₁ : B₁ → Bs₁ ⇨ C₁}
+                 {As₂ B₂ Bs₂ C₂} {f₂ : As₂ ⇨ B₂} {g₂ : B₂ → Bs₂ ⇨ C₂} →
+               f₁ ≈ f₂ → (∀ {x₁ x₂} → x₁ ≅ x₂ → g₁ x₁ ≈ g₂ x₂) →
+               f₁ >>= g₁ ≈ f₂ >>= g₂
+  val       >>=-cong g₁≈g₂ = g₁≈g₂ H.refl
+  fun f₁≈f₂ >>=-cong g₁≈g₂ = fun (λ x → f₁≈f₂ x >>=-cong g₁≈g₂)
hunk ./ReverseComposition.agda 207
-  return-cong H.refl = refl (return _)
+  return-cong H.refl = refl
hunk ./ReverseComposition.agda 209
-  ⊙-cong : ∀ {As₁ B₁ Bs₁ C₁} (f₁ : As₁ ⇨ B₁) {g₁ : B₁ ∷ Bs₁ ⇨ C₁}
-             {As₂ B₂ Bs₂ C₂} {f₂ : As₂ ⇨ B₂} {g₂ : B₂ ∷ Bs₂ ⇨ C₂} →
-           f₁ ≈ f₂ → g₁ ≈ g₂ → f₁ ⊙ g₁ ≈ f₂ ⊙ g₂
-  ⊙-cong f₁ f₁≈f₂ g₁≈g₂ = >>=-cong f₁ f₁≈f₂ (proj₂ g₁≈g₂)
+  _⊙-cong_ : ∀ {As₁ B₁ Bs₁ C₁} {f₁ : As₁ ⇨ B₁} {g₁ : B₁ ∷ Bs₁ ⇨ C₁}
+               {As₂ B₂ Bs₂ C₂} {f₂ : As₂ ⇨ B₂} {g₂ : B₂ ∷ Bs₂ ⇨ C₂} →
+             f₁ ≈ f₂ → g₁ ≈ g₂ → f₁ ⊙ g₁ ≈ f₂ ⊙ g₂
+  _⊙-cong_ {g₁ = g₁} {g₂ = g₂} f₁≈f₂ (fun g₁≈g₂) =
+    f₁≈f₂ >>=-cong (λ {x₁} x₁≅x₂ →
+      H.subst (λ z → g₁ · x₁ ≈ g₂ · z) x₁≅x₂ (g₁≈g₂ x₁))
hunk ./ReverseComposition.agda 217
-  identity-cong = refl identity
+  identity-cong = refl