# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511680794 -32400
# Node ID ea84cc6c17975a659ab2e08778f3678943263bea
# Parent  e663c63cdf41c3332b84c5597a434d0cf27e502b
monoidal functor and applicative done

diff -r e663c63cdf41 -r ea84cc6c1797 monoidal.agda
--- a/monoidal.agda	Sun Nov 26 16:00:54 2017 +0900
+++ b/monoidal.agda	Sun Nov 26 16:19:54 2017 +0900
@@ -317,8 +317,8 @@
 
 
 MonoidalSets : {c : Level} → Monoidal (Sets {c})
-MonoidalSets = record {
-      m-i = One ;
+MonoidalSets {c} = record {
+      m-i = One {c} ;
       m-bi = SetsTensorProduct  ;
       isMonoidal = record {
               mα-iso  =  record { ≅→  =  mα→ ; ≅← =  mα← ; iso→  = refl ; iso← = refl } ;
@@ -522,7 +522,7 @@
 Applicative→Monoidal :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F )
    → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf ) 
    → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
-Applicative→Monoidal F mf ismf = record {
+Applicative→Monoidal {l} F mf ismf = record {
       MF = F
     ; ψ  = λ x → unit
     ; isMonodailFunctor = record {
@@ -740,7 +740,7 @@
                ≡⟨ sym  comp  ⟩
                  ( ( pure _・_   <*>  (pure proj₁ ) ) <*> ((pure _・_   <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k))) <*> x
                ≡⟨ trans ( trans ( trans ( left ( left p*p)) ( left ( right (left p*p) ))) (left (right p*p) )  ) (left p*p) ⟩
-                 pure ( ( _・_ proj₁ ) ((_・_  ((λ f → f OneObj))) (λ j k → j , k))) <*> x
+                 pure ( ( _・_ (proj₁ {l} {l})) ((_・_  ((λ f → f OneObj))) (λ j k → j , k))) <*> x
                ≡⟨⟩
                  pure id <*> x
                ≡⟨ IsApplicative.identity ismf  ⟩
@@ -767,7 +767,7 @@
                ≡⟨ sym comp ⟩
                   ((pure  _・_  <*>  (pure proj₂)) <*> (pure (λ j k → j , k) <*> (pure OneObj))) <*> x
                ≡⟨ trans (trans (left (left p*p )) (left ( right p*p)) ) (left p*p)  ⟩
-                  pure ((_・_  proj₂) ((λ j k → j , k) OneObj)) <*> x
+                  pure ((_・_  (proj₂ {l}) )((λ (j : One {l})  (k : b ) → j , k) OneObj)) <*> x
                ≡⟨⟩
                  pure id <*> x
                ≡⟨ IsApplicative.identity ismf  ⟩