From 110e3510c5f37b06ceec1088370d470d1ed05a4a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 6 Mar 2018 15:55:03 +0100 Subject: [PATCH] Use postulates --- src/Cat/Category/Monad.agda | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index c7e6ee8..f1b65d1 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -535,11 +535,13 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where postulate pureNTEq : (λ i → NaturalTransformation F.identity (Req i)) [ M.RawMonad.pureNT (backRaw (forth m)) ≡ pureNT ] + joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i)) + [ M.RawMonad.joinNT (backRaw (forth m)) ≡ joinNT ] backRawEq : backRaw (forth m) ≡ M.Monad.raw m -- stuck M.RawMonad.R (backRawEq i) = Req i - M.RawMonad.pureNT (backRawEq i) = {!!} -- pureNTEq i - M.RawMonad.joinNT (backRawEq i) = {!!} + M.RawMonad.pureNT (backRawEq i) = pureNTEq i -- pureNTEq i + M.RawMonad.joinNT (backRawEq i) = joinNTEq i backeq : (m : M.Monad) → back (forth m) ≡ m backeq m = M.Monad≡ (backRawEq m)