cat/src/Cat/Category/Monad.agda

186 lines
5.4 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 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
open Category hiding (IsAssociative)
open NaturalTransformation
record RawMonad : Set where
field
R : Functor
-- pure
ηNat : NaturalTransformation F.identity R
-- (>=>)
μNat : NaturalTransformation F[ R R ] R
η : Transformation F.identity R
η = proj₁ ηNat
μ : Transformation F[ R R ] R
μ = proj₁ μNat
2018-02-24 13:00:52 +00:00
private
2018-02-24 13:00:52 +00:00
module R = Functor R
module RR = Functor F[ R R ]
module _ {X : Object} where
-- module IdRX = Functor (F.identity {C = RX})
ηX : [ X , R.func* X ]
ηX = η X
RηX : [ R.func* X , R.func* (R.func* X) ] -- [ R.func* X , {!R.func* (R.func* X))!} ]
RηX = R.func→ ηX
ηRX = η (R.func* X)
IdRX : Arrow (R.func* X) (R.func* X)
IdRX = 𝟙 {R.func* X}
μX : [ RR.func* X , R.func* X ]
μX = μ X
RμX : [ R.func* (RR.func* X) , RR.func* X ]
RμX = R.func→ μX
μRX : [ RR.func* (R.func* X) , R.func* (R.func* X) ]
μRX = μ (R.func* X)
IsAssociative' : Set _
IsAssociative' = [ μX RμX ] [ μX μRX ]
IsInverse' : Set _
IsInverse'
= [ μX ηRX ] IdRX
× [ μX RηX ] IdRX
-- We don't want the objects to be indexes of the type, but rather just
-- universally quantify over *all* objects of the category.
IsAssociative = {X : Object} IsAssociative' {X}
IsInverse = {X : Object} IsInverse' {X}
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-24 13:01:57 +00:00
record Monad : Set where
field
raw : RawMonad
isMonad : IsMonad raw
open IsMonad isMonad public
-- "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
open Category hiding (IsIdentity)
record RawMonad : Set where
field
RR : Object Object
-- Note name-change from [voe]
ζ : {X : Object} [ X , RR X ]
2018-02-24 13:00:52 +00:00
rr : {X Y : Object} [ X , RR Y ] [ RR X , RR Y ]
2018-02-24 14:25:07 +00:00
-- Note the correspondance with Haskell:
--
-- RR ~ m
-- ζ ~ pure
-- rr ~ flip (>>=)
--
-- Where those things have these types:
--
-- m : 𝓤𝓤
-- pure : x → m x
-- flip (>>=) :: (a → m b) → m a → m b
--
2018-02-24 13:00:52 +00:00
IsIdentity = {X : Object}
rr ζ 𝟙 {RR X}
2018-02-24 13:00:52 +00:00
IsNatural = {X Y : Object} (f : [ X , RR Y ])
( [ rr f ζ ]) f
2018-02-24 13:00:52 +00:00
IsDistributive = {X Y Z : Object} (g : [ Y , RR Z ]) (f : [ X , RR Y ])
[ rr g rr f ] rr ( [ rr g f ])
record IsMonad (raw : RawMonad) : Set where
open RawMonad raw public
field
isIdentity : IsIdentity
isNatural : IsNatural
isDistributive : IsDistributive
record Monad : Set where
field
raw : RawMonad
isMonad : IsMonad raw
open IsMonad isMonad public
-- Problem 2.3
module _ {a b : Level} { : Category a b} where
private
open Category using (Object ; Arrow ; 𝟙)
open Functor using (func* ; func→)
module M = Monoidal
module K = Kleisli
module _ (m : M.RawMonad) where
private
open M.RawMonad m
module Kraw = K.RawMonad
RR : Object Object
RR = func* R
R→ : {A B : Object} [ A , B ] [ RR A , RR B ]
R→ = func→ R
ζ : {X : Object} [ X , RR X ]
ζ = {!!}
rr : {X Y : Object} [ X , RR Y ] [ RR X , RR Y ]
-- Order is different now!
rr {X} {Y} f = [ f {!!} ]
where
μY : [ func* F[ R R ] Y , func* R Y ]
μY = μ Y
ζY : [ Y , RR Y ]
ζY = ζ {Y}
forthRaw : K.RawMonad
Kraw.RR forthRaw = RR
Kraw.ζ forthRaw = ζ
Kraw.rr forthRaw = rr
module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
open M.IsMonad m
module Kraw = K.RawMonad (forthRaw raw)
module Kis = K.IsMonad
isIdentity : Kraw.IsIdentity
isIdentity = {!!}
isNatural : Kraw.IsNatural
isNatural = {!!}
isDistributive : Kraw.IsDistributive
isDistributive = {!!}
forthIsMonad : K.IsMonad (forthRaw raw)
Kis.isIdentity forthIsMonad = isIdentity
Kis.isNatural forthIsMonad = isNatural
Kis.isDistributive forthIsMonad = isDistributive
forth : M.Monad K.Monad
Kleisli.Monad.raw (forth m) = forthRaw (M.Monad.raw m)
Kleisli.Monad.isMonad (forth m) = forthIsMonad (M.Monad.isMonad m)
eqv : isEquiv M.Monad K.Monad forth
eqv = {!!}
Monoidal≃Kleisli : M.Monad K.Monad
Monoidal≃Kleisli = forth , eqv