Mercurial > hg > Members > kono > Proof > category

comparison monoid-monad.agda @ 142:94796ddb9570

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Aug 2013 18:02:45 +0900
parents 4a362cf32a74
children bbaaca9b21ce
comparison
equal deleted inserted replaced
141:4a362cf32a74 142:94796ddb9570
2 open import Category.Monoid 2 open import Category.Monoid
3 open import Algebra 3 open import Algebra
4 open import Level 4 open import Level
5 module monoid-monad {c c₁ c₂ ℓ : Level} { Mono : Monoid c ℓ} where 5 module monoid-monad {c c₁ c₂ ℓ : Level} { Mono : Monoid c ℓ} where
6 6
7 open import Algebra.Structures
7 open import HomReasoning 8 open import HomReasoning
8 open import cat-utility 9 open import cat-utility
9 open import Category.Cat 10 open import Category.Cat
10 open import Category.Sets 11 open import Category.Sets
11 open import Data.Product 12 open import Data.Product
74 } 75 }
75 } 76 }
76 77
77 open NTrans 78 open NTrans
78 79
79 Lemma-MM31 : ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x )) ≡ ( λ x → x ) 80 Lemma-MM32 : ∀{ℓ} {a : Set ℓ } -> {f g : a -> a } -> {x : a } -> ( f ≡ g ) -> ( ( λ x → f x ) ≡ ( λ x → g x ) )
80 Lemma-MM31 = ? 81 Lemma-MM32 eq = cong ( \f -> \x -> f x ) eq
82
83 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x )
84 Lemma-MM33 = _≡_.refl
85
86 Lemma-M-34 : ( x : Carrier Mono ) -> _≈_ Mono ((_∙_ Mono (ε Mono) x)) x
87 Lemma-M-34 = proj₁ ( IsMonoid.identity ( isMonoid Mono ) )
88
89 Lemma-MM31 : ( a : Obj ( Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ) -> {x : FObj T a } → (((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ) ≡ x )
90 Lemma-MM31 a = {!!}
81 91
82 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ 92 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ
83 MonoidMonad = record { 93 MonoidMonad = record {
84 isMonad = record { 94 isMonad = record {
85 unity1 = \{a} -> Lemma-MM3 {a} ; 95 unity1 = \{a} -> Lemma-MM3 {a} ;
92 Lemma-MM3 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in 102 Lemma-MM3 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
93 begin 103 begin
94 TMap μ a o TMap η ( FObj T a ) 104 TMap μ a o TMap η ( FObj T a )
95 ≈⟨⟩ 105 ≈⟨⟩
96 ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x )) 106 ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
97 ≈⟨ Lemma-MM31 ⟩ 107 ≈⟨ {!!} ⟩
98 ( λ x → x ) 108 ( λ x → x )
99 ≈⟨⟩ 109 ≈⟨⟩
100 Id {_} {_} {_} {A} (FObj T a) 110 Id {_} {_} {_} {A} (FObj T a)
101 ∎ 111 ∎
102 Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] 112 Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]