Mercurial > hg > Members > kono > Proof > category

changeset 144:0948df8c88b8

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 Wed, 14 Aug 2013 10:26:45 +0900
parents bbaaca9b21ce
children 57df6cb8f253
files HomReasoning.agda monoid-monad.agda
diffstat 2 files changed, 47 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Tue Aug 13 18:07:27 2013 +0900
+++ b/HomReasoning.agda	Wed Aug 14 10:26:45 2013 +0900
@@ -81,8 +81,8 @@
 --  ≈-≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≈ y ) → x ≡ y
 --  ≈-≡  x≈y = irr x≈y
   ≡-cong : { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  →
-             a ≡ b  → (f : Hom B x y → Hom A x' y' ) →  f a  ≈  f b
-  ≡-cong refl f =  ≡-≈ refl
+             (f : Hom B x y → Hom A x' y' )  → a ≡ b →  f a  ≈  f b
+  ≡-cong f refl =  ≡-≈ refl
 
 --  cong-≈ :  { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  → 
 --             B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) →  f a ≈ f b
--- a/monoid-monad.agda	Tue Aug 13 18:07:27 2013 +0900
+++ b/monoid-monad.agda	Wed Aug 14 10:26:45 2013 +0900
@@ -31,12 +31,14 @@
                    Sets [ f ≈ g ] → Sets [ map (λ x → x) f ≈ map (λ x → x) g ]
         cong1 _≡_.refl = _≡_.refl
 
+open Functor
+
 Lemma-MM1 :  {a b : Obj Sets} {f : Hom Sets a b} →
-        Sets [ Sets [ Functor.FMap T f o (λ x → ε Mono , x) ] ≈
+        Sets [ Sets [ FMap T f o (λ x → ε Mono , x) ] ≈
         Sets [ (λ x → ε Mono , x) o f ] ]
 Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in 
         begin
-             Functor.FMap T f o (λ x → ε Mono , x)
+             FMap T f o (λ x → ε Mono , x)
         ≈⟨⟩
              (λ x → ε Mono , x) o f
         ∎
@@ -52,8 +54,6 @@
 
 -- (m,(m',a)) → (m*m,a)
 
-open Functor
-
 muMap : (a : Obj Sets  ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a )
 muMap a ( m , ( m' , x ) ) = ( _∙_ Mono m  m'  ,  x )
 
@@ -77,18 +77,28 @@
 
 open NTrans
 
---Lemma-MM32 :  ∀{ℓ} {a : Set ℓ } -> {f g : a -> a } -> {x : a } -> ( f ≡ g ) -> ( ( λ x → f x )  ≡ ( λ x → g x ) )
---Lemma-MM32 eq = cong ( \f -> \x -> f x  ) eq
+-- Lemma-MM32 :  ∀{ℓ} {a : Set ℓ } -> {f g : a -> a } -> {x : a } -> (  _≈_ Mono f  g ) -> ( ( λ x → f x )  ≡ ( λ x → g x ) )
+-- Lemma-MM32 eq = cong ( \f -> \x -> f x  ) eq
 
---Lemma-MM31 : ( a : Obj ( Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ) -> {x : FObj T a } →  (((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ) ≡  x )
---Lemma-MM31 a = {!!}
+--cong-≈ :  { a b : Carrier Mono }  → (f : Carrier Mono  -> Carrier Mono ) →   
+--              _≈_ Mono a b  → _≈_ Mono (f a) (f b) 
+--cong-≈ f eq = {!!}
 
-Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b}  {x :  Σ A B } →  (((proj₁ x) , proj₂ x ) ≡  x )
+Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b}  {x :  Σ A B } →  (((proj₁ x) , proj₂ x ) ≡ x )
 Lemma-MM33 =  _≡_.refl
 
 Lemma-M-34 : { x : Carrier Mono  } -> _≈_ Mono ((_∙_ Mono (ε Mono)  x)) x 
 Lemma-M-34  {x} = ( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x
 
+Lemma-M-35 : { x : Carrier Mono  } -> _≈_ Mono ((_∙_ Mono x (ε Mono))) x 
+Lemma-M-35  {x} = ( proj₂  ( IsMonoid.identity ( isMonoid Mono )) ) x
+
+Lemma-M-36 : { x y z : Carrier Mono } -> _≈_ Mono (_∙_ Mono  (_∙_ Mono  x y ) z ) (_∙_ Mono  x (_∙_ Mono y z ) )
+Lemma-M-36  {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono ))  x y z
+
+≡-to≈ : { f g : Carrier Mono } -> f ≡ g -> _≈_ Mono f g
+≡-to≈  _≡_.refl = IsEquivalence.refl (IsMonoid.isEquivalence (isMonoid Mono ) )
+
 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ 
 MonoidMonad = record {
        isMonad = record {
@@ -104,15 +114,38 @@
                      TMap μ a o TMap η ( FObj T a )
                 ≈⟨⟩
                     ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
-                ≈⟨ {!!} ⟩
+                ≈⟨  cong ( \f -> ( \x ->  ( f (proj₁ x) ) , proj₂ x )) ( _≡_.refl )  ⟩
+                    ( λ x → (proj₁ x) , proj₂ x )
+                ≈⟨⟩
                     ( λ x → x )
                 ≈⟨⟩
                      Id {_} {_} {_} {A} (FObj T a)
                 ∎
        Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-       Lemma-MM4 = {!!}
+       Lemma-MM4 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
+                begin
+                     TMap μ a o (FMap T (TMap η a ))
+                ≈⟨⟩
+                    ( λ x → (Mono ∙ proj₁ x) (ε Mono) , proj₂ x )
+                ≈⟨  cong ( \f -> ( \x ->  ( f (proj₁ x) ) , proj₂ x )) ( _≡_.refl )  ⟩
+                    ( λ x → (proj₁ x) , proj₂ x )
+                ≈⟨⟩
+                    ( λ x → x )
+                ≈⟨⟩
+                     Id {_} {_} {_} {A} (FObj T a)
+                ∎
        Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
-       Lemma-MM5 = {!!}
+       Lemma-MM5 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
+                begin
+                      TMap μ a o TMap μ ( FObj T a ) 
+                ≈⟨⟩
+                      ( λ x → (Mono ∙ (Mono ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x)))
+                -- ≈⟨ (\x ->  Lemma-M-36 ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x)))  )) ⟩
+                ≈⟨ ? ⟩
+                      ( λ x → (Mono ∙ proj₁ x) ((Mono ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
+                ≈⟨⟩
+                      TMap μ a o FMap T (TMap μ a)
+                ∎