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

Add comment

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-06 09:41:29 +01:00
parent 7647a452cd
commit b6457a0b14
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -28,6 +28,8 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
pureNT : NaturalTransformation F.identity R pureNT : NaturalTransformation F.identity R
joinNT : NaturalTransformation F[ R ∘ R ] R joinNT : NaturalTransformation F[ R ∘ R ] R
-- Note that `pureT` and `joinT` differs from their definition in the
-- kleisli formulation only by having an explicit parameter.
pureT : Transformation F.identity R pureT : Transformation F.identity R
pureT = proj₁ pureNT pureT = proj₁ pureNT
pureN : Natural F.identity R pureT pureN : Natural F.identity R pureT