fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Use postulates

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-06 15:55:03 +01:00
parent 5ae68df582
commit 110e3510c5
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Cat/Category/Monad.agda
View file

@ -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)