From a7f31bb3e29f539f34fb14cf656e6795baa5247e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Thu, 1 Mar 2018 18:00:51 +0100
Subject: [PATCH] Prove "foreign naturality condition"

---
 src/Cat/Category/Monad.agda | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 5c815c9..26347a2 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -277,8 +277,22 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
     isNaturalForeign : IsNaturalForeign
     isNaturalForeign = begin
-      join ∘ fmap join ≡⟨ {!!} ⟩
-      join ∘ join      ∎
+      fmap join >>> join ≡⟨⟩
+      bind (join >>> pure) >>> bind 𝟙
+        ≡⟨ isDistributive _ _ ⟩
+      bind ((join >>> pure) >>> bind 𝟙)
+        ≡⟨ cong bind ℂ.isAssociative ⟩
+      bind (join >>> (pure >>> bind 𝟙))
+        ≡⟨ cong (λ φ → bind (join >>> φ)) (isNatural _) ⟩
+      bind (join >>> 𝟙)
+        ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
+      bind join           ≡⟨⟩
+      bind (bind 𝟙)
+        ≡⟨ cong bind (sym (proj₁ ℂ.isIdentity)) ⟩
+      bind (𝟙 >>> bind 𝟙) ≡⟨⟩
+      bind (𝟙 >=> 𝟙)      ≡⟨ sym (isDistributive _ _) ⟩
+      bind 𝟙 >>> bind 𝟙   ≡⟨⟩
+      join >>> join       ∎
 
     isInverse : IsInverse
     isInverse = inv-l , inv-r