# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1514514739 -32400
# Node ID 60942538dc41d866529ea147742327d4cb10546b
# Parent  b7a774977345f5aa3401ed6d3f3d0bbfe652ef88
...

diff -r b7a774977345 -r 60942538dc41 README.txt
--- a/README.txt	Wed Dec 13 09:34:45 2017 +0900
+++ b/README.txt	Fri Dec 29 11:32:19 2017 +0900
@@ -21,7 +21,6 @@
     list-monoid-cat.agda
     list-nat.agda
     list-nat0.agda
-    maybe-monad.agda
     maybeCat.agda
     monoid-monad.agda
 
@@ -34,6 +33,8 @@
     adj-monad.agda
     comparison-em.agda
     comparison-functor.agda
+    maybe-monad.agda
+    maybeCat.agda
 
 -- Limit 
 
@@ -41,16 +42,28 @@
     universal-mapping.agda
     free-monoid.agda
     CatExponetial.agda
-    pullback.agda
+    pullback.agda                -- including limit from product and equalizer
     discrete.agda
     limit-to.agda
+    SetsCompleteness.agda
+
+-- Freyd Adjoint Functor Theorem
+
+    Comma.agda
+    Comma1.agda
+    freyd.agda
+    freyd1.agda
+    freyd2.agda
+
+-- Monoidal functor and Applicative
+
+    monoidal.agda                 -- Monoidal category and Functor
+    applicative.agda              -- Applicative functor is a monoidal functor
+    monad→monoidal.agda
 
 -- no yet finished
 
-    freyd.agda
-    Comma.agda
-    linton.agda
-
 -- repositories
 
    https://bitbucket.org/shinji_kono/category-exercise-in-agda/src
+
diff -r b7a774977345 -r 60942538dc41 applicative.agda
--- a/applicative.agda	Wed Dec 13 09:34:45 2017 +0900
+++ b/applicative.agda	Fri Dec 29 11:32:19 2017 +0900
@@ -315,7 +315,7 @@
 
 ----
 --
--- Monoidal laws imples Applicative laws
+-- Monoidal laws implies Applicative laws
 --
 
 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
diff -r b7a774977345 -r 60942538dc41 monad→monoidal.agda
--- a/monad→monoidal.agda	Wed Dec 13 09:34:45 2017 +0900
+++ b/monad→monoidal.agda	Fri Dec 29 11:32:19 2017 +0900
@@ -46,6 +46,38 @@
           open IsMonoidal
           id : { a : Obj (Sets {l}) } → a → a
           id x = x
+          natφ' : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d  }
+             → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
+          natφ' {a} {b} {c} {d} {x} {y} {f} {g} = monoidal.≡-cong ( λ h → h x ) ( begin
+                ( λ x → (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ・ (μ (Σ a (λ k → b))))  ( FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) x ))
+             ≈⟨⟩
+                (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy))  o (μ (Σ a (λ k → b)))) o  FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y)  
+             ≈⟨ car {_} {_} {_} {_} {_} {FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y)} ( nat (Monad.μ monad) ) ⟩
+                ( μ ( c * d)  o FMap F (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)))) o  FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y)  
+             ≈↑⟨ cdr {_} {_} {_} {_} {_} {μ ( c * d)} ( distr F ) ⟩
+                 μ ( c * d)  o FMap F (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o  (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) )
+             ≈⟨ cdr {_} {_} {_} {_} {_} {μ ( c * d)} (  begin
+                  FMap F (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o  (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) )
+                ≈⟨⟩
+                  FMap F (λ x₁ → (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y)) x₁)
+                ≈⟨ fcong F ( extensionality Sets ( λ x₁ →  monoidal.≡-cong ( λ h → h x₁ ) ( begin
+                       FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y )
+                    ≈⟨ {!!}  ⟩
+                        ( λ x₁ →  FMap F (λ g₁ → f x₁ , g₁)    (FMap F g y) )
+                    ∎ 
+                    ) ) )  ⟩
+                  FMap F (λ x₁ → FMap F (λ g₁ → f x₁ , g₁) (FMap F g y))
+                ≈⟨⟩
+                  FMap F ( (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) o f )
+                ≈⟨ distr F  ⟩
+                  FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) o (FMap F f )
+                ∎ 
+                ) ⟩
+                 μ ( c * d)  o (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) o (FMap F f ))
+             ≈⟨⟩
+                ( λ x →  μ  (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) (FMap F f x)))
+             ∎ ) where
+                  open ≈-Reasoning Sets hiding ( _o_ )
           natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d  }
              → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
           natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin
diff -r b7a774977345 -r 60942538dc41 monoid-monad.agda
--- a/monoid-monad.agda	Wed Dec 13 09:34:45 2017 +0900
+++ b/monoid-monad.agda	Fri Dec 29 11:32:19 2017 +0900
@@ -122,9 +122,12 @@
 Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z))  ≡ (λ x y z → ( _∙_ M  x (_∙_ M y z ) ))
 Lemma-MM11 = extensionality30 Lemma-MM36 
 
-MonoidMonad : Monad A T η μ 
+MonoidMonad : Monad A 
 MonoidMonad = record {
-       isMonad = record {
+       T = T 
+     ; η = η 
+     ; μ = μ 
+     ; isMonad = record {
            unity1 = Lemma-MM3 ;
            unity2 = Lemma-MM4 ;
            assoc  = Lemma-MM5 
@@ -181,7 +184,7 @@
 
 Lemma-MM12 =  Monad.join MonoidMonad (F m f) (F m' g)
 
-open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad}
+open import kleisli {_} {_} {_} {A} {T} {η} {μ} {Monad.isMonad MonoidMonad}
 
 -- nat-ε   TMap = λ a₁ → record { KMap = λ x → x }
 -- nat-η   TMap = λ a₁ → _,_ (ε,  M)