cat/src/Cat/Category/Monad.agda

774 lines
28 KiB
Agda
Raw Normal View History

{-# OPTIONS --cubical --allow-unsolved-metas #-}
module Cat.Category.Monad where
open import Agda.Primitive
open import Data.Product
open import Cubical
open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP)
2018-03-06 09:16:42 +00:00
open import Cubical.GradLemma using (gradLemma)
2018-03-02 12:31:46 +00:00
open import Cat.Category
open import Cat.Category.Functor as F
open import Cat.Category.NaturalTransformation
open import Cat.Categories.Fun
-- "A monad in the monoidal form" [voe]
module Monoidal {a b : Level} ( : Category a b) where
private
= a b
2018-02-25 00:27:20 +00:00
open Category using (Object ; Arrow ; 𝟙 ; _∘_)
open NaturalTransformation
record RawMonad : Set where
field
2018-03-06 08:56:44 +00:00
R : EndoFunctor
2018-03-06 08:30:41 +00:00
pureNT : NaturalTransformation F.identity R
joinNT : NaturalTransformation F[ R R ] R
2018-03-06 08:41:29 +00:00
-- Note that `pureT` and `joinT` differs from their definition in the
-- kleisli formulation only by having an explicit parameter.
2018-03-06 08:30:41 +00:00
pureT : Transformation F.identity R
pureT = proj₁ pureNT
pureN : Natural F.identity R pureT
pureN = proj₂ pureNT
2018-02-26 19:31:47 +00:00
2018-03-06 08:30:41 +00:00
joinT : Transformation F[ R R ] R
joinT = proj₁ joinNT
joinN : Natural F[ R R ] R joinT
joinN = proj₂ joinNT
2018-02-24 13:00:52 +00:00
2018-03-06 08:52:01 +00:00
Romap = Functor.func* R
Rfmap = Functor.func→ R
bind : {X Y : Object} [ X , Romap Y ] [ Romap X , Romap Y ]
bind {X} {Y} f = joinT Y Rfmap f
2018-02-25 18:03:30 +00:00
IsAssociative : Set _
IsAssociative = {X : Object}
2018-03-06 08:56:44 +00:00
joinT X Rfmap (joinT X) joinT X joinT (Romap X)
2018-02-25 18:03:30 +00:00
IsInverse : Set _
IsInverse = {X : Object}
2018-03-06 08:56:44 +00:00
joinT X pureT (Romap X) 𝟙
× joinT X Rfmap (pureT X) 𝟙
IsNatural = {X Y} f joinT Y Rfmap f pureT X f
IsDistributive = {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y))
joinT Z Rfmap g (joinT Y Rfmap f)
joinT Z Rfmap (joinT Z Rfmap g f)
record IsMonad (raw : RawMonad) : Set where
open RawMonad raw public
field
isAssociative : IsAssociative
isInverse : IsInverse
2018-02-24 13:00:52 +00:00
2018-02-26 19:31:47 +00:00
private
module R = Functor R
module = Category
isNatural : IsNatural
isNatural {X} {Y} f = begin
2018-03-06 08:30:41 +00:00
joinT Y R.func→ f pureT X ≡⟨ sym .isAssociative
joinT Y (R.func→ f pureT X) ≡⟨ cong (λ φ joinT Y φ) (sym (pureN f))
joinT Y (pureT (R.func* Y) f) ≡⟨ .isAssociative
joinT Y pureT (R.func* Y) f ≡⟨ cong (λ φ φ f) (proj₁ isInverse)
2018-02-26 19:31:47 +00:00
𝟙 f ≡⟨ proj₂ .isIdentity
f
isDistributive : IsDistributive
2018-03-06 08:39:48 +00:00
isDistributive {X} {Y} {Z} g f = sym aux
where
module R² = Functor F[ R R ]
2018-03-06 08:39:48 +00:00
distrib3 : {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
2018-03-01 19:47:36 +00:00
R.func→ (a b c)
R.func→ a R.func→ b R.func→ c
2018-03-06 08:39:48 +00:00
distrib3 {a = a} {b} {c} = begin
R.func→ (a b c) ≡⟨ R.isDistributive
R.func→ (a b) R.func→ c ≡⟨ cong (_∘ _) R.isDistributive
2018-03-01 19:47:36 +00:00
R.func→ a R.func→ b R.func→ c
2018-03-06 08:39:48 +00:00
aux = begin
2018-03-06 08:30:41 +00:00
joinT Z R.func→ (joinT Z R.func→ g f)
2018-03-06 08:39:48 +00:00
≡⟨ cong (λ φ joinT Z φ) distrib3
2018-03-06 08:30:41 +00:00
joinT Z (R.func→ (joinT Z) R.func→ (R.func→ g) R.func→ f)
2018-03-01 19:47:36 +00:00
≡⟨⟩
2018-03-06 08:30:41 +00:00
joinT Z (R.func→ (joinT Z) R².func→ g R.func→ f)
2018-03-06 08:39:48 +00:00
≡⟨ cong (_∘_ (joinT Z)) (sym .isAssociative)
2018-03-06 08:30:41 +00:00
joinT Z (R.func→ (joinT Z) (R².func→ g R.func→ f))
2018-03-01 19:47:36 +00:00
≡⟨ .isAssociative
2018-03-06 08:30:41 +00:00
(joinT Z R.func→ (joinT Z)) (R².func→ g R.func→ f)
2018-03-01 19:47:36 +00:00
≡⟨ cong (λ φ φ (R².func→ g R.func→ f)) isAssociative
2018-03-06 08:30:41 +00:00
(joinT Z joinT (R.func* Z)) (R².func→ g R.func→ f)
2018-03-06 08:39:48 +00:00
≡⟨ .isAssociative
2018-03-06 08:30:41 +00:00
joinT Z joinT (R.func* Z) R².func→ g R.func→ f
2018-03-06 08:39:48 +00:00
≡⟨⟩
2018-03-06 08:30:41 +00:00
((joinT Z joinT (R.func* Z)) R².func→ g) R.func→ f
2018-03-01 19:47:36 +00:00
≡⟨ cong (_∘ R.func→ f) (sym .isAssociative)
2018-03-06 08:30:41 +00:00
(joinT Z (joinT (R.func* Z) R².func→ g)) R.func→ f
2018-03-06 08:39:48 +00:00
≡⟨ cong (λ φ φ R.func→ f) (cong (_∘_ (joinT Z)) (joinN g))
(joinT Z (R.func→ g joinT Y)) R.func→ f
≡⟨ cong (_∘ R.func→ f) .isAssociative
2018-03-06 08:30:41 +00:00
joinT Z R.func→ g joinT Y R.func→ f
2018-03-01 19:47:36 +00:00
≡⟨ sym (Category.isAssociative )
2018-03-06 08:30:41 +00:00
joinT Z R.func→ g (joinT Y R.func→ f)
2018-03-01 19:47:36 +00:00
2018-02-24 13:01:57 +00:00
record Monad : Set where
field
2018-03-06 09:05:35 +00:00
raw : RawMonad
2018-02-24 13:01:57 +00:00
isMonad : IsMonad raw
open IsMonad isMonad public
2018-03-01 19:12:49 +00:00
private
module _ {m : RawMonad} where
open RawMonad m
propIsAssociative : isProp IsAssociative
propIsAssociative x y i {X}
= Category.arrowsAreSets _ _ (x {X}) (y {X}) i
propIsInverse : isProp IsInverse
propIsInverse x y i {X} = e1 i , e2 i
where
xX = x {X}
yX = y {X}
e1 = Category.arrowsAreSets _ _ (proj₁ xX) (proj₁ yX)
e2 = Category.arrowsAreSets _ _ (proj₂ xX) (proj₂ yX)
2018-03-06 09:05:35 +00:00
2018-03-01 19:12:49 +00:00
open IsMonad
propIsMonad : (raw : _) isProp (IsMonad raw)
IsMonad.isAssociative (propIsMonad raw a b i) j
= propIsAssociative {raw}
(isAssociative a) (isAssociative b) i j
IsMonad.isInverse (propIsMonad raw a b i)
= propIsInverse {raw}
(isInverse a) (isInverse b) i
module _ {m n : Monad} (eq : Monad.raw m Monad.raw n) where
2018-03-06 09:05:35 +00:00
private
eqIsMonad : (λ i IsMonad (eq i)) [ Monad.isMonad m Monad.isMonad n ]
eqIsMonad = lemPropF propIsMonad eq
2018-03-01 19:12:49 +00:00
Monad≡ : m n
Monad.raw (Monad≡ i) = eq i
Monad.isMonad (Monad≡ i) = eqIsMonad i
-- "A monad in the Kleisli form" [voe]
2018-02-24 13:00:52 +00:00
module Kleisli {a b : Level} ( : Category a b) where
private
= a b
2018-03-01 13:58:01 +00:00
module = Category
open using (Arrow ; 𝟙 ; Object ; _∘_ ; _>>>_)
2018-02-26 19:08:48 +00:00
-- | Data for a monad.
--
-- Note that (>>=) is not expressible in a general category because objects
-- are not generally types.
2018-02-24 13:00:52 +00:00
record RawMonad : Set where
field
2018-03-06 09:05:35 +00:00
omap : Object Object
pure : {X : Object} [ X , omap X ]
bind : {X Y : Object} [ X , omap Y ] [ omap X , omap Y ]
2018-02-26 19:08:48 +00:00
-- | functor map
--
-- This should perhaps be defined in a "Klesli-version" of functors as well?
2018-03-06 09:05:35 +00:00
fmap : {A B} [ A , B ] [ omap A , omap B ]
2018-02-26 18:58:27 +00:00
fmap f = bind (pure f)
2018-02-26 19:08:48 +00:00
-- | Composition of monads aka. the kleisli-arrow.
2018-03-06 09:05:35 +00:00
_>=>_ : {A B C : Object} [ A , omap B ] [ B , omap C ] [ A , omap C ]
2018-02-26 18:57:05 +00:00
f >=> g = f >>> (bind g)
2018-02-26 19:08:48 +00:00
-- | Flattening nested monads.
2018-03-06 09:05:35 +00:00
join : {A : Object} [ omap (omap A) , omap A ]
2018-02-26 18:57:05 +00:00
join = bind 𝟙
2018-02-26 19:08:48 +00:00
------------------
-- * Monad laws --
------------------
-- There may be better names than what I've chosen here.
2018-02-24 13:00:52 +00:00
IsIdentity = {X : Object}
2018-03-06 09:05:35 +00:00
bind pure 𝟙 {omap X}
IsNatural = {X Y : Object} (f : [ X , omap Y ])
2018-02-26 18:57:05 +00:00
pure >>> (bind f) f
2018-03-06 09:05:35 +00:00
IsDistributive = {X Y Z : Object} (g : [ Y , omap Z ]) (f : [ X , omap Y ])
2018-02-26 18:57:05 +00:00
(bind f) >>> (bind g) bind (f >=> g)
2018-02-26 19:08:48 +00:00
-- | Functor map fusion.
--
-- This is really a functor law. Should we have a kleisli-representation of
-- functors as well and make them a super-class?
Fusion = {X Y Z : Object} {g : [ Y , Z ]} {f : [ X , Y ]}
fmap (g f) fmap g fmap f
2018-02-24 13:00:52 +00:00
2018-03-01 13:58:01 +00:00
-- In the ("foreign") formulation of a monad `IsNatural`'s analogue here would be:
IsNaturalForeign : Set _
IsNaturalForeign = {X : Object} join {X} fmap join join join
IsInverse : Set _
IsInverse = {X : Object} join {X} pure 𝟙 × join {X} fmap pure 𝟙
2018-02-24 13:00:52 +00:00
record IsMonad (raw : RawMonad) : Set where
open RawMonad raw public
field
isIdentity : IsIdentity
isNatural : IsNatural
isDistributive : IsDistributive
2018-02-26 19:23:31 +00:00
-- | Map fusion is admissable.
fusion : Fusion
fusion {g = g} {f} = begin
2018-02-26 19:23:31 +00:00
fmap (g f) ≡⟨⟩
2018-03-06 09:05:35 +00:00
bind ((f >>> g) >>> pure) ≡⟨ cong bind .isAssociative
2018-02-26 18:57:05 +00:00
bind (f >>> (g >>> pure)) ≡⟨ cong (λ φ bind (f >>> φ)) (sym (isNatural _))
bind (f >>> (pure >>> (bind (g >>> pure)))) ≡⟨⟩
bind (f >>> (pure >>> fmap g)) ≡⟨⟩
2018-03-06 09:05:35 +00:00
bind ((fmap g pure) f) ≡⟨ cong bind (sym .isAssociative)
bind (fmap g (pure f)) ≡⟨ sym distrib
bind (pure g) bind (pure f) ≡⟨⟩
fmap g fmap f
where
2018-03-06 09:05:35 +00:00
distrib : fmap g fmap f bind (fmap g (pure f))
distrib = isDistributive (pure g) (pure f)
2018-02-24 13:00:52 +00:00
-- | This formulation gives rise to the following endo-functor.
private
rawR : RawFunctor
2018-03-06 09:05:35 +00:00
RawFunctor.func* rawR = omap
2018-02-28 18:31:53 +00:00
RawFunctor.func→ rawR = fmap
isFunctorR : IsFunctor rawR
IsFunctor.isIdentity isFunctorR = begin
bind (pure 𝟙) ≡⟨ cong bind (proj₁ .isIdentity)
bind pure ≡⟨ isIdentity
𝟙
IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
bind (pure (g f)) ≡⟨⟩
fmap (g f) ≡⟨ fusion
fmap g fmap f ≡⟨⟩
bind (pure g) bind (pure f)
-- TODO: Naming!
2018-02-28 18:03:11 +00:00
R : EndoFunctor
Functor.raw R = rawR
Functor.isFunctor R = isFunctorR
2018-02-28 18:31:53 +00:00
private
open NaturalTransformation
R⁰ : EndoFunctor
R⁰ = F.identity
: EndoFunctor
= F[ R R ]
module R = Functor R
module R = Functor R⁰
module R² = Functor
2018-03-06 08:30:41 +00:00
pureT : Transformation R⁰ R
pureT A = pure
2018-03-06 08:45:04 +00:00
pureN : Natural R⁰ R pureT
pureN {A} {B} f = begin
2018-03-06 08:30:41 +00:00
pureT B R⁰.func→ f ≡⟨⟩
2018-02-28 18:31:53 +00:00
pure f ≡⟨ sym (isNatural _)
bind (pure f) pure ≡⟨⟩
fmap f pure ≡⟨⟩
2018-03-06 08:30:41 +00:00
R.func→ f pureT A
joinT : Transformation R
joinT C = join
2018-03-06 08:45:04 +00:00
joinN : Natural R joinT
joinN f = begin
join R².func→ f ≡⟨⟩
bind 𝟙 R².func→ f ≡⟨⟩
R².func→ f >>> bind 𝟙 ≡⟨⟩
fmap (fmap f) >>> bind 𝟙 ≡⟨⟩
fmap (bind (f >>> pure)) >>> bind 𝟙 ≡⟨⟩
bind (bind (f >>> pure) >>> pure) >>> bind 𝟙
≡⟨ isDistributive _ _
bind ((bind (f >>> pure) >>> pure) >=> 𝟙)
≡⟨⟩
bind ((bind (f >>> pure) >>> pure) >>> bind 𝟙)
≡⟨ cong bind .isAssociative
bind (bind (f >>> pure) >>> (pure >>> bind 𝟙))
≡⟨ cong (λ φ bind (bind (f >>> pure) >>> φ)) (isNatural _)
bind (bind (f >>> pure) >>> 𝟙)
≡⟨ cong bind (proj₂ .isIdentity)
bind (bind (f >>> pure))
≡⟨ cong bind (sym (proj₁ .isIdentity))
bind (𝟙 >>> bind (f >>> pure)) ≡⟨⟩
bind (𝟙 >=> (f >>> pure))
≡⟨ sym (isDistributive _ _)
bind 𝟙 >>> bind (f >>> pure) ≡⟨⟩
bind 𝟙 >>> fmap f ≡⟨⟩
bind 𝟙 >>> R.func→ f ≡⟨⟩
R.func→ f bind 𝟙 ≡⟨⟩
R.func→ f join
2018-02-28 18:31:53 +00:00
2018-03-06 08:30:41 +00:00
pureNT : NaturalTransformation R⁰ R
proj₁ pureNT = pureT
2018-03-06 08:45:04 +00:00
proj₂ pureNT = pureN
2018-02-28 18:31:53 +00:00
2018-03-06 08:30:41 +00:00
joinNT : NaturalTransformation R
proj₁ joinNT = joinT
2018-03-06 08:45:04 +00:00
proj₂ joinNT = joinN
2018-02-28 18:31:53 +00:00
2018-03-01 13:58:01 +00:00
isNaturalForeign : IsNaturalForeign
isNaturalForeign = begin
2018-03-01 17:00:51 +00:00
fmap join >>> join ≡⟨⟩
bind (join >>> pure) >>> bind 𝟙
≡⟨ isDistributive _ _
bind ((join >>> pure) >>> bind 𝟙)
≡⟨ cong bind .isAssociative
bind (join >>> (pure >>> bind 𝟙))
≡⟨ cong (λ φ bind (join >>> φ)) (isNatural _)
bind (join >>> 𝟙)
≡⟨ cong bind (proj₂ .isIdentity)
bind join ≡⟨⟩
bind (bind 𝟙)
≡⟨ cong bind (sym (proj₁ .isIdentity))
bind (𝟙 >>> bind 𝟙) ≡⟨⟩
bind (𝟙 >=> 𝟙) ≡⟨ sym (isDistributive _ _)
bind 𝟙 >>> bind 𝟙 ≡⟨⟩
join >>> join
2018-03-01 13:58:01 +00:00
isInverse : IsInverse
isInverse = inv-l , inv-r
where
inv-l = begin
2018-03-01 16:50:06 +00:00
pure >>> join ≡⟨⟩
pure >>> bind 𝟙 ≡⟨ isNatural _
2018-03-01 13:58:01 +00:00
𝟙
inv-r = begin
2018-03-01 16:50:06 +00:00
fmap pure >>> join ≡⟨⟩
bind (pure >>> pure) >>> bind 𝟙
≡⟨ isDistributive _ _
bind ((pure >>> pure) >=> 𝟙) ≡⟨⟩
bind ((pure >>> pure) >>> bind 𝟙)
≡⟨ cong bind .isAssociative
bind (pure >>> (pure >>> bind 𝟙))
≡⟨ cong (λ φ bind (pure >>> φ)) (isNatural _)
bind (pure >>> 𝟙)
≡⟨ cong bind (proj₂ .isIdentity)
bind pure ≡⟨ isIdentity
2018-03-01 13:58:01 +00:00
𝟙
2018-02-24 13:00:52 +00:00
record Monad : Set where
field
raw : RawMonad
isMonad : IsMonad raw
open IsMonad isMonad public
2018-03-06 09:16:42 +00:00
private
module _ (raw : RawMonad) where
open RawMonad raw
propIsIdentity : isProp IsIdentity
propIsIdentity x y i = .arrowsAreSets _ _ x y i
propIsNatural : isProp IsNatural
propIsNatural x y i = λ f
.arrowsAreSets _ _ (x f) (y f) i
propIsDistributive : isProp IsDistributive
propIsDistributive x y i = λ g f
.arrowsAreSets _ _ (x g f) (y g f) i
open IsMonad
propIsMonad : (raw : _) isProp (IsMonad raw)
IsMonad.isIdentity (propIsMonad raw x y i)
= propIsIdentity raw (isIdentity x) (isIdentity y) i
IsMonad.isNatural (propIsMonad raw x y i)
= propIsNatural raw (isNatural x) (isNatural y) i
IsMonad.isDistributive (propIsMonad raw x y i)
= propIsDistributive raw (isDistributive x) (isDistributive y) i
module _ {m n : Monad} (eq : Monad.raw m Monad.raw n) where
2018-03-06 09:06:45 +00:00
private
eqIsMonad : (λ i IsMonad (eq i)) [ Monad.isMonad m Monad.isMonad n ]
eqIsMonad = lemPropF propIsMonad eq
Monad≡ : m n
Monad.raw (Monad≡ i) = eq i
Monad.isMonad (Monad≡ i) = eqIsMonad i
2018-02-26 19:23:31 +00:00
-- | The monoidal- and kleisli presentation of monads are equivalent.
--
2018-03-06 22:18:23 +00:00
-- This is *not* problem 2.3 in [voe].
2018-02-26 19:23:31 +00:00
-- This is problem 2.3 in [voe].
module _ {a b : Level} { : Category a b} where
private
module = Category
open using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_)
open Functor using (func* ; func→)
module M = Monoidal
2018-03-06 08:55:18 +00:00
module K = Kleisli
module _ (m : M.RawMonad) where
2018-03-06 08:52:01 +00:00
open M.RawMonad m
forthRaw : K.RawMonad
2018-03-06 09:16:42 +00:00
K.RawMonad.omap forthRaw = Romap
2018-03-06 08:52:01 +00:00
K.RawMonad.pure forthRaw = pureT _
K.RawMonad.bind forthRaw = bind
module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
2018-03-01 13:19:46 +00:00
private
module MI = M.IsMonad m
forthIsMonad : K.IsMonad (forthRaw raw)
2018-03-06 08:55:18 +00:00
K.IsMonad.isIdentity forthIsMonad = proj₂ MI.isInverse
K.IsMonad.isNatural forthIsMonad = MI.isNatural
K.IsMonad.isDistributive forthIsMonad = MI.isDistributive
forth : M.Monad K.Monad
2018-03-06 09:16:42 +00:00
Kleisli.Monad.raw (forth m) = forthRaw (M.Monad.raw m)
Kleisli.Monad.isMonad (forth m) = forthIsMonad (M.Monad.isMonad m)
module _ (m : K.Monad) where
2018-03-06 09:16:42 +00:00
open K.Monad m
backRaw : M.RawMonad
2018-03-06 09:16:42 +00:00
M.RawMonad.R backRaw = R
M.RawMonad.pureNT backRaw = pureNT
M.RawMonad.joinNT backRaw = joinNT
2018-03-01 13:58:01 +00:00
private
2018-03-06 09:16:42 +00:00
open M.RawMonad backRaw
module R = Functor (M.RawMonad.R backRaw)
2018-03-01 13:58:01 +00:00
2018-03-01 13:19:46 +00:00
backIsMonad : M.IsMonad backRaw
2018-03-06 09:16:42 +00:00
M.IsMonad.isAssociative backIsMonad {X} = begin
2018-03-06 08:30:41 +00:00
joinT X R.func→ (joinT X) ≡⟨⟩
2018-03-06 09:16:42 +00:00
join fmap (joinT X) ≡⟨⟩
join fmap join ≡⟨ isNaturalForeign
join join ≡⟨⟩
2018-03-06 08:30:41 +00:00
joinT X joinT (R.func* X)
2018-03-06 09:16:42 +00:00
M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r
2018-03-01 13:58:01 +00:00
where
inv-l = begin
2018-03-06 08:30:41 +00:00
joinT X pureT (R.func* X) ≡⟨⟩
2018-03-06 09:16:42 +00:00
join pure ≡⟨ proj₁ isInverse
𝟙
2018-03-01 13:58:01 +00:00
inv-r = begin
2018-03-06 08:30:41 +00:00
joinT X R.func→ (pureT X) ≡⟨⟩
2018-03-06 09:16:42 +00:00
join fmap pure ≡⟨ proj₂ isInverse
𝟙
2018-02-24 18:07:58 +00:00
back : K.Monad M.Monad
Monoidal.Monad.raw (back m) = backRaw m
Monoidal.Monad.isMonad (back m) = backIsMonad m
2018-02-25 02:12:23 +00:00
module _ (m : K.Monad) where
2018-03-06 14:52:22 +00:00
private
open K.Monad m
bindEq : {X Y}
K.RawMonad.bind (forthRaw (backRaw m)) {X} {Y}
K.RawMonad.bind (K.Monad.raw m)
bindEq {X} {Y} = begin
K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩
(λ f join fmap f) ≡⟨⟩
(λ f bind (f >>> pure) >>> bind 𝟙) ≡⟨ funExt lem
(λ f bind f) ≡⟨⟩
bind
where
lem : (f : Arrow X (omap Y))
bind (f >>> pure) >>> bind 𝟙
bind f
lem f = begin
bind (f >>> pure) >>> bind 𝟙
≡⟨ isDistributive _ _
bind ((f >>> pure) >>> bind 𝟙)
≡⟨ cong bind .isAssociative
bind (f >>> (pure >>> bind 𝟙))
≡⟨ cong (λ φ bind (f >>> φ)) (isNatural _)
bind (f >>> 𝟙)
≡⟨ cong bind (proj₂ .isIdentity)
bind f
2018-02-25 02:12:23 +00:00
forthRawEq : forthRaw (backRaw m) K.Monad.raw m
2018-03-06 09:05:35 +00:00
K.RawMonad.omap (forthRawEq _) = omap
2018-02-26 18:58:27 +00:00
K.RawMonad.pure (forthRawEq _) = pure
K.RawMonad.bind (forthRawEq i) = bindEq i
2018-02-24 18:07:58 +00:00
fortheq : (m : K.Monad) forth (back m) m
fortheq m = K.Monad≡ (forthRawEq m)
2018-02-25 02:12:23 +00:00
module _ (m : M.Monad) where
2018-03-06 14:52:22 +00:00
private
open M.Monad m
module KM = K.Monad (forth m)
module R = Functor R
omapEq : KM.omap Romap
omapEq = refl
bindEq : {X Y} {f : Arrow X (Romap Y)} KM.bind f bind f
bindEq {X} {Y} {f} = begin
KM.bind f ≡⟨⟩
joinT Y Rfmap f ≡⟨⟩
bind f
joinEq : {X} KM.join joinT X
joinEq {X} = begin
KM.join ≡⟨⟩
KM.bind 𝟙 ≡⟨⟩
bind 𝟙 ≡⟨⟩
joinT X Rfmap 𝟙 ≡⟨ cong (λ φ _ φ) R.isIdentity
joinT X 𝟙 ≡⟨ proj₁ .isIdentity
joinT X
fmapEq : {A B} KM.fmap {A} {B} Rfmap
fmapEq {A} {B} = funExt (λ f begin
KM.fmap f ≡⟨⟩
KM.bind (f >>> KM.pure) ≡⟨⟩
bind (f >>> pureT _) ≡⟨⟩
Rfmap (f >>> pureT B) >>> joinT B ≡⟨⟩
Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ φ >>> joinT B) R.isDistributive
Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ .isAssociative
joinT B Rfmap (pureT B) Rfmap f ≡⟨ cong (λ φ φ Rfmap f) (proj₂ isInverse)
𝟙 Rfmap f ≡⟨ proj₂ .isIdentity
Rfmap f
)
rawEq : Functor.raw KM.R Functor.raw R
RawFunctor.func* (rawEq i) = omapEq i
RawFunctor.func→ (rawEq i) = fmapEq i
2018-03-05 16:31:13 +00:00
Req : M.RawMonad.R (backRaw (forth m)) R
2018-03-05 16:10:41 +00:00
Req = Functor≡ rawEq
open NaturalTransformation
2018-03-07 14:23:07 +00:00
pureTEq : M.RawMonad.pureT (backRaw (forth m)) pureT
pureTEq = funExt (λ X refl)
pureNTEq : (λ i NaturalTransformation F.identity (Req i))
[ M.RawMonad.pureNT (backRaw (forth m)) pureNT ]
pureNTEq = lemSigP (λ i propIsNatural F.identity (Req i)) _ _ pureTEq
2018-03-07 14:23:07 +00:00
joinTEq : M.RawMonad.joinT (backRaw (forth m)) joinT
joinTEq = funExt (λ X begin
M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩
KM.join ≡⟨⟩
joinT X Rfmap 𝟙 ≡⟨ cong (λ φ joinT X φ) R.isIdentity
joinT X 𝟙 ≡⟨ proj₁ .isIdentity
joinT X )
joinNTEq : (λ i NaturalTransformation F[ Req i Req i ] (Req i))
[ M.RawMonad.joinNT (backRaw (forth m)) joinNT ]
joinNTEq = lemSigP (λ i propIsNatural F[ Req i Req i ] (Req i)) _ _ joinTEq
2018-03-07 14:23:07 +00:00
2018-02-25 02:12:23 +00:00
backRawEq : backRaw (forth m) M.Monad.raw m
2018-03-06 09:16:42 +00:00
M.RawMonad.R (backRawEq i) = Req i
2018-03-06 22:18:23 +00:00
M.RawMonad.pureNT (backRawEq i) = pureNTEq i
2018-03-06 14:55:03 +00:00
M.RawMonad.joinNT (backRawEq i) = joinNTEq i
2018-02-24 18:07:58 +00:00
backeq : (m : M.Monad) back (forth m) m
backeq m = M.Monad≡ (backRawEq m)
2018-02-24 18:07:58 +00:00
eqv : isEquiv M.Monad K.Monad forth
2018-02-24 18:07:58 +00:00
eqv = gradLemma forth back fortheq backeq
Monoidal≃Kleisli : M.Monad K.Monad
Monoidal≃Kleisli = forth , eqv
2018-03-06 22:18:23 +00:00
2018-03-07 10:33:08 +00:00
module _ {a b : Level} ( : Category a b) where
2018-03-06 22:18:23 +00:00
private
= a b
module = Category
open using (Object ; Arrow ; _∘_)
open NaturalTransformation
module M = Monoidal
module K = Kleisli
module voe-2-3 (omap : Omap ) (pure : {X : Object} Arrow X (omap X)) where
2018-03-06 22:18:23 +00:00
record voe-2-3-1 : Set where
open M
field
fmap : Fmap omap
join : {A : Object} [ omap (omap A) , omap A ]
Rraw : RawFunctor
Rraw = record
{ func* = omap
; func→ = fmap
}
field
RisFunctor : IsFunctor Rraw
R : EndoFunctor
R = record
{ raw = Rraw
; isFunctor = RisFunctor
}
pureT : (X : Object) Arrow X (omap X)
pureT X = pure {X}
field
pureN : Natural F.identity R pureT
pureNT : NaturalTransformation F.identity R
pureNT = pureT , pureN
joinT : (A : Object) [ omap (omap A) , omap A ]
joinT A = join {A}
field
joinN : Natural F[ R R ] R joinT
joinNT : NaturalTransformation F[ R R ] R
joinNT = joinT , joinN
rawMnd : RawMonad
rawMnd = record
{ R = R
; pureNT = pureNT
; joinNT = joinNT
}
field
isMnd : IsMonad rawMnd
toMonad : Monad
toMonad = record
2018-03-06 22:18:23 +00:00
{ raw = rawMnd
; isMonad = isMnd
}
record voe-2-3-2 : Set where
open K
field
bind : {X Y : Object} [ X , omap Y ] [ omap X , omap Y ]
rawMnd : RawMonad
rawMnd = record
{ omap = omap
; pure = pure
; bind = bind
}
field
isMnd : IsMonad rawMnd
toMonad : Monad
toMonad = record
2018-03-06 22:18:23 +00:00
{ raw = rawMnd
; isMonad = isMnd
}
module _ {a b : Level} { : Category a b} where
private
module M = Monoidal
module K = Kleisli
2018-03-07 10:33:08 +00:00
open voe-2-3
voe-2-3-1-fromMonad : (m : M.Monad) voe-2-3-1 (M.Monad.Romap m) (λ {X} M.Monad.pureT m X)
voe-2-3-1-fromMonad m = record
{ fmap = Functor.func→ R
; RisFunctor = Functor.isFunctor R
; pureN = pureN
; join = λ {X} joinT X
; joinN = joinN
; isMnd = M.Monad.isMonad m
}
where
raw = M.Monad.raw m
R = M.RawMonad.R raw
pureT = M.RawMonad.pureT raw
pureN = M.RawMonad.pureN raw
joinT = M.RawMonad.joinT raw
joinN = M.RawMonad.joinN raw
voe-2-3-2-fromMonad : (m : K.Monad) voe-2-3-2 (K.Monad.omap m) (K.Monad.pure m)
voe-2-3-2-fromMonad m = record
{ bind = K.Monad.bind m
; isMnd = K.Monad.isMonad m
}
module _ {a b : Level} { : Category a b} where
private
= a b
module = Category
open using (Object ; Arrow)
open NaturalTransformation
module M = Monoidal
module K = Kleisli
open import Function using (_∘_ ; _$_)
module _ (omap : Omap ) (pure : {X : Object} Arrow X (omap X)) where
2018-03-07 23:36:38 +00:00
open voe-2-3
private
Monoidal→Kleisli : M.Monad K.Monad
Monoidal→Kleisli = proj₁ Monoidal≃Kleisli
Kleisli→Monoidal : K.Monad M.Monad
2018-03-07 15:24:43 +00:00
Kleisli→Monoidal = inverse Monoidal≃Kleisli
2018-03-07 23:36:38 +00:00
forth : voe-2-3-1 omap pure voe-2-3-2 omap pure
forth = voe-2-3-2-fromMonad Monoidal→Kleisli voe-2-3.voe-2-3-1.toMonad
2018-03-07 23:36:38 +00:00
back : voe-2-3-2 omap pure voe-2-3-1 omap pure
back = voe-2-3-1-fromMonad Kleisli→Monoidal voe-2-3.voe-2-3-2.toMonad
2018-03-07 10:45:11 +00:00
2018-03-07 23:36:38 +00:00
forthEq : m _ _
forthEq m = begin
(forth back) m ≡⟨⟩
-- In full gory detail:
2018-03-07 23:36:38 +00:00
( voe-2-3-2-fromMonad
Monoidal→Kleisli
voe-2-3.voe-2-3-1.toMonad
voe-2-3-1-fromMonad
Kleisli→Monoidal
voe-2-3.voe-2-3-2.toMonad
2018-03-07 23:36:38 +00:00
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
( voe-2-3-2-fromMonad
Monoidal→Kleisli
Kleisli→Monoidal
voe-2-3.voe-2-3-2.toMonad
2018-03-07 23:36:38 +00:00
) m ≡⟨ u
-- Monoidal→Kleisli and Kleisli→Monoidal are inverses
-- I should be able to prove this using congruence and `lem` below.
2018-03-07 23:36:38 +00:00
( voe-2-3-2-fromMonad
voe-2-3.voe-2-3-2.toMonad
2018-03-07 23:36:38 +00:00
) m ≡⟨⟩
( voe-2-3-2-fromMonad
voe-2-3.voe-2-3-2.toMonad
2018-03-07 23:36:38 +00:00
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
m
where
lem : Monoidal→Kleisli Kleisli→Monoidal Function.id
lem = verso-recto Monoidal≃Kleisli
t : { : Level} {A B : Set } {a : _ A} {b : B _}
a (Monoidal→Kleisli Kleisli→Monoidal) b a b
t {a = a} {b} = cong (λ φ a φ b) lem
u : { : Level} {A B : Set } {a : _ A} {b : B _}
{m : _} (a (Monoidal→Kleisli Kleisli→Monoidal) b) m (a b) m
u {m = m} = cong (λ φ φ m) t
2018-03-07 10:45:11 +00:00
backEq : m (back forth) m m
backEq m = begin
(back forth) m ≡⟨⟩
2018-03-07 23:36:38 +00:00
( voe-2-3-1-fromMonad
Kleisli→Monoidal
2018-03-07 23:36:38 +00:00
voe-2-3.voe-2-3-2.toMonad
voe-2-3-2-fromMonad
Monoidal→Kleisli
2018-03-07 23:36:38 +00:00
voe-2-3.voe-2-3-1.toMonad
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
( voe-2-3-1-fromMonad
Kleisli→Monoidal
Monoidal→Kleisli
2018-03-07 23:36:38 +00:00
voe-2-3.voe-2-3-1.toMonad
) m ≡⟨ cong (λ φ φ m) t -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
( voe-2-3-1-fromMonad
voe-2-3.voe-2-3-1.toMonad
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
m
2018-03-07 23:36:38 +00:00
where
t = cong (λ φ voe-2-3-1-fromMonad φ voe-2-3.voe-2-3-1.toMonad) (recto-verso Monoidal≃Kleisli)
2018-03-07 23:36:38 +00:00
voe-isEquiv : isEquiv (voe-2-3-1 omap pure) (voe-2-3-2 omap pure) forth
voe-isEquiv = gradLemma forth back forthEq backEq
2018-03-07 23:36:38 +00:00
equiv-2-3 : voe-2-3-1 omap pure voe-2-3-2 omap pure
equiv-2-3 = forth , voe-isEquiv