Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 714:bc21e89cd273

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 23 Nov 2017 20:18:09 +0900
parents 5e101ee6dab9
children 1be42267eeee
comparison
equal deleted inserted replaced
713:5e101ee6dab9 714:bc21e89cd273
367 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) 367 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
368 law2 : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } 368 law2 : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
369 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) 369 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c))
370 law3 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x 370 law3 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
371 law4 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x 371 law4 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
372
373 -- http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
374 -- naturality of φ fmap(f × g)(φ u v) = φ ( fmap f u) ( fmap g v )
375 -- left identity fmap snd (φ unit v) = v
376 -- right identity fmap fst (φ u unit) = u
377 -- associativity fmap assoc (φ u (φ v w)) = φ (φ u v) w
378
372 379
373 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) 380 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
374 : Set (suc (suc c₁)) where 381 : Set (suc (suc c₁)) where
375 field 382 field
376 unit : FObj f One 383 unit : FObj f One
478 ( _<*>_ : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b ) 485 ( _<*>_ : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b )
479 : Set (suc (suc c₁)) where 486 : Set (suc (suc c₁)) where
480 _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c 487 _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
481 _・_ f g = λ x → f ( g x ) 488 _・_ f g = λ x → f ( g x )
482 field 489 field
490 -- http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
483 identity : { a : Obj Sets } { u : FObj f a } → pure ( id1 Sets a ) <*> u ≡ u 491 identity : { a : Obj Sets } { u : FObj f a } → pure ( id1 Sets a ) <*> u ≡ u
484 composition : { a b c : Obj Sets } { u : FObj f ( b → c ) } { v : FObj f (a → b ) } { w : FObj f a } 492 composition : { a b c : Obj Sets } { u : FObj f ( b → c ) } { v : FObj f (a → b ) } { w : FObj f a }
485 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) 493 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w)
486 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) 494 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x)
487 interchange : { a b : Obj Sets } { u : FObj f ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u 495 interchange : { a b : Obj Sets } { u : FObj f ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
523 ; composition = composition 531 ; composition = composition
524 ; homomorphism = homomorphism 532 ; homomorphism = homomorphism
525 ; interchange = interchange 533 ; interchange = interchange
526 } 534 }
527 where 535 where
536 id : { a : Obj Sets } → a → a
537 id x = x
528 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct 538 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct
529 isM = Monoidal.isMonoidal MonoidalSets 539 isM = Monoidal.isMonoidal MonoidalSets
530 open IsMonoidal 540 open IsMonoidal
531 pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) 541 pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
532 pure {a} x = FMap F ( λ y → x ) (unit ) 542 pure {a} x = FMap F ( λ y → x ) (unit )
534 _<*>_ {a} {b} x y = FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) (φ ( x , y )) 544 _<*>_ {a} {b} x y = FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) (φ ( x , y ))
535 _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c 545 _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
536 _・_ f g = λ x → f ( g x ) 546 _・_ f g = λ x → f ( g x )
537 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u 547 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u
538 identity {a} {u} = begin 548 identity {a} {u} = begin
539 pure ( id1 Sets a ) <*> u 549 pure id <*> u
540 ≡⟨⟩ 550 ≡⟨⟩
541 ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id1 Sets a ) unit , u ) ) 551 ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id ) unit , u ) )
542 ≡⟨ sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id1 Sets a ) unit , k u ))) 552 ≡⟨ sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id ) unit , k u )))
543 ( IsFunctor.identity ( Functor.isFunctor F ) ) ) ⟩ 553 ( IsFunctor.identity ( Functor.isFunctor F ) ) ) ⟩
544 ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id1 Sets a ) unit , FMap F (id1 Sets a) u ) ) 554 ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id ) unit , FMap F id u ) )
545 ≡⟨ sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) k ) ( IsHaskellMonoidalFunctor.law1 mono ) ) ⟩ 555 ≡⟨ sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) k ) ( IsHaskellMonoidalFunctor.law1 mono ) ) ⟩
546 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y → id1 Sets a) (λ x → x )) (φ (unit , u ))) 556 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y → id) id) (φ (unit , u )))
547 ≡⟨ ≡-cong ( λ k → k (φ (unit , u ) )) ( sym ( IsFunctor.distr ( Functor.isFunctor F ) ) ) ⟩ 557 ≡⟨ ≡-cong ( λ k → k (φ (unit , u ) )) ( sym ( IsFunctor.distr ( Functor.isFunctor F ) ) ) ⟩
548 FMap F (λ x → (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y → id1 Sets a) (λ x → x )) x )) (φ (unit , u ) ) 558 FMap F (λ x → (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y → id) id) x )) (φ (unit , u ) )
549 ≡⟨⟩ 559 ≡⟨⟩
550 FMap F (λ x → proj₂ x ) (φ (unit , u ) ) 560 FMap F (λ x → proj₂ x ) (φ (unit , u ) )
551 ≡⟨⟩ 561 ≡⟨⟩
552 FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u )) 562 FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u ))
553 ≡⟨ IsHaskellMonoidalFunctor.law4 mono ⟩ 563 ≡⟨ IsHaskellMonoidalFunctor.law4 mono ⟩
556 where 566 where
557 open Relation.Binary.PropositionalEquality.≡-Reasoning 567 open Relation.Binary.PropositionalEquality.≡-Reasoning
558 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a } 568 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
559 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) 569 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w)
560 composition {a} {b} {c} {u} {v} {w} = begin 570 composition {a} {b} {c} {u} {v} {w} = begin
561 ? 571 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
562 ≡⟨ ? ⟩ 572 (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ y f g x → f (g x)) unit , u)) , v)) , w))
563 ? 573 ≡⟨ {!!} ⟩
574 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
575 (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ y f g x → f (g x)) unit , FMap F id u)) , FMap F id v)) , FMap F id w))
576 ≡⟨ {!!} ⟩
577 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
578 (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y f g x → f (g x)) id ) (φ ( unit , u))) , FMap F id v)) , FMap F id w))
579 ≡⟨ {!!} ⟩
580 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
581 (FMap F ( λ x → (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , FMap F id v)) , FMap F id w))
582 ≡⟨⟩
583 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
584 (FMap F ( λ y → (λ f g x → f (g x)) (proj₂ y ) ) (φ ( unit , u)) , FMap F id v)) , FMap F id w))
585 ≡⟨ {!!} ⟩
586 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (
587 FMap F ( map ( λ y → (λ f g x → f (g x)) (proj₂ y ) ) id ) ( φ ( φ ( unit , u) , v))) , FMap F id w))
588 ≡⟨ {!!} ⟩
589 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (
590 FMap F ( λ x → (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (( map ( λ y → (λ f g x → f (g x)) (proj₂ y ) ) id ) x)) ( φ ( φ ( unit , u) , v))
591 , FMap F id w))
592 ≡⟨⟩
593 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (
594 FMap F ( λ z → ((( λ f g x → f (g x)) (proj₂ (proj₁ z))) ( proj₂ z ))) ( φ ( φ ( unit , u) , v))
595 , FMap F id w))
596 ≡⟨ {!!} ⟩
597 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (u , FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (v , w))))
564 ∎ 598 ∎
565 where 599 where
566 open Relation.Binary.PropositionalEquality.≡-Reasoning 600 open Relation.Binary.PropositionalEquality.≡-Reasoning
567 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) 601 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x)
568 homomorphism = {!!} 602 homomorphism = {!!}