[Proved that concat and _>>=_ are congruences.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100202134700
 Ignore-this: 851209fc26de640a408ff1b4444fc54d
] hunk ./src/Data/List/Any/BagEquality.agda 10
+open import Category.Monad
hunk ./src/Data/List/Any/BagEquality.agda 29
+open RawMonad List.monad
hunk ./src/Data/List/Any/BagEquality.agda 92
+
+-- concat is a congruence.
+
+concat-cong : {A : Set} {xss₁ xss₂ : List (List A)} →
+              xss₁ ≈ xss₂ → concat xss₁ ≈ concat xss₂
+concat-cong xss₁≈xss₂ =
+  concat⇿ ⟪∘⟫ Any-cong (λ _ → Inv.id) xss₁≈xss₂ ⟪∘⟫ Inv.sym concat⇿
+
+-- The list monad's bind is a congruence.
+
+>>=-cong : ∀ {A B : Set} {xs₁ xs₂} {f₁ f₂ : A → List B} →
+           xs₁ ≈ xs₂ → (∀ x → f₁ x ≈ f₂ x) →
+           (xs₁ >>= f₁) ≈ (xs₂ >>= f₂)
+>>=-cong xs₁≈xs₂ f₁≈f₂ =
+  >>=⇿ ⟪∘⟫ Any-cong (λ x → f₁≈f₂ x) xs₁≈xs₂ ⟪∘⟫ Inv.sym >>=⇿