Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 768:9bcdbfbaaa39

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 12 Dec 2017 10:25:59 +0900
parents c30ca91f3a76
children 43138aead09b
comparison
equal deleted inserted replaced
767:0f8e3b962c13 768:9bcdbfbaaa39
492 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o 492 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
493 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] 493 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
494 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x ) 494 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x )
495 495
496 496
497 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
498 _・_ f g = λ x → f ( g x )
499
500 record IsApplicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
501 ( pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) )
502 ( _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b )
503 : Set (suc (suc c₁)) where
504 field
505 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u
506 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
507 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w)
508 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x)
509 interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
510 -- from http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
511
512 record Applicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
513 : Set (suc (suc c₁)) where
514 field
515 pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
516 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
517 isApplicative : IsApplicative F pure <*>
518
519 ------
520 --
521 -- Appllicative Functor is a Monoidal Functor
522 --
523
524 Applicative→Monoidal : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F )
525 → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf )
526 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
527 Applicative→Monoidal {l} F mf ismf = record {
528 MF = F
529 ; ψ = λ x → unit
530 ; isMonodailFunctor = record {
531 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } }
532 ; associativity = λ {a b c} → comm1 {a} {b} {c}
533 ; unitarity-idr = λ {a b} → comm2 {a} {b}
534 ; unitarity-idl = λ {a b} → comm3 {a} {b}
535 }
536 } where
537 open Monoidal
538 open IsMonoidal hiding ( _■_ ; _□_ )
539 M = MonoidalSets
540 isM = Monoidal.isMonoidal MonoidalSets
541 unit = Applicative.pure mf OneObj
542 _⊗_ : (x y : Obj Sets ) → Obj Sets
543 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
544 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
545 _□_ f g = FMap (m-bi M) ( f , g )
546 φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
547 φ x = Applicative.<*> mf (FMap F (λ j k → (j , k)) (proj₁ x )) (proj₂ x)
548 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
549 _<*>_ = Applicative.<*> mf
550 left : {a b : Obj Sets} → {x y : FObj F ( a → b )} → {h : FObj F a } → ( x ≡ y ) → x <*> h ≡ y <*> h
551 left {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k <*> h ) eq
552 right : {a b : Obj Sets} → {h : FObj F ( a → b )} → {x y : FObj F a } → ( x ≡ y ) → h <*> x ≡ h <*> y
553 right {_} {_} {h} {_} {_} eq = ≡-cong ( λ k → h <*> k ) eq
554 id : { a : Obj Sets } → a → a
555 id x = x
556 pure : {a : Obj Sets } → Hom Sets a ( FObj F a )
557 pure a = Applicative.pure mf a
558 -- special case
559 F→pureid : {a b : Obj Sets } → (x : FObj F a ) → FMap F id x ≡ pure id <*> x
560 F→pureid {a} {b} x = sym ( begin
561 pure id <*> x
562 ≡⟨ IsApplicative.identity ismf ⟩
563 x
564 ≡⟨ ≡-cong ( λ k → k x ) (sym ( IsFunctor.identity (isFunctor F ) )) ⟩ FMap F id x
565 ∎ )
566 where
567 open Relation.Binary.PropositionalEquality
568 open Relation.Binary.PropositionalEquality.≡-Reasoning
569 F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } → FMap F f x ≡ pure f <*> x
570 F→pure {a} {b} {f} {x} = sym ( begin
571 pure f <*> x
572 ≡⟨ ≡-cong ( λ k → k x ) (UniquenessOfFunctor Sets Sets F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x → IsApplicative.identity ismf ))) ⟩
573 FMap F f x
574 ∎ )
575 where
576 open Relation.Binary.PropositionalEquality
577 open Relation.Binary.PropositionalEquality.≡-Reasoning
578 p*p : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x)
579 p*p = IsApplicative.homomorphism ismf
580 comp = IsApplicative.composition ismf
581 inter = IsApplicative.interchange ismf
582 pureAssoc : {a b c : Obj Sets } ( f : b → c ) ( g : a → b ) ( h : FObj F a ) → pure f <*> ( pure g <*> h ) ≡ pure ( f ・ g ) <*> h
583 pureAssoc f g h = trans ( trans (sym comp) (left (left p*p) )) ( left p*p )
584 where
585 open Relation.Binary.PropositionalEquality
586 comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
587 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
588 comm00 {a} {b} {(f , g)} (x , y) = begin
589 ( FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ( φ (x , y) )
590 ≡⟨⟩
591 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y)
592 ≡⟨⟩
593 FMap F (map f g) ((FMap F (λ j k → j , k) x) <*> y)
594 ≡⟨ F→pure ⟩
595 (pure (map f g) <*> (FMap F (λ j k → j , k) x <*> y))
596 ≡⟨ right ( left F→pure ) ⟩
597 (pure (map f g)) <*> ((pure (λ j k → j , k) <*> x) <*> y)
598 ≡⟨ sym ( IsApplicative.composition ismf ) ⟩
599 (( pure _・_ <*> (pure (map f g))) <*> (pure (λ j k → j , k) <*> x)) <*> y
600 ≡⟨ left ( sym ( IsApplicative.composition ismf )) ⟩
601 ((( pure _・_ <*> (( pure _・_ <*> (pure (map f g))))) <*> pure (λ j k → j , k)) <*> x) <*> y
602 ≡⟨ trans ( trans (left ( left (left (right p*p )))) ( left ( left ( left p*p)))) (left (left p*p)) ⟩
603 (pure (( _・_ (( _・_ ((map f g))))) (λ j k → j , k)) <*> x) <*> y
604 ≡⟨⟩
605 (pure (λ j k → f j , g k) <*> x) <*> y
606 ≡⟨⟩
607 ( pure ((_・_ (( _・_ ( ( λ h → h g ))) ( _・_ ))) ((λ j k → f j , k))) <*> x ) <*> y
608 ≡⟨ sym ( trans (left (left (left p*p))) (left ( left p*p)) ) ⟩
609 ((((pure _・_ <*> pure ((λ h → h g) ・ _・_)) <*> pure (λ j k → f j , k)) <*> x) <*> y)
610 ≡⟨ sym (trans ( left ( left ( left (right (left p*p) )))) (left ( left (left (right p*p ))))) ⟩
611 (((pure _・_ <*> (( pure _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ ))) <*> (pure (λ j k → f j , k))) <*> x ) <*> y
612 ≡⟨ left ( ( IsApplicative.composition ismf )) ⟩
613 ((( pure _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ )) <*> (pure (λ j k → f j , k) <*> x )) <*> y
614 ≡⟨ left (IsApplicative.composition ismf ) ⟩
615 ( pure ( λ h → h g ) <*> ( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) ) <*> y
616 ≡⟨ left (sym (IsApplicative.interchange ismf )) ⟩
617 (( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) <*> pure g) <*> y
618 ≡⟨ IsApplicative.composition ismf ⟩
619 (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y)
620 ≡⟨ sym ( trans (left F→pure ) ( right F→pure ) ) ⟩
621 (FMap F (λ j k → f j , k) x) <*> (FMap F g y)
622 ≡⟨ ≡-cong ( λ k → k x <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F )) ⟩
623 (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y)
624 ≡⟨⟩
625 φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) )
626 ∎
627 where
628 open Relation.Binary.PropositionalEquality
629 open Relation.Binary.PropositionalEquality.≡-Reasoning
630 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]
631 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
632 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
633 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 ≡
634 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x
635 comm10 {x} {y} {f} ((a , b) , c ) = begin
636 φ (( id □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
637 ≡⟨⟩
638 (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c)
639 ≡⟨ trans (left F→pure) (right (left F→pure) ) ⟩
640 (pure (λ j k → j , k) <*> a) <*> ( (pure (λ j k → j , k) <*> b) <*> c)
641 ≡⟨ sym comp ⟩
642 ( ( pure _・_ <*> (pure (λ j k → j , k) <*> a)) <*> (pure (λ j k → j , k) <*> b)) <*> c
643 ≡⟨ sym ( left comp ) ⟩
644 (( ( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k) <*> a))) <*> (pure (λ j k → j , k))) <*> b) <*> c
645 ≡⟨ sym ( left ( left ( left (right comp )))) ⟩
646 (( ( pure _・_ <*> (( (pure _・_ <*> pure _・_ ) <*> (pure (λ j k → j , k))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c
647 ≡⟨ trans (left ( left (left ( right (left ( left p*p )))))) (left ( left ( left (right (left p*p))))) ⟩
648 (( ( pure _・_ <*> ((pure ((_・_ ( _・_ )) ((λ j k → j , k)))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c
649 ≡⟨ sym (left ( left ( left comp ) )) ⟩
650 (((( ( pure _・_ <*> (pure _・_ )) <*> (pure ((_・_ ( _・_ )) ((λ j k → j , k))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c
651 ≡⟨ trans (left ( left ( left (left (left p*p))))) (left ( left ( left (left p*p )))) ⟩
652 ((((pure ( ( _・_ (_・_ )) (((_・_ ( _・_ )) ((λ j k → j , k)))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c
653 ≡⟨⟩
654 ((((pure (λ f g x y → f , g x y)) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c
655 ≡⟨ left ( left inter ) ⟩
656 (((pure (λ f → f (λ j k → j , k))) <*> ((pure (λ f g x y → f , g x y)) <*> a) ) <*> b) <*> c
657 ≡⟨ sym ( left ( left comp )) ⟩
658 (((( pure _・_ <*> (pure (λ f → f (λ j k → j , k)))) <*> (pure (λ f g x y → f , g x y))) <*> a ) <*> b) <*> c
659 ≡⟨ trans (left ( left (left (left p*p) ))) (left (left (left p*p ) )) ⟩
660 ((pure (( _・_ (λ f → f (λ j k → j , k))) (λ f g x y → f , g x y)) <*> a ) <*> b) <*> c
661 ≡⟨⟩
662 (((pure (λ f g h → f , g , h)) <*> a) <*> b) <*> c
663 ≡⟨⟩
664 ((pure ((_・_ ((_・_ ((_・_ ( (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc)))))))
665 (( _・_ ( _・_ ((λ j k → j , k)))) (λ j k → j , k))) <*> a) <*> b) <*> c
666 ≡⟨ sym (trans ( left ( left ( left (left (right (right p*p))) ) )) (trans (left (left( left (left (right p*p)))))
667 (trans (left (left (left (left p*p)))) (trans ( left (left (left (right (left (right p*p ))))))
668 (trans (left (left (left (right (left p*p))))) (trans (left (left (left (right p*p)))) (left (left (left p*p)))) ) ) )
669 ) ) ⟩
670 ((((pure _・_ <*> ((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) <*>
671 (( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k))) <*> a) <*> b) <*> c
672 ≡⟨ left (left comp ) ⟩
673 (((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))) <*>
674 ((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a)) <*> b) <*> c
675 ≡⟨ left comp ⟩
676 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*>
677 (((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a) <*> b)) <*> c
678 ≡⟨ left ( right (left comp )) ⟩
679 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*>
680 ((( pure _・_ <*> (pure (λ j k → j , k))) <*> (pure (λ j k → j , k) <*> a)) <*> b)) <*> c
681 ≡⟨ left ( right comp ) ⟩
682 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*>
683 (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b))) <*> c
684 ≡⟨ comp ⟩
685 pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) <*> ( (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b)) <*> c)
686 ≡⟨ sym ( trans ( trans F→pure (right (left F→pure ))) ( right ( left (right (left F→pure ))))) ⟩
687 FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) ( (FMap F (λ j k → j , k) ( (FMap F (λ j k → j , k) a) <*> b)) <*> c)
688 ≡⟨⟩
689 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c)))
690 ∎
691 where
692 open Relation.Binary.PropositionalEquality
693 open Relation.Binary.PropositionalEquality.≡-Reasoning
694 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ
695 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
696 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ]
697 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x )
698 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [
699 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
700 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x
701 comm20 {a} {b} (x , OneObj ) = begin
702 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ (( FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) ))
703 ≡⟨⟩
704 FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (pure OneObj))
705 ≡⟨ ≡-cong ( λ k → FMap F proj₁ k) ( IsApplicative.interchange ismf ) ⟩
706 FMap F proj₁ ((pure (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x))
707 ≡⟨ ( trans F→pure (right ( right F→pure )) ) ⟩
708 pure proj₁ <*> ((pure (λ f → f OneObj)) <*> (pure (λ j k → j , k) <*> x))
709 ≡⟨ sym ( right comp ) ⟩
710 pure proj₁ <*> (((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k)) <*> x)
711 ≡⟨ sym comp ⟩
712 ( ( pure _・_ <*> (pure proj₁ ) ) <*> ((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k))) <*> x
713 ≡⟨ trans ( trans ( trans ( left ( left p*p)) ( left ( right (left p*p) ))) (left (right p*p) ) ) (left p*p) ⟩
714 pure ( ( _・_ (proj₁ {l} {l})) ((_・_ ((λ f → f OneObj))) (λ j k → j , k))) <*> x
715 ≡⟨⟩
716 pure id <*> x
717 ≡⟨ IsApplicative.identity ismf ⟩
718 x
719 ≡⟨⟩
720 Iso.≅→ (mρ-iso isM) (x , OneObj)
721 ∎
722 where
723 open Relation.Binary.PropositionalEquality
724 open Relation.Binary.PropositionalEquality.≡-Reasoning
725 comm2 : {a b : Obj Sets} → Sets [ Sets [
726 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
727 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
728 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x )
729 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [
730 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o
731 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x
732 comm30 {a} {b} ( OneObj , x) = begin
733 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) )
734 ≡⟨⟩
735 FMap F proj₂ ((FMap F (λ j k → j , k) (pure OneObj)) <*> x)
736 ≡⟨ ( trans F→pure (right ( left F→pure )) ) ⟩
737 pure proj₂ <*> ((pure (λ j k → j , k) <*> (pure OneObj)) <*> x)
738 ≡⟨ sym comp ⟩
739 ((pure _・_ <*> (pure proj₂)) <*> (pure (λ j k → j , k) <*> (pure OneObj))) <*> x
740 ≡⟨ trans (trans (left (left p*p )) (left ( right p*p)) ) (left p*p) ⟩
741 pure ((_・_ (proj₂ {l}) )((λ (j : One {l}) (k : b ) → j , k) OneObj)) <*> x
742 ≡⟨⟩
743 pure id <*> x
744 ≡⟨ IsApplicative.identity ismf ⟩
745 x
746 ≡⟨⟩
747 Iso.≅→ (mλ-iso isM) ( OneObj , x )
748 ∎
749 where
750 open Relation.Binary.PropositionalEquality
751 open Relation.Binary.PropositionalEquality.≡-Reasoning
752 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
753 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
754 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x )
755
756 ----
757 --
758 -- Monoidal laws imples Applicative laws
759 --
760
761 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
762 ( Mono : HaskellMonoidalFunctor F )
763 → Applicative F
764 HaskellMonoidal→Applicative {c₁} F Mono = record {
765 pure = pure ;
766 <*> = _<*>_ ;
767 isApplicative = record {
768 identity = identity
769 ; composition = composition
770 ; homomorphism = homomorphism
771 ; interchange = interchange
772 }
773 }
774 where
775 unit : FObj F One
776 unit = HaskellMonoidalFunctor.unit Mono
777 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) )
778 φ = HaskellMonoidalFunctor.φ Mono
779 mono : IsHaskellMonoidalFunctor F unit φ
780 mono = HaskellMonoidalFunctor.isHaskellMonoidalFunctor Mono
781 id : { a : Obj Sets } → a → a
782 id x = x
783 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct
784 isM = Monoidal.isMonoidal MonoidalSets
785 pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
786 pure {a} x = FMap F ( λ y → x ) (unit )
787 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
788 _<*>_ {a} {b} x y = FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ ( x , y ))
789 -- right does not work right it makes yellows. why?
790 -- right : {n : Level} { a b : Set n} → { x y : a } { h : a → b } → ( x ≡ y ) → h x ≡ h y
791 -- right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq
792 left : {n : Level} { a b : Set n} → { x y : a → b } { h : a } → ( x ≡ y ) → x h ≡ y h
793 left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq
794 open Relation.Binary.PropositionalEquality
795 FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d }
796 { f : Hom Sets (c * d) e }
797 { x : FObj F a } { y : FObj F b }
798 → FMap F f ( φ ( FMap F g x , FMap F h y ) ) ≡ FMap F ( f o map g h ) ( φ ( x , y ) )
799 FφF→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin
800 FMap F ( f o map g h ) ( φ ( x , y ) )
801 ≡⟨ ≡-cong ( λ k → k ( φ ( x , y ))) ( IsFunctor.distr (isFunctor F) ) ⟩
802 FMap F f (( FMap F ( map g h ) ) ( φ ( x , y )))
803 ≡⟨ ≡-cong ( λ k → FMap F f k ) ( IsHaskellMonoidalFunctor.natφ mono ) ⟩
804 FMap F f ( φ ( FMap F g x , FMap F h y ) )
805 ∎ )
806 where
807 open Relation.Binary.PropositionalEquality.≡-Reasoning
808 u→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u
809 u→F {a} {u} = sym ( ≡-cong ( λ k → k u ) ( IsFunctor.identity ( isFunctor F ) ) )
810 φunitr : {a : Obj Sets } {u : FObj F a} → φ ( unit , u) ≡ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
811 φunitr {a} {u} = sym ( begin
812 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
813 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩
814 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) ( φ ( unit , u) ) )
815 ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩
816 (FMap F ( (Iso.≅← (IsMonoidal.mλ-iso isM)) o (Iso.≅→ (IsMonoidal.mλ-iso isM)))) ( φ ( unit , u) )
817 ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( unit , u) )) (Iso.iso→ ( (IsMonoidal.mλ-iso isM) )) ⟩
818 FMap F id ( φ ( unit , u) )
819 ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩
820 id ( φ ( unit , u) )
821 ≡⟨⟩
822 φ ( unit , u)
823 ∎ )
824 where
825 open Relation.Binary.PropositionalEquality.≡-Reasoning
826 φunitl : {a : Obj Sets } {u : FObj F a} → φ ( u , unit ) ≡ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
827 φunitl {a} {u} = sym ( begin
828 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
829 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩
830 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) ( φ ( u , unit ) ) )
831 ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩
832 (FMap F ( (Iso.≅← (IsMonoidal.mρ-iso isM)) o (Iso.≅→ (IsMonoidal.mρ-iso isM)))) ( φ ( u , unit ) )
833 ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( u , unit ) )) (Iso.iso→ ( (IsMonoidal.mρ-iso isM) )) ⟩
834 FMap F id ( φ ( u , unit ) )
835 ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩
836 id ( φ ( u , unit ) )
837 ≡⟨⟩
838 φ ( u , unit )
839 ∎ )
840 where
841 open Relation.Binary.PropositionalEquality.≡-Reasoning
842 open IsMonoidal
843 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u
844 identity {a} {u} = begin
845 pure id <*> u
846 ≡⟨⟩
847 ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , u ) )
848 ≡⟨ ≡-cong ( λ k → ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , k ))) u→F ⟩
849 ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , FMap F id u ) )
850 ≡⟨ FφF→F ⟩
851 FMap F (λ x → proj₂ x ) (φ (unit , u ) )
852 ≡⟨⟩
853 FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u ))
854 ≡⟨ IsHaskellMonoidalFunctor.idlφ mono ⟩
855 u
856 ∎
857 where
858 open Relation.Binary.PropositionalEquality.≡-Reasoning
859 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
860 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w)
861 composition {a} {b} {c} {u} {v} {w} = begin
862 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
863 (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , u)) , v)) , w))
864 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , k)) , v)) , w)) ) u→F ⟩
865 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
866 (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , FMap F id u )) , v)) , w))
867 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( k , v)) , w)) ) FφF→F ⟩
868 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
869 (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , v)) , w))
870 ≡⟨ ≡-cong ( λ k → ( FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
871 (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) k , v)) , w)) ) ) φunitr ⟩
872 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
873 ( (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w))
874 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
875 (k u , v)) , w)) ) (sym ( IsFunctor.distr (isFunctor F ))) ⟩
876 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
877 ( FMap F (λ x → ((λ y f g x₁ → f (g x₁)) unit x) ) u , v)) , w))
878 ≡⟨⟩
879 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
880 ( FMap F (λ x g h → x (g h) ) u , v)) , w))
881 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( FMap F (λ x g h → x (g h) ) u , k)) , w)) ) u→F ⟩
882 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x g h → x (g h)) u , FMap F id v)) , w))
883 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w)) ) FφF→F ⟩
884 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x g h → x (g h)) id) (φ (u , v)) , w))
885 ≡⟨⟩
886 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w))
887 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k)) ) u→F ⟩
888 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , FMap F id w))
889 ≡⟨ FφF→F ⟩
890 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id) (φ (φ (u , v) , w))
891 ≡⟨⟩
892 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w))
893 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)) )) (sym (IsFunctor.identity (isFunctor F ))) ⟩
894 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F id (φ (φ (u , v) , w)) )
895 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F k (φ (φ (u , v) , w)) ) ) (sym (Iso.iso→ (mα-iso isM))) ⟩
896 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F ( (Iso.≅← (mα-iso isM)) o (Iso.≅→ (mα-iso isM))) (φ (φ (u , v) , w)) )
897 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)))) ( IsFunctor.distr (isFunctor F )) ⟩
898 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) ( FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (u , v) , w)) ))
899 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) k) ) (sym ( IsHaskellMonoidalFunctor.assocφ mono ) ) ⟩
900 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w))))
901 ≡⟨⟩
902 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) (φ (u , φ (v , w))))
903 ≡⟨ left (sym ( IsFunctor.distr (isFunctor F ))) ⟩
904 FMap F (λ y → (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) ((λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) y )) (φ (u , φ (v , w)))
905 ≡⟨⟩
906 FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w)))
907 ≡⟨⟩
908 FMap F ( λ x → (proj₁ x) ((λ r → proj₁ r (proj₂ r)) ( proj₂ x))) ( φ ( u , (φ (v , w))))
909 ≡⟨ sym FφF→F ⟩
910 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
911 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) ) (sym u→F ) ⟩
912 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
913 ∎
914 where
915 open Relation.Binary.PropositionalEquality.≡-Reasoning
916 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x)
917 homomorphism {a} {b} {f} {x} = begin
918 pure f <*> pure x
919 ≡⟨⟩
920 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y → f) unit , FMap F (λ y → x) unit))
921 ≡⟨ FφF→F ⟩
922 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y → f) (λ y → x)) (φ (unit , unit))
923 ≡⟨⟩
924 FMap F (λ y → f x) (φ (unit , unit))
925 ≡⟨ ≡-cong ( λ k → FMap F (λ y → f x) k ) φunitl ⟩
926 FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit)
927 ≡⟨⟩
928 FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit)
929 ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F ))) ⟩
930 FMap F (λ y → f x) unit
931 ≡⟨⟩
932 pure (f x)
933 ∎
934 where
935 open Relation.Binary.PropositionalEquality.≡-Reasoning
936 interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
937 interchange {a} {b} {u} {x} = begin
938 u <*> pure x
939 ≡⟨⟩
940 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ y → x) unit))
941 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ y → x) unit)) ) u→F ⟩
942 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ y → x) unit))
943 ≡⟨ FφF→F ⟩
944 FMap F ((λ r → proj₁ r (proj₂ r)) o map id (λ y → x)) (φ (u , unit))
945 ≡⟨⟩
946 FMap F (λ r → proj₁ r x) (φ (u , unit))
947 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r x) k ) φunitl ⟩
948 FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u )
949 ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩
950 FMap F (( λ r → proj₁ r x) o ((Iso.≅← (mρ-iso isM) ))) u
951 ≡⟨⟩
952 FMap F (( λ r → proj₂ r x) o ((Iso.≅← (mλ-iso isM) ))) u
953 ≡⟨ left ( IsFunctor.distr (isFunctor F )) ⟩
954 FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u)
955 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩
956 FMap F (λ r → proj₂ r x) (φ (unit , u))
957 ≡⟨⟩
958 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y f → f x) id) (φ (unit , u))
959 ≡⟨ sym FφF→F ⟩
960 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , FMap F id u))
961 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , k)) ) (sym u→F) ⟩
962 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , u))
963 ≡⟨⟩
964 pure (λ f → f x) <*> u
965 ∎
966 where
967 open Relation.Binary.PropositionalEquality.≡-Reasoning
968
969 ----
970 --
971 -- Applicative laws imples Monoidal laws
972 --
973
974 Applicative→HaskellMonoidal : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
975 ( App : Applicative F )
976 → HaskellMonoidalFunctor F
977 Applicative→HaskellMonoidal {l} F App = record {
978 unit = unit ;
979 φ = φ ;
980 isHaskellMonoidalFunctor = record {
981 natφ = natφ
982 ; assocφ = assocφ
983 ; idrφ = idrφ
984 ; idlφ = idlφ
985 }
986 } where
987 pure = Applicative.pure App
988 <*> = Applicative.<*> App
989 app = Applicative.isApplicative App
990 unit : FObj F One
991 unit = pure OneObj
992 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) )
993 φ = λ x → <*> (FMap F (λ j k → (j , k)) ( proj₁ x)) ( proj₂ x)
994 isM : IsMonoidal (Sets {l}) One SetsTensorProduct
995 isM = Monoidal.isMonoidal MonoidalSets
996 MF : MonoidalFunctor {_} {l} {_} {Sets} {Sets} MonoidalSets MonoidalSets
997 MF = Applicative→Monoidal F App app
998 isMF = MonoidalFunctor.isMonodailFunctor MF
999 natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d }
1000 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
1001 natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin
1002 FMap F (map f g) (φ (x , y))
1003 ≡⟨⟩
1004 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (<*> (FMap F (λ j k → j , k) x) y)
1005 ≡⟨ ≡-cong ( λ h → h (x , y)) ( IsNTrans.commute ( NTrans.isNTrans ( IsMonoidalFunctor.φab isMF ))) ⟩
1006 <*> (FMap F (λ j k → j , k) (FMap F f x)) (FMap F g y)
1007 ≡⟨⟩
1008 φ (FMap F f x , FMap F g y)
1009 ∎
1010 where
1011 open Relation.Binary.PropositionalEquality.≡-Reasoning
1012 assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
1013 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (IsMonoidal.mα-iso isM)) (φ (φ (a , b) , c))
1014 assocφ {x} {y} {z} {a} {b} {c} = ≡-cong ( λ h → h ((a , b) , c ) ) ( IsMonoidalFunctor.associativity isMF )
1015 idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) (φ (x , unit)) ≡ x
1016 idrφ {a} {x} = ≡-cong ( λ h → h (x , OneObj ) ) ( IsMonoidalFunctor.unitarity-idr isMF {a} {One} )
1017 idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x
1018 idlφ {a} {x} = ≡-cong ( λ h → h (OneObj , x ) ) ( IsMonoidalFunctor.unitarity-idl isMF {One} {a} )
1019
1020