|
660
|
1 open import Level
|
|
|
2 open import Category
|
|
|
3 open import Category.Sets
|
|
|
4 module maybe-monad {c : Level} where
|
|
|
5
|
|
|
6 open import HomReasoning
|
|
|
7 open import cat-utility
|
|
|
8 open import Relation.Binary.Core
|
|
661
|
9 open import Category.Cat
|
|
660
|
10
|
|
|
11 import Relation.Binary.PropositionalEquality
|
|
|
12 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
|
|
|
13 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
|
|
|
14
|
|
|
15 data maybe (A : Set c) : Set c where
|
|
|
16 just : A → maybe A
|
|
|
17 nothing : maybe A
|
|
|
18
|
|
|
19 -- Maybe : A → ⊥ + A
|
|
|
20
|
|
|
21 A = Sets {c}
|
|
|
22
|
|
|
23 Maybe : Functor A A
|
|
|
24 Maybe = record {
|
|
|
25 FObj = λ a → maybe a
|
|
|
26 ; FMap = λ {a} {b} f → fmap f
|
|
|
27 ; isFunctor = record {
|
|
|
28 identity = λ {x} → extensionality A ( λ y → identity1 x y )
|
|
|
29 ; distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ w → distr2 a b c f g w )
|
|
|
30 ; ≈-cong = λ {a} {b} {c} {f} f≡g → extensionality A ( λ z → ≈-cong1 a b c f z f≡g )
|
|
|
31 }
|
|
|
32 } where
|
|
|
33 fmap : {a b : Obj A} → (f : Hom A a b ) → Hom A (maybe a) (maybe b)
|
|
|
34 fmap f nothing = nothing
|
|
|
35 fmap f (just x) = just (f x)
|
|
|
36 identity1 : (x : Obj A) → (y : maybe x ) → fmap (id1 A x) y ≡ id1 A (maybe x) y
|
|
|
37 identity1 x nothing = refl
|
|
|
38 identity1 x (just y) = refl
|
|
|
39 distr2 : (x y z : Obj A) (f : Hom A x y ) ( g : Hom A y z ) → (w : maybe x) → fmap (λ w → g (f w)) w ≡ fmap g ( fmap f w)
|
|
|
40 distr2 x y z f g nothing = refl
|
|
|
41 distr2 x y z f g (just w) = refl
|
|
|
42 ≈-cong1 : (x y : Obj A) ( f g : Hom A x y ) → ( z : maybe x ) → f ≡ g → fmap f z ≡ fmap g z
|
|
|
43 ≈-cong1 x y f g nothing refl = refl
|
|
|
44 ≈-cong1 x y f g (just z) refl = refl
|
|
|
45
|
|
661
|
46 -- Maybe-η : 1 → M
|
|
|
47
|
|
|
48 open Functor
|
|
|
49 open NTrans
|
|
|
50
|
|
|
51 Maybe-η : NTrans A A identityFunctor Maybe
|
|
|
52 Maybe-η = record {
|
|
|
53 TMap = λ a → λ(x : a) → just x ;
|
|
|
54 isNTrans = record {
|
|
|
55 commute = λ {a b : Obj A} {f : Hom A a b} → comm a b f
|
|
|
56 }
|
|
|
57 } where
|
|
|
58 comm1 : (a b : Obj A) (f : Hom A a b) → (x : a) →
|
|
|
59 (A [ FMap Maybe f o just ]) x ≡ (A [ just o FMap (identityFunctor {_} {_} {_} {A}) f ]) x
|
|
|
60 comm1 a b f x = refl
|
|
|
61 comm : (a b : Obj A) (f : Hom A a b) →
|
|
|
62 A [ A [ Functor.FMap Maybe f o (λ x → just x) ] ≈
|
|
|
63 A [ (λ x → just x) o FMap (identityFunctor {_} {_} {_} {A} ) f ] ]
|
|
|
64 comm a b f = extensionality A ( λ x → comm1 a b f x )
|
|
|
65
|
|
|
66
|
|
|
67
|
|
|
68 -- Maybe-μ : MM → M
|
|
660
|
69
|
|
661
|
70 Maybe-μ : NTrans A A ( Maybe ○ Maybe ) Maybe
|
|
|
71 Maybe-μ = record {
|
|
|
72 TMap = λ a → tmap a
|
|
|
73 ; isNTrans = record {
|
|
|
74 commute = comm
|
|
|
75 }
|
|
|
76 } where
|
|
|
77 tmap : (a : Obj A) → Hom A (FObj (Maybe ○ Maybe) a) (FObj Maybe a )
|
|
|
78 tmap a nothing = nothing
|
|
|
79 tmap a (just nothing ) = nothing
|
|
|
80 tmap a (just (just x) ) = just x
|
|
|
81 comm1 : (a b : Obj A) (f : Hom A a b) → ( x : maybe ( maybe a) ) →
|
|
|
82 ( A [ FMap Maybe f o tmap a ] ) x ≡ ( A [ tmap b o FMap (Maybe ○ Maybe) f ] ) x
|
|
|
83 comm1 a b f nothing = refl
|
|
|
84 comm1 a b f (just nothing ) = refl
|
|
|
85 comm1 a b f (just (just x)) = refl
|
|
|
86 comm : {a b : Obj A} {f : Hom A a b} →
|
|
|
87 A [ A [ FMap Maybe f o tmap a ] ≈ A [ tmap b o FMap (Maybe ○ Maybe) f ] ]
|
|
|
88 comm {a} {b} {f} = extensionality A ( λ x → comm1 a b f x )
|
|
|
89
|
|
|
90 MaybeMonad : Monad A Maybe Maybe-η Maybe-μ
|
|
|
91 MaybeMonad = record {
|
|
|
92 isMonad = record {
|
|
|
93 unity1 = unity1
|
|
|
94 ; unity2 = unity2
|
|
|
95 ; assoc = assoc
|
|
|
96 }
|
|
|
97 } where
|
|
|
98 unity1-1 : (a : Obj A ) → (x : maybe a) → (A [ TMap Maybe-μ a o TMap Maybe-η (FObj Maybe a) ]) x ≡ id1 A (FObj Maybe a) x
|
|
|
99 unity1-1 a nothing = refl
|
|
|
100 unity1-1 a (just x) = refl
|
|
|
101 unity2-1 : (a : Obj A ) → (x : maybe a) → (A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-η a) ]) x ≡ id1 A (FObj Maybe a) x
|
|
|
102 unity2-1 a nothing = refl
|
|
|
103 unity2-1 a (just x) = refl
|
|
|
104 assoc-1 : (a : Obj A ) → (x : maybe (maybe (maybe a))) → (A [ TMap Maybe-μ a o TMap Maybe-μ (FObj Maybe a) ]) x ≡
|
|
|
105 (A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-μ a) ]) x
|
|
|
106 assoc-1 a nothing = refl
|
|
|
107 assoc-1 a (just nothing) = refl
|
|
|
108 assoc-1 a (just (just nothing )) = refl
|
|
|
109 assoc-1 a (just (just (just x) )) = refl
|
|
|
110 unity1 : {a : Obj A} →
|
|
|
111 A [ A [ TMap Maybe-μ a o TMap Maybe-η (FObj Maybe a) ] ≈ id1 A (FObj Maybe a) ]
|
|
|
112 unity1 {a} = extensionality A ( λ x → unity1-1 a x )
|
|
|
113 unity2 : {a : Obj A} →
|
|
|
114 A [ A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-η a) ] ≈ id1 A (FObj Maybe a) ]
|
|
|
115 unity2 {a} = extensionality A ( λ x → unity2-1 a x )
|
|
|
116 assoc : {a : Obj A} → A [ A [ TMap Maybe-μ a o TMap Maybe-μ (FObj Maybe a) ] ≈
|
|
|
117 A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-μ a) ] ]
|
|
|
118 assoc {a} = extensionality A ( λ x → assoc-1 a x )
|
|
|
119
|
|
|
120
|
|
|
121
|
