diff src/monoid-monad.agda @ 949:ac53803b3b2a

reorganization for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 16:40:15 +0900 (2020-12-21)
parents monoid-monad.agda@bded2347efa4
children 9746e93a8c31
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/monoid-monad.agda	Mon Dec 21 16:40:15 2020 +0900
@@ -0,0 +1,201 @@
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Algebra
+open import Level
+open import Category.Sets
+module monoid-monad {c : Level} where
+
+open import Algebra.Structures
+open import HomReasoning
+open import cat-utility
+open import Category.Cat
+open import Data.Product
+open import Relation.Binary.Core
+open import Relation.Binary
+
+-- open Monoid
+open import Algebra.FunctionProperties using (Op₁; Op₂)
+
+open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
+
+
+record ≡-Monoid c : Set (suc c) where
+  infixl 7 _*_
+  field
+    Carrier  : Set c
+    _*_      : Op₂ Carrier
+    ε        : Carrier   -- id in Monoid
+    isMonoid : IsMonoid _≡_ _*_ ε
+
+postulate M : ≡-Monoid c
+open ≡-Monoid
+
+infixl 7 _∙_
+
+_∙_   : ( m m' : Carrier M ) → Carrier M
+_∙_ m m' = _*_ M m m'
+
+A = Sets {c}
+
+-- T : A → (M x A)
+
+T : Functor A A
+T = record {
+        FObj = λ a → (Carrier M) × a
+        ; FMap = λ f p → (proj₁ p , f (proj₂ p )) 
+        ; isFunctor = record {
+             identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
+             ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
+             ; ≈-cong = cong1
+        } 
+    } where
+        cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} → 
+                   Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier M) → x) f ≈ map (λ (x : Carrier M) → x) g ]
+        cong1 _≡_.refl = _≡_.refl
+
+open Functor
+
+Lemma-MM1 :  {a b : Obj A} {f : Hom A a b} →
+        A [ A [ FMap T f o (λ x → ε M , x) ] ≈
+        A [ (λ x → ε M , x) o f ] ]
+Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in 
+        begin
+             FMap T f o (λ x → ε M , x)
+        ≈⟨⟩
+             (λ x → ε M , x) o f
+        ∎
+
+-- η : a → (ε,a)
+η : NTrans  A A identityFunctor T
+η = record {
+       TMap = λ a → λ(x : a) → ( ε M , x ) ;
+       isNTrans = record {
+            commute = Lemma-MM1
+       }
+  }
+
+-- μ : (m,(m',a)) → (m*m,a)
+
+muMap : (a : Obj A  ) → FObj T ( FObj T a ) → Σ (Carrier M) (λ x → a )
+muMap a ( m , ( m' , x ) ) = ( m ∙ m' ,  x )
+
+Lemma-MM2 :  {a b : Obj A} {f : Hom A a b} →
+        A [ A [ FMap T f o (λ x → muMap a x) ] ≈
+        A [ (λ x → muMap b x) o FMap (T ○ T) f ] ]
+Lemma-MM2 {a} {b} {f} =  let open ≈-Reasoning A renaming ( _o_ to _*_ ) in                                                       
+        begin
+             FMap T f o (λ x → muMap a x)
+        ≈⟨⟩
+             (λ x → muMap b x) o FMap (T ○ T) f
+        ∎
+
+μ : NTrans  A A ( T ○ T ) T
+μ = record {
+       TMap = λ a → λ x  → muMap a x ; 
+       isNTrans = record {
+            commute = λ{a} {b} {f} → Lemma-MM2 {a} {b} {f}
+       }
+  }
+
+open NTrans
+
+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-MM34 : ∀( x : Carrier M  ) → ε M ∙ x ≡ x  
+Lemma-MM34  x = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
+
+Lemma-MM35 : ∀( x : Carrier M  ) → x ∙ ε M ≡ x
+Lemma-MM35  x = ( proj₂  ( IsMonoid.identity ( isMonoid M )) ) x
+
+Lemma-MM36 : ∀( x y z : Carrier M ) → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z ) 
+Lemma-MM36  x y z = ( IsMonoid.assoc ( isMonoid M ))  x y z
+
+-- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
+import Relation.Binary.PropositionalEquality
+-- postulate extensionality : { a b : Obj A } {f g : Hom A a b } →  Relation.Binary.PropositionalEquality.Extensionality c c
+postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c
+
+-- Multi Arguments Functional Extensionality
+extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → 
+               (∀ x y z  → f x y z ≡ g x y z )  → ( f ≡ g ) 
+extensionality30 eq = extensionality ( λ x → extensionality ( λ y → extensionality (eq x y) ) )
+
+Lemma-MM9  :  (λ(x : Carrier M) → ( ε M ∙ x ))  ≡ ( λ(x : Carrier M) → x  )
+Lemma-MM9  = extensionality Lemma-MM34
+
+Lemma-MM10 : ( λ x →   (x ∙ ε M))  ≡ ( λ x → x ) 
+Lemma-MM10  = extensionality Lemma-MM35
+
+Lemma-MM11 : (λ x y z → ((x ∙ y ) ∙ z))  ≡ (λ x y z → ( x ∙ (y ∙ z ) ))
+Lemma-MM11 = extensionality30 Lemma-MM36 
+
+MonoidMonad : Monad A 
+MonoidMonad = record {
+       T = T 
+     ; η = η 
+     ; μ = μ 
+     ; isMonad = record {
+           unity1 = Lemma-MM3 ;
+           unity2 = Lemma-MM4 ;
+           assoc  = Lemma-MM5 
+       }  
+   } where
+       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 (A) renaming ( _o_ to _*_ ) in
+                begin
+                     TMap μ a o TMap η ( FObj T a )
+                ≈⟨⟩
+                    ( λ x →   ε M ∙ (proj₁ x) , proj₂ x )
+                ≈⟨  cong ( λ f → ( λ x →  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
+                    ( λ (x : FObj T a) → (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 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
+                begin
+                     TMap μ a o (FMap T (TMap η a ))
+                ≈⟨⟩
+                    ( λ x → ( proj₁ x ∙ (ε M) , proj₂ x ))
+                ≈⟨  cong ( λ f → ( λ x →  ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 )  ⟩
+                    ( λ 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 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
+                begin
+                      TMap μ a o TMap μ ( FObj T a ) 
+                ≈⟨⟩
+                      ( λ x → (proj₁ x) ∙ (proj₁ (proj₂ x)) ∙ (proj₁ (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 → ( proj₁ x) ∙(( proj₁ (proj₂ x)) ∙ (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
+                ≈⟨⟩
+                      TMap μ a o FMap T (TMap μ a)
+                ∎
+
+
+F  : (m : Carrier M) → { a b : Obj A } → ( f : a → b ) → Hom A a ( FObj T b )
+F m {a} {b} f =  λ (x : a ) → ( m , ( f x) )
+
+postulate m m' : Carrier M
+postulate a b c' : Obj A 
+postulate f :  b → c'
+postulate g :  a → b
+
+Lemma-MM12 =  Monad.join MonoidMonad (F m f) (F m' g)
+
+open import kleisli {_} {_} {_} {A} {T} {η} {μ} {Monad.isMonad MonoidMonad}
+
+-- nat-ε   TMap = λ a₁ → record { KMap = λ x → x }
+-- nat-η   TMap = λ a₁ → _,_ (ε,  M)
+-- U_T     Functor Kleisli A
+-- U_T     FObj = λ B → Σ (Carrier M) (λ x → B)     FMap = λ {a₁} {b₁} f₁ x → ( proj₁ x ∙ (proj₁ (KMap f₁ (proj₂ x)))  , proj₂ (KMap f₁ (proj₂ x))
+-- F_T     Functor A Kleisli 
+-- F_T     FObj = λ a₁ → a₁                         FMap = λ {a₁} {b₁} f₁ → record { KMap = λ x → ε M , f₁ x }