Mercurial > hg > Members > kono > Proof > category

changeset 148:6e80e1aaa8b9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no yellow on monoid monad
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 15 Aug 2013 11:45:24 +0900
parents eabd1685139a
children 2f68a9e0167b
files monoid-monad.agda
diffstat 1 files changed, 11 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/monoid-monad.agda	Thu Aug 15 04:46:22 2013 +0900
+++ b/monoid-monad.agda	Thu Aug 15 11:45:24 2013 +0900
@@ -31,7 +31,7 @@
 
 -- T : A → (M x A)
 
-T : Functor (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ })
+T : Functor (Sets {c}) (Sets {c})
 T = record {
         FObj = \a → (Carrier Mono) × a
         ; FMap = \f → map ( \x → x ) f
@@ -58,7 +58,7 @@
         ∎
 
 -- a → (ε,a)
-η : NTrans  (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) identityFunctor T
+η : NTrans  (Sets {c}) (Sets {c}) identityFunctor T
 η = record {
        TMap = \a → \(x : a) → ( ε Mono , x ) ;
        isNTrans = record {
@@ -81,7 +81,7 @@
              (λ x → muMap b x) o FMap (T ○ T) f
         ∎
 
-μ : NTrans  (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ( T ○ T ) T
+μ : NTrans  (Sets {c}) (Sets {c}) ( T ○ T ) T
 μ = record {
        TMap = \a → \x  → muMap a x ; 
        isNTrans = record {
@@ -108,10 +108,10 @@
 -- Lemma-MM38 {x} {f} {g} eq  = {!!}
 
 -- Functional Extensionarity 
-postulate Lemma-MM39 : {x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x)  -> ( f ≡ g ) 
+postulate Lemma-MM39 : {f g : Carrier Mono -> Carrier Mono } -> (∀ {x} -> (f x ≡ g x))  -> ( f ≡ g ) 
 
-postulate Lemma-MM40 :  ∀{x y z : Carrier Mono } {f g : Carrier Mono -> Carrier Mono -> Carrier Mono -> Carrier Mono } -> 
-               (f x y z ≡ g x y z )  -> ( f ≡ g ) 
+postulate Lemma-MM40 :   {f g : Carrier Mono -> Carrier Mono -> Carrier Mono -> Carrier Mono } -> 
+               (∀{x y z} -> f x y z ≡ g x y z )  -> ( f ≡ g ) 
 
 Lemma-MM9  : ( \(x : Carrier Mono) -> ( Mono ∙ ε Mono ) x )  ≡ ( \(x : Carrier Mono) -> x ) 
 Lemma-MM9  = Lemma-MM39 Lemma-MM34
@@ -122,22 +122,22 @@
 Lemma-MM11 : (\x y z -> ((Mono ∙ (Mono ∙ x) y) z))  ≡ (\x y z -> ( _∙_ Mono  x (_∙_ Mono y z ) ))
 Lemma-MM11 = Lemma-MM40 Lemma-MM36 
 
-MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ 
+MonoidMonad : Monad (Sets {c}) T η μ 
 MonoidMonad = record {
        isMonad = record {
-           unity1 =  \{a} -> Lemma-MM3 {a} ;
+           unity1 = Lemma-MM3 ;
            unity2 = Lemma-MM4 ;
-           assoc = Lemma-MM5 
+           assoc  = Lemma-MM5 
        }  
    } where
-       A = Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ } 
+       A = Sets {c} 
        Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
        Lemma-MM3 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
                 begin
                      TMap μ a o TMap η ( FObj T a )
                 ≈⟨⟩
                     ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
-                ≈⟨  cong ( \f -> ( \(x : FObj T a ) ->  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
+                ≈⟨  cong ( \f -> ( \x ->  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
                     ( λ (x : FObj T a) → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
                     ( λ x → x )