This commit is contained in:
Frederik Hanghøj Iversen 2018-03-06 10:05:35 +01:00
parent 9173468b03
commit 4de27aa06c

View file

@ -114,7 +114,7 @@ module Monoidal {a b : Level} ( : Category a b) where
record Monad : Set where record Monad : Set where
field field
raw : RawMonad raw : RawMonad
isMonad : IsMonad raw isMonad : IsMonad raw
open IsMonad isMonad public open IsMonad isMonad public
@ -131,6 +131,7 @@ module Monoidal {a b : Level} ( : Category a b) where
yX = y {X} yX = y {X}
e1 = Category.arrowsAreSets _ _ (proj₁ xX) (proj₁ yX) e1 = Category.arrowsAreSets _ _ (proj₁ xX) (proj₁ yX)
e2 = Category.arrowsAreSets _ _ (proj₂ xX) (proj₂ yX) e2 = Category.arrowsAreSets _ _ (proj₂ xX) (proj₂ yX)
open IsMonad open IsMonad
propIsMonad : (raw : _) isProp (IsMonad raw) propIsMonad : (raw : _) isProp (IsMonad raw)
IsMonad.isAssociative (propIsMonad raw a b i) j IsMonad.isAssociative (propIsMonad raw a b i) j
@ -141,8 +142,9 @@ module Monoidal {a b : Level} ( : Category a b) where
(isInverse a) (isInverse b) i (isInverse a) (isInverse b) i
module _ {m n : Monad} (eq : Monad.raw m Monad.raw n) where module _ {m n : Monad} (eq : Monad.raw m Monad.raw n) where
eqIsMonad : (λ i IsMonad (eq i)) [ Monad.isMonad m Monad.isMonad n ] private
eqIsMonad = lemPropF propIsMonad eq eqIsMonad : (λ i IsMonad (eq i)) [ Monad.isMonad m Monad.isMonad n ]
eqIsMonad = lemPropF propIsMonad eq
Monad≡ : m n Monad≡ : m n
Monad.raw (Monad≡ i) = eq i Monad.raw (Monad≡ i) = eq i
@ -161,23 +163,22 @@ module Kleisli {a b : Level} ( : Category a b) where
-- are not generally types. -- are not generally types.
record RawMonad : Set where record RawMonad : Set where
field field
Romap : Object Object omap : Object Object
-- Note name-change from [voe] pure : {X : Object} [ X , omap X ]
pure : {X : Object} [ X , Romap X ] bind : {X Y : Object} [ X , omap Y ] [ omap X , omap Y ]
bind : {X Y : Object} [ X , Romap Y ] [ Romap X , Romap Y ]
-- | functor map -- | functor map
-- --
-- This should perhaps be defined in a "Klesli-version" of functors as well? -- This should perhaps be defined in a "Klesli-version" of functors as well?
fmap : {A B} [ A , B ] [ Romap A , Romap B ] fmap : {A B} [ A , B ] [ omap A , omap B ]
fmap f = bind (pure f) fmap f = bind (pure f)
-- | Composition of monads aka. the kleisli-arrow. -- | Composition of monads aka. the kleisli-arrow.
_>=>_ : {A B C : Object} [ A , Romap B ] [ B , Romap C ] [ A , Romap C ] _>=>_ : {A B C : Object} [ A , omap B ] [ B , omap C ] [ A , omap C ]
f >=> g = f >>> (bind g) f >=> g = f >>> (bind g)
-- | Flattening nested monads. -- | Flattening nested monads.
join : {A : Object} [ Romap (Romap A) , Romap A ] join : {A : Object} [ omap (omap A) , omap A ]
join = bind 𝟙 join = bind 𝟙
------------------ ------------------
@ -187,10 +188,10 @@ module Kleisli {a b : Level} ( : Category a b) where
-- There may be better names than what I've chosen here. -- There may be better names than what I've chosen here.
IsIdentity = {X : Object} IsIdentity = {X : Object}
bind pure 𝟙 {Romap X} bind pure 𝟙 {omap X}
IsNatural = {X Y : Object} (f : [ X , Romap Y ]) IsNatural = {X Y : Object} (f : [ X , omap Y ])
pure >>> (bind f) f pure >>> (bind f) f
IsDistributive = {X Y Z : Object} (g : [ Y , Romap Z ]) (f : [ X , Romap Y ]) IsDistributive = {X Y Z : Object} (g : [ Y , omap Z ]) (f : [ X , omap Y ])
(bind f) >>> (bind g) bind (f >=> g) (bind f) >>> (bind g) bind (f >=> g)
-- | Functor map fusion. -- | Functor map fusion.
@ -218,23 +219,22 @@ module Kleisli {a b : Level} ( : Category a b) where
fusion : Fusion fusion : Fusion
fusion {g = g} {f} = begin fusion {g = g} {f} = begin
fmap (g f) ≡⟨⟩ fmap (g f) ≡⟨⟩
bind ((f >>> g) >>> pure) ≡⟨ cong bind isAssociative bind ((f >>> g) >>> pure) ≡⟨ cong bind .isAssociative
bind (f >>> (g >>> pure)) ≡⟨ cong (λ φ bind (f >>> φ)) (sym (isNatural _)) bind (f >>> (g >>> pure)) ≡⟨ cong (λ φ bind (f >>> φ)) (sym (isNatural _))
bind (f >>> (pure >>> (bind (g >>> pure)))) ≡⟨⟩ bind (f >>> (pure >>> (bind (g >>> pure)))) ≡⟨⟩
bind (f >>> (pure >>> fmap g)) ≡⟨⟩ bind (f >>> (pure >>> fmap g)) ≡⟨⟩
bind ((fmap g pure) f) ≡⟨ cong bind (sym isAssociative) bind ((fmap g pure) f) ≡⟨ cong bind (sym .isAssociative)
bind (fmap g (pure f)) ≡⟨ sym lem bind (fmap g (pure f)) ≡⟨ sym distrib
bind (pure g) bind (pure f) ≡⟨⟩ bind (pure g) bind (pure f) ≡⟨⟩
fmap g fmap f fmap g fmap f
where where
open Category using (isAssociative) distrib : fmap g fmap f bind (fmap g (pure f))
lem : fmap g fmap f bind (fmap g (pure f)) distrib = isDistributive (pure g) (pure f)
lem = isDistributive (pure g) (pure f)
-- | This formulation gives rise to the following endo-functor. -- | This formulation gives rise to the following endo-functor.
private private
rawR : RawFunctor rawR : RawFunctor
RawFunctor.func* rawR = Romap RawFunctor.func* rawR = omap
RawFunctor.func→ rawR = fmap RawFunctor.func→ rawR = fmap
isFunctorR : IsFunctor rawR isFunctorR : IsFunctor rawR
@ -302,7 +302,6 @@ module Kleisli {a b : Level} ( : Category a b) where
bind 𝟙 >>> R.func→ f ≡⟨⟩ bind 𝟙 >>> R.func→ f ≡⟨⟩
R.func→ f bind 𝟙 ≡⟨⟩ R.func→ f bind 𝟙 ≡⟨⟩
R.func→ f join R.func→ f join
where
pureNT : NaturalTransformation R⁰ R pureNT : NaturalTransformation R⁰ R
proj₁ pureNT = pureT proj₁ pureNT = pureT
@ -400,7 +399,7 @@ module _ {a b : Level} { : Category a b} where
open M.RawMonad m open M.RawMonad m
forthRaw : K.RawMonad forthRaw : K.RawMonad
K.RawMonad.Romap forthRaw = Romap K.RawMonad.omap forthRaw = Romap
K.RawMonad.pure forthRaw = pureT _ K.RawMonad.pure forthRaw = pureT _
K.RawMonad.bind forthRaw = bind K.RawMonad.bind forthRaw = bind
@ -469,7 +468,7 @@ module _ {a b : Level} { : Category a b} where
bind bind
where where
joinT = proj₁ joinNT joinT = proj₁ joinNT
lem : (f : Arrow X (Romap Y)) bind (f >>> pure) >>> bind 𝟙 bind f lem : (f : Arrow X (omap Y)) bind (f >>> pure) >>> bind 𝟙 bind f
lem f = begin lem f = begin
bind (f >>> pure) >>> bind 𝟙 bind (f >>> pure) >>> bind 𝟙
≡⟨ isDistributive _ _ ≡⟨ isDistributive _ _
@ -485,7 +484,7 @@ module _ {a b : Level} { : Category a b} where
x & f = f x x & f = f x
forthRawEq : forthRaw (backRaw m) K.Monad.raw m forthRawEq : forthRaw (backRaw m) K.Monad.raw m
K.RawMonad.Romap (forthRawEq _) = Romap K.RawMonad.omap (forthRawEq _) = omap
K.RawMonad.pure (forthRawEq _) = pure K.RawMonad.pure (forthRawEq _) = pure
-- stuck -- stuck
K.RawMonad.bind (forthRawEq i) = bindEq i K.RawMonad.bind (forthRawEq i) = bindEq i