Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 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 6bc9d68898ef
comparison
equal deleted inserted replaced
726:e663c63cdf41 727:ea84cc6c1797
315 ≈-cong (refl , refl) = refl 315 ≈-cong (refl , refl) = refl
316 316
317 317
318 318
319 MonoidalSets : {c : Level} → Monoidal (Sets {c}) 319 MonoidalSets : {c : Level} → Monoidal (Sets {c})
320 MonoidalSets = record { 320 MonoidalSets {c} = record {
321 m-i = One ; 321 m-i = One {c} ;
322 m-bi = SetsTensorProduct ; 322 m-bi = SetsTensorProduct ;
323 isMonoidal = record { 323 isMonoidal = record {
324 mα-iso = record { ≅→ = mα→ ; ≅← = mα← ; iso→ = refl ; iso← = refl } ; 324 mα-iso = record { ≅→ = mα→ ; ≅← = mα← ; iso→ = refl ; iso← = refl } ;
325 mλ-iso = record { ≅→ = mλ→ ; ≅← = mλ← ; iso→ = extensionality Sets ( λ x → mλiso x ) ; iso← = refl } ; 325 mλ-iso = record { ≅→ = mλ→ ; ≅← = mλ← ; iso→ = extensionality Sets ( λ x → mλiso x ) ; iso← = refl } ;
326 mρ-iso = record { ≅→ = mρ→ ; ≅← = mρ← ; iso→ = extensionality Sets ( λ x → mρiso x ) ; iso← = refl } ; 326 mρ-iso = record { ≅→ = mρ→ ; ≅← = mρ← ; iso→ = extensionality Sets ( λ x → mρiso x ) ; iso← = refl } ;
520 <*> {a} {b} x y = FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ mono ( x , y )) 520 <*> {a} {b} x y = FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ mono ( x , y ))
521 521
522 Applicative→Monoidal : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F ) 522 Applicative→Monoidal : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F )
523 → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf ) 523 → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf )
524 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets 524 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
525 Applicative→Monoidal F mf ismf = record { 525 Applicative→Monoidal {l} F mf ismf = record {
526 MF = F 526 MF = F
527 ; ψ = λ x → unit 527 ; ψ = λ x → unit
528 ; isMonodailFunctor = record { 528 ; isMonodailFunctor = record {
529 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } } 529 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } }
530 ; associativity = λ {a b c} → comm1 {a} {b} {c} 530 ; associativity = λ {a b c} → comm1 {a} {b} {c}
738 ≡⟨ sym ( right comp ) ⟩ 738 ≡⟨ sym ( right comp ) ⟩
739 pure proj₁ <*> (((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k)) <*> x) 739 pure proj₁ <*> (((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k)) <*> x)
740 ≡⟨ sym comp ⟩ 740 ≡⟨ sym comp ⟩
741 ( ( pure _・_ <*> (pure proj₁ ) ) <*> ((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k))) <*> x 741 ( ( pure _・_ <*> (pure proj₁ ) ) <*> ((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k))) <*> x
742 ≡⟨ trans ( trans ( trans ( left ( left p*p)) ( left ( right (left p*p) ))) (left (right p*p) ) ) (left p*p) ⟩ 742 ≡⟨ trans ( trans ( trans ( left ( left p*p)) ( left ( right (left p*p) ))) (left (right p*p) ) ) (left p*p) ⟩
743 pure ( ( _・_ proj₁ ) ((_・_ ((λ f → f OneObj))) (λ j k → j , k))) <*> x 743 pure ( ( _・_ (proj₁ {l} {l})) ((_・_ ((λ f → f OneObj))) (λ j k → j , k))) <*> x
744 ≡⟨⟩ 744 ≡⟨⟩
745 pure id <*> x 745 pure id <*> x
746 ≡⟨ IsApplicative.identity ismf ⟩ 746 ≡⟨ IsApplicative.identity ismf ⟩
747 x 747 x
748 ≡⟨⟩ 748 ≡⟨⟩
765 ≡⟨ ( trans F→pure (right ( left F→pure )) ) ⟩ 765 ≡⟨ ( trans F→pure (right ( left F→pure )) ) ⟩
766 pure proj₂ <*> ((pure (λ j k → j , k) <*> (pure OneObj)) <*> x) 766 pure proj₂ <*> ((pure (λ j k → j , k) <*> (pure OneObj)) <*> x)
767 ≡⟨ sym comp ⟩ 767 ≡⟨ sym comp ⟩
768 ((pure _・_ <*> (pure proj₂)) <*> (pure (λ j k → j , k) <*> (pure OneObj))) <*> x 768 ((pure _・_ <*> (pure proj₂)) <*> (pure (λ j k → j , k) <*> (pure OneObj))) <*> x
769 ≡⟨ trans (trans (left (left p*p )) (left ( right p*p)) ) (left p*p) ⟩ 769 ≡⟨ trans (trans (left (left p*p )) (left ( right p*p)) ) (left p*p) ⟩
770 pure ((_・_ proj₂) ((λ j k → j , k) OneObj)) <*> x 770 pure ((_・_ (proj₂ {l}) )((λ (j : One {l}) (k : b ) → j , k) OneObj)) <*> x
771 ≡⟨⟩ 771 ≡⟨⟩
772 pure id <*> x 772 pure id <*> x
773 ≡⟨ IsApplicative.identity ismf ⟩ 773 ≡⟨ IsApplicative.identity ismf ⟩
774 x 774 x
775 ≡⟨⟩ 775 ≡⟨⟩