[Changed the type of the proof constructor return.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101119150324
 Ignore-this: 854c7280d3de71312f0fdc98a7a67c15
] hunk ./ReverseComposition.agda 57
-  return : ∀ {B} {x : B} → return x ≈ return x
+  return : ∀ {B} {x₁ x₂ : B} →
+           (x₁≡x₂ : x₁ ≡ x₂) → return x₁ ≈ return x₂
hunk ./ReverseComposition.agda 63
-refl (return x) = return
+refl (return x) = return P.refl
hunk ./ReverseComposition.agda 68
-sym return  = return
-sym (Λ f≈g) = Λ (sym ∘ f≈g)
+sym (return x≡y) = return (P.sym x≡y)
+sym (Λ f≈g)      = Λ (sym ∘ f≈g)
hunk ./ReverseComposition.agda 74
-trans return  return  = return
-trans (Λ f≈g) (Λ g≈h) = Λ (λ x → trans (f≈g x) (g≈h x))
+trans (return x≡y) (return y≡z) = return (P.trans x≡y y≡z)
+trans (Λ f≈g)      (Λ g≈h)      = Λ (λ x → trans (f≈g x) (g≈h x))
hunk ./ReverseComposition.agda 132
-!-cong return = H.refl
+!-cong (return x₁≡x₂) = H.≡-to-≅ x₁≡x₂
hunk ./ReverseComposition.agda 152
-  right-identity (return x) = return
+  right-identity (return x) = return P.refl
hunk ./ReverseComposition.agda 167
-  return  >>=-cong g₁≈g₂ = g₁≈g₂ H.refl
-  Λ f₁≈f₂ >>=-cong g₁≈g₂ = Λ λ x → f₁≈f₂ x >>=-cong g₁≈g₂
+  return x₁≡x₂ >>=-cong g₁≈g₂ = g₁≈g₂ (H.≡-to-≅ x₁≡x₂)
+  Λ f₁≈f₂      >>=-cong g₁≈g₂ = Λ λ x → f₁≈f₂ x >>=-cong g₁≈g₂