Mercurial > hg > Members > kono > Proof > category

changeset 146:945f26ed12d5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 15 Aug 2013 03:34:00 +0900
parents 57df6cb8f253
children eabd1685139a
files HomReasoning.agda monoid-monad.agda
diffstat 2 files changed, 54 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Wed Aug 14 22:45:50 2013 +0900
+++ b/HomReasoning.agda	Thu Aug 15 03:34:00 2013 +0900
@@ -116,7 +116,7 @@
       →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
   nat η  =  IsNTrans.commute ( isNTrans η  )
 
-  infixr  2 _∎
+  infixr 2 _∎
   infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
   infix  1 begin_
 
@@ -136,12 +136,20 @@
            x ≈ y → y IsRelatedTo z → x IsRelatedTo z
   _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
 
+
+  _≈↑⟨_⟩_  : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → 
+           y ≈ x → y IsRelatedTo z → x IsRelatedTo z
+  _≈↑⟨_⟩_ _  x≈y (relTo y≈z) = relTo (trans-hom (sym x≈y) y≈z)
+
+  infixr 2 _≈↑⟨_⟩_ 
+
   _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y
   _ ≈⟨⟩ x∼y = x∼y
 
   _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x
   _∎ _ = relTo refl-hom
 
+
 -- an example
 
 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
--- a/monoid-monad.agda	Wed Aug 14 22:45:50 2013 +0900
+++ b/monoid-monad.agda	Thu Aug 15 03:34:00 2013 +0900
@@ -1,8 +1,7 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
-open import Category.Monoid
 open import Algebra
 open import Level
-module monoid-monad {c c₁ c₂ ℓ : Level} { Mono : Monoid c ℓ}  where
+module monoid-monad {c c₁ c₂ ℓ : Level}   where
 
 open import Algebra.Structures
 open import HomReasoning
@@ -13,7 +12,22 @@
 open import Relation.Binary.Core
 open import Relation.Binary
 
-open Monoid
+-- open Monoid
+open import Algebra.FunctionProperties using (Op₁; Op₂)
+
+
+record ≡-Monoid c : Set (suc c) where
+  infixl 7 _∙_
+  field
+    Carrier  : Set c
+    _∙_      : Op₂ Carrier
+    ε        : Carrier
+    isMonoid : IsMonoid _≡_ _∙_ ε
+  open IsMonoid isMonoid public
+
+postulate Mono : ≡-Monoid c
+open ≡-Monoid
+
 
 -- T : A → (M x A)
 
@@ -28,7 +42,7 @@
         } 
     } where
         cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} → 
-                   Sets [ f ≈ g ] → Sets [ map (λ x → x) f ≈ map (λ x → x) g ]
+                   Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier Mono) → x) f ≈ map (λ (x : Carrier Mono) → x) g ]
         cong1 _≡_.refl = _≡_.refl
 
 open Functor
@@ -77,30 +91,35 @@
 
 open NTrans
 
--- 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
-
---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 =  _≡_.refl
 
-Lemma-M-34 : { x : Carrier Mono  } -> _≈_ Mono ((_∙_ Mono (ε Mono)  x)) x 
-Lemma-M-34  {x} = ( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x
+Lemma-MM34 : { x : Carrier Mono  } -> ( (Mono ∙ ε Mono) x ≡ x  )
+Lemma-MM34  {x} = ( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x
+
+Lemma-MM35 : { x : Carrier Mono  } -> ((Mono ∙ x) (ε Mono))  ≡ x
+Lemma-MM35  {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-MM36 : { x y z : Carrier Mono } -> ((Mono ∙ (Mono ∙ x) y) z)  ≡ (_∙_ Mono  x (_∙_ Mono y z ) )
+Lemma-MM36  {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono ))  x y z
+
+-- We cannot prove this ...
+-- Lemma-MM38 :  ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x)  -> (( λ x -> f x)  ≡ (λ x -> g x) )
+-- Lemma-MM38 {x} {f} {g} eq  = {!!}
 
-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
+postulate Lemma-MM39 :  ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (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 ) 
 
-≡-to≈ : { f g : Carrier Mono } -> f ≡ g -> _≈_ Mono f g
-≡-to≈  _≡_.refl = IsEquivalence.refl (IsMonoid.isEquivalence (isMonoid Mono ) )
+Lemma-MM9  : ( \(x : Carrier Mono) -> ( Mono ∙ ε Mono ) x )  ≡ ( \(x : Carrier Mono) -> x ) 
+Lemma-MM9  = Lemma-MM39 Lemma-MM34
 
-Lemma-M-37 : { a x y : Set } ( f g : Set -> Carrier Mono ) -> ( _≈_ Mono ( f a ) ( g a) ) ->  ( f x , y ) ≡ ( g x , y )
-Lemma-M-37 f g eq =  ?
+Lemma-MM10 : ( \x ->   ((Mono ∙ x) (ε Mono)))  ≡ ( \x -> x ) 
+Lemma-MM10 = Lemma-MM39 Lemma-MM35
+
+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 = record {
@@ -117,7 +136,7 @@
                      TMap μ a o TMap η ( FObj T a )
                 ≈⟨⟩
                     ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
-                ≈⟨  cong ( \f -> ( \x ->  ( f (proj₁ x) ) , proj₂ x )) ( _≡_.refl )  ⟩
+                ≈⟨  cong ( \f -> ( \x ->  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
                     ( λ x → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
                     ( λ x → x )
@@ -130,7 +149,7 @@
                      TMap μ a o (FMap T (TMap η a ))
                 ≈⟨⟩
                     ( λ x → (Mono ∙ proj₁ x) (ε Mono) , proj₂ x )
-                ≈⟨  cong ( \f -> ( \x ->  ( f (proj₁ x) ) , proj₂ x )) ( _≡_.refl )  ⟩
+                ≈⟨  cong ( \f -> ( \x ->  ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 )  ⟩
                     ( λ x → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
                     ( λ x → x )
@@ -143,8 +162,9 @@
                       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)))  )) ⟩
-                ≈⟨ {!!} ⟩
+                ≈⟨ cong ( \f -> ( \x -> 
+                         (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x)))  )) ,  proj₂ (proj₂ (proj₂ x)) )
+                         )) Lemma-MM11  ⟩
                       ( λ x → (Mono ∙ proj₁ x) ((Mono ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
                 ≈⟨⟩
                       TMap μ a o FMap T (TMap μ a)