Mercurial > hg > Members > kono > Proof > category

changeset 727:ea84cc6c1797

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
monoidal functor and applicative done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 26 Nov 2017 16:19:54 +0900
parents e663c63cdf41
children 3275be7cf62d
files monoidal.agda
diffstat 1 files changed, 5 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- 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  ⟩