Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 719:a017ed40dd77

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Applicative law → Monoidal law begin
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Nov 2017 16:38:34 +0900
parents a41b2b9b0407
children 13cef2bfa5c8
comparison
equal deleted inserted replaced
718:f2e617dc2c21 719:a017ed40dd77
517 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) 517 pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
518 pure {a} x = FMap F ( λ y → x ) (unit mono) 518 pure {a} x = FMap F ( λ y → x ) (unit mono)
519 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b -- ** mono x y 519 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b -- ** mono x y
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 )
523 → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf )
524 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
525 Applicative→Monoidal F mf ismf = record {
526 MF = F
527 ; ψ = λ x → unit
528 ; isMonodailFunctor = record {
529 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } }
530 ; associativity = λ {a b c} → comm1 {a} {b} {c}
531 ; unitarity-idr = λ {a b} → comm2 {a} {b}
532 ; unitarity-idl = λ {a b} → comm3 {a} {b}
533 }
534 } where
535 open Monoidal
536 open IsMonoidal hiding ( _■_ ; _□_ )
537 M = MonoidalSets
538 isM = Monoidal.isMonoidal MonoidalSets
539 unit = Applicative.pure mf OneObj
540 _⊗_ : (x y : Obj Sets ) → Obj Sets
541 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
542 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
543 _□_ f g = FMap (m-bi M) ( f , g )
544 φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
545 φ x = Applicative.<*> mf (FMap F (λ j k → (j , k)) (proj₁ x )) (proj₂ x)
546 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
547 _<*>_ = Applicative.<*> mf
548 comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
549 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
550 comm00 {a} {b} {(f , g)} (x , y) = begin
551 ( FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ( φ (x , y) )
552 ≡⟨⟩
553 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y)
554 ≡⟨ {!!} ⟩
555 (FMap F (λ j k → f j , k) x) <*> (FMap F g y)
556 ≡⟨ {!!} ⟩
557 (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y)
558 ≡⟨⟩
559 φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) )
560 ∎
561 where
562 open Relation.Binary.PropositionalEquality.≡-Reasoning
563 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]
564 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
565 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
566 comm10 : {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ o Sets [ id1 Sets (FObj F a) □ φ o Iso.≅→ (mα-iso isM) ] ]) x ≡
567 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x
568 comm10 {x} {y} {f} ((a , b) , c ) = begin
569 {!!}
570 ≡⟨ {!!} ⟩
571 {!!}
572 ∎
573 where
574 open Relation.Binary.PropositionalEquality.≡-Reasoning
575 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ
576 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
577 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ]
578 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x )
579 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [
580 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
581 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x
582 comm20 {a} {b} (x , OneObj ) = begin
583 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ (( FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) ))
584 ≡⟨⟩
585 FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (Applicative.pure mf OneObj))
586 ≡⟨ ≡-cong ( λ k → FMap F proj₁ k) ( IsApplicative.interchange ismf ) ⟩
587 FMap F proj₁ ((Applicative.pure mf (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x))
588 ≡⟨ {!!} ⟩
589 x
590 ≡⟨⟩
591 Iso.≅→ (mρ-iso isM) (x , OneObj)
592 ∎
593 where
594 open Relation.Binary.PropositionalEquality.≡-Reasoning
595 comm2 : {a b : Obj Sets} → Sets [ Sets [
596 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
597 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
598 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x )
599 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [
600 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o
601 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x
602 comm30 {a} {b} ( OneObj , x) = begin
603 {!!}
604 ≡⟨ {!!} ⟩
605 {!!}
606 ∎
607 where
608 open Relation.Binary.PropositionalEquality.≡-Reasoning
609 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
610 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
611 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x )
612
613
522 614
523 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) 615 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
524 ( unit : FObj F One ) 616 ( unit : FObj F One )
525 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) ) 617 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) )
526 ( mono : IsHaskellMonoidalFunctor F unit φ ) 618 ( mono : IsHaskellMonoidalFunctor F unit φ )