From 00e6e1aa6603b8cbc625694570d2a79b45408018 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 7 Mar 2018 11:45:11 +0100
Subject: [PATCH] State problem with approach

---
 src/Cat/Category/Monad.agda | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index f2b6ee0..7ffe664 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -719,6 +719,19 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       back : voe-2-3-2 → voe-2-3-1
       back = voe-2-3-1-fromMonad ∘f Kleisli→Monoidal ∘f voe-2-3-2.toMonad
 
+      Voe-2-3-1-inverse = (toMonad ∘f fromMonad) ≡ Function.id
+        where
+        toMonad : voe-2-3-1 → M.Monad
+        toMonad = voe-2-3-1.toMonad
+        t : (m : M.Monad) → voe-2-3.voe-2-3-1 ℂ (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
+        t = voe-2-3-1-fromMonad
+        -- Problem: `t` does not fit the type of `fromMonad`!
+        fromMonad : M.Monad → voe-2-3-1
+        fromMonad = {!t!}
+
+      voe-2-3-1-inverse : Voe-2-3-1-inverse
+      voe-2-3-1-inverse = {!!}
+
       forthEq : ∀ m → (forth ∘f back) m ≡ m
       forthEq m = begin
         (forth ∘f back) m ≡⟨⟩