From 19103e1678b7a3c6f0b1b5ebcdcb7049f9d7c018 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 7 Mar 2018 16:24:43 +0100 Subject: [PATCH] Update cubical --- libs/cubical | 2 +- src/Cat/Category/Monad.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/libs/cubical b/libs/cubical index 159c519..2fa05f7 160000 --- a/libs/cubical +++ b/libs/cubical @@ -1 +1 @@ -Subproject commit 159c519936afcfb72afe5c1528637dd0f0a7303a +Subproject commit 2fa05f70edfc59f205be9af2227996bdd6084948 diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 279e457..9c343a2 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -759,7 +759,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where Monoidal→Kleisli = proj₁ Monoidal≃Kleisli Kleisli→Monoidal : K.Monad → M.Monad - Kleisli→Monoidal = reverse Monoidal≃Kleisli + Kleisli→Monoidal = inverse Monoidal≃Kleisli forth : voe-2-3-1 → voe-2-3-2 forth = voe-2-3-2-fromMonad ∘f Monoidal→Kleisli ∘f voe-2-3-1.toMonad