Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 713:5e101ee6dab9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
identity done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 23 Nov 2017 18:24:44 +0900
parents 9092874a0633
children bc21e89cd273
comparison
equal deleted inserted replaced
712:9092874a0633 713:5e101ee6dab9
352 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x 352 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x
353 mρiso (_ , OneObj ) = refl 353 mρiso (_ , OneObj ) = refl
354 354
355 ≡-cong = Relation.Binary.PropositionalEquality.cong 355 ≡-cong = Relation.Binary.PropositionalEquality.cong
356 356
357
358 record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
359 ( unit : FObj F One )
360 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) )
361 : Set (suc (suc c₁)) where
362 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct
363 isM = Monoidal.isMonoidal MonoidalSets
364 open IsMonoidal
365 field
366 law1 : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d }
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 }
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
371 law4 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
372
357 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) 373 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
358 : Set (suc (suc c₁)) where 374 : Set (suc (suc c₁)) where
359 field 375 field
360 unit : FObj f One 376 unit : FObj f One
361 φ : {a b : Obj Sets} → Hom Sets ((FObj f a) * (FObj f b )) ( FObj f ( a * b ) ) 377 φ : {a b : Obj Sets} → Hom Sets ((FObj f a) * (FObj f b )) ( FObj f ( a * b ) )
362 ** : {a b : Obj Sets} → FObj f a → FObj f b → FObj f ( a * b ) 378 ** : {a b : Obj Sets} → FObj f a → FObj f b → FObj f ( a * b )
363 ** x y = φ ( x , y ) 379 ** x y = φ ( x , y )
364 380
365 lemma0 : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → HaskellMonoidalFunctor F → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets 381 lemma0 : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F )
366 lemma0 F mf = record { 382 → IsHaskellMonoidalFunctor F ( HaskellMonoidalFunctor.unit mf ) ( HaskellMonoidalFunctor.φ mf )
383 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
384 lemma0 F mf ismf = record {
367 MF = F 385 MF = F
368 ; ψ = λ _ → HaskellMonoidalFunctor.unit mf 386 ; ψ = λ _ → HaskellMonoidalFunctor.unit mf
369 ; isMonodailFunctor = record { 387 ; isMonodailFunctor = record {
370 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } } 388 φab = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } }
371 ; associativity = λ {a b c} → comm1 {a} {b} {c} 389 ; associativity = λ {a b c} → comm1 {a} {b} {c}
390 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) (φ (x , y)) 408 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) (φ (x , y))
391 ≡⟨⟩ 409 ≡⟨⟩
392 (FMap F ( f □ g ) ) (φ (x , y)) 410 (FMap F ( f □ g ) ) (φ (x , y))
393 ≡⟨⟩ 411 ≡⟨⟩
394 FMap F ( map f g ) (φ (x , y)) 412 FMap F ( map f g ) (φ (x , y))
395 ≡⟨ {!!} ⟩ 413 ≡⟨ IsHaskellMonoidalFunctor.law1 ismf ⟩
396 φ ( FMap F f x , FMap F g y ) 414 φ ( FMap F f x , FMap F g y )
397 ≡⟨⟩ 415 ≡⟨⟩
398 φ ( ( FMap F f □ FMap F g ) (x , y) ) 416 φ ( ( FMap F f □ FMap F g ) (x , y) )
399 ≡⟨⟩ 417 ≡⟨⟩
400 φ ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) ) 418 φ ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) )
401 ∎ 419 ∎
402 where 420 where
403 open import Relation.Binary.PropositionalEquality 421 open Relation.Binary.PropositionalEquality.≡-Reasoning
404 open ≡-Reasoning
405 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] 422 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]
406 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] 423 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
407 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x ) 424 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
408 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 ≡ 425 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 ≡
409 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x 426 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x
410 comm10 {x} {y} {f} ((a , b) , c ) = begin 427 comm10 {x} {y} {f} ((a , b) , c ) = begin
411 φ (( id1 Sets (FObj F x) □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) 428 φ (( id1 Sets (FObj F x) □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
412 ≡⟨⟩ 429 ≡⟨⟩
413 φ ( a , φ (b , c)) 430 φ ( a , φ (b , c))
414 ≡⟨ {!!} ⟩ 431 ≡⟨ IsHaskellMonoidalFunctor.law2 ismf ⟩
415 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ (a , b)) , c )) 432 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ (a , b)) , c ))
416 ≡⟨⟩ 433 ≡⟨⟩
417 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c))) 434 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c)))
418 ∎ 435 ∎
419 where 436 where
420 open import Relation.Binary.PropositionalEquality 437 open Relation.Binary.PropositionalEquality.≡-Reasoning
421 open ≡-Reasoning
422 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ 438 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ
423 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] 439 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
424 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] 440 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ]
425 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x ) 441 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x )
426 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ 442 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [
427 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o 443 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
428 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x 444 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x
429 comm20 {a} {b} (x , OneObj ) = begin 445 comm20 {a} {b} (x , OneObj ) = begin
430 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ( x , unit ) ) 446 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ( x , unit ) )
431 ≡⟨ {!!} ⟩ 447 ≡⟨ IsHaskellMonoidalFunctor.law3 ismf ⟩
432 x 448 x
433 ≡⟨⟩ 449 ≡⟨⟩
434 Iso.≅→ (mρ-iso isM) ( x , OneObj ) 450 Iso.≅→ (mρ-iso isM) ( x , OneObj )
435 ∎ 451 ∎
436 where 452 where
437 open import Relation.Binary.PropositionalEquality 453 open Relation.Binary.PropositionalEquality.≡-Reasoning
438 open ≡-Reasoning
439 comm2 : {a b : Obj Sets} → Sets [ Sets [ 454 comm2 : {a b : Obj Sets} → Sets [ Sets [
440 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o 455 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
441 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] 456 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
442 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x ) 457 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x )
443 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ 458 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [
444 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o 459 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o
445 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x 460 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x
446 comm30 {a} {b} ( OneObj , x) = begin 461 comm30 {a} {b} ( OneObj , x) = begin
447 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) ) 462 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) )
448 ≡⟨ {!!} ⟩ 463 ≡⟨ IsHaskellMonoidalFunctor.law4 ismf ⟩
449 x 464 x
450 ≡⟨⟩ 465 ≡⟨⟩
451 Iso.≅→ (mλ-iso isM) ( OneObj , x ) 466 Iso.≅→ (mλ-iso isM) ( OneObj , x )
452 ∎ 467 ∎
453 where 468 where
454 open import Relation.Binary.PropositionalEquality 469 open Relation.Binary.PropositionalEquality.≡-Reasoning
455 open ≡-Reasoning
456 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o 470 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
457 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] 471 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
458 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x ) 472 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x )
459 473
460 474
461 record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) 475
476 record IsApplicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
477 ( pure : {a : Obj Sets} → Hom Sets a ( FObj f a ) )
478 ( _<*>_ : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b )
462 : Set (suc (suc c₁)) where 479 : Set (suc (suc c₁)) where
463 field 480 _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
464 pure : {a : Obj Sets} → Hom Sets a ( FObj f a ) 481 _・_ f g = λ x → f ( g x )
465 <*> : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b 482 field
483 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 }
485 → (( 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)
487 interchange : { a b : Obj Sets } { u : FObj f ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
488
489 record Applicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
490 : Set (suc (suc c₁)) where
491 field
492 pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
493 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
466 -- should have Applicative law 494 -- should have Applicative law
467 495
468 lemma1 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative f → HaskellMonoidalFunctor f 496 lemma1 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative F → HaskellMonoidalFunctor F
469 lemma1 f app = record { unit = unit ; φ = φ } 497 lemma1 F app = record { unit = unit ; φ = φ }
470 where 498 where
471 open Applicative 499 open Applicative
472 unit : FObj f One 500 unit : FObj F One
473 unit = pure app OneObj 501 unit = pure app OneObj
474 φ : {a b : Obj Sets} → Hom Sets ((FObj f a) * (FObj f b )) ( FObj f ( a * b ) ) 502 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) )
475 φ {a} {b} ( x , y ) = <*> app (FMap f (λ j k → (j , k)) x) y 503 φ {a} {b} ( x , y ) = <*> app (FMap F (λ j k → (j , k)) x) y
476 504
477 lemma2 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor f → Applicative f 505 lemma2 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor F → Applicative F
478 lemma2 f mono = record { pure = pure ; <*> = <*> } 506 lemma2 F mono = record { pure = pure ; <*> = <*> }
479 where 507 where
480 open HaskellMonoidalFunctor 508 open HaskellMonoidalFunctor
481 pure : {a : Obj Sets} → Hom Sets a ( FObj f a ) 509 pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
482 pure {a} x = FMap f ( λ y → x ) (unit mono) 510 pure {a} x = FMap F ( λ y → x ) (unit mono)
483 <*> : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b -- ** mono x y 511 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b -- ** mono x y
484 <*> {a} {b} x y = FMap f ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) (φ mono ( x , y )) 512 <*> {a} {b} x y = FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) (φ mono ( x , y ))
513
514 open Relation.Binary.PropositionalEquality
515
516 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
517 ( unit : FObj F One )
518 ( φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) ) )
519 ( mono : IsHaskellMonoidalFunctor F unit φ )
520 → IsApplicative F (λ x → FMap F ( λ y → x ) unit) (λ x y → FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) (φ ( x , y )))
521 HaskellMonoidal→Applicative {c₁} F unit φ mono = record {
522 identity = identity
523 ; composition = composition
524 ; homomorphism = homomorphism
525 ; interchange = interchange
526 }
527 where
528 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct
529 isM = Monoidal.isMonoidal MonoidalSets
530 open IsMonoidal
531 pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
532 pure {a} x = FMap F ( λ y → x ) (unit )
533 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
534 _<*>_ {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
536 _・_ f g = λ x → f ( g x )
537 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u
538 identity {a} {u} = begin
539 pure ( id1 Sets a ) <*> u
540 ≡⟨⟩
541 ( FMap F ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b )) ) ( φ ( FMap F ( λ y → id1 Sets a ) 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 )))
543 ( 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 ) )
545 ≡⟨ 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 )))
547 ≡⟨ ≡-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 ) )
549 ≡⟨⟩
550 FMap F (λ x → proj₂ x ) (φ (unit , u ) )
551 ≡⟨⟩
552 FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u ))
553 ≡⟨ IsHaskellMonoidalFunctor.law4 mono ⟩
554 u
555 ∎
556 where
557 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 }
559 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w)
560 composition {a} {b} {c} {u} {v} {w} = begin
561 ?
562 ≡⟨ ? ⟩
563 ?
564 ∎
565 where
566 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)
568 homomorphism = {!!}
569 interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
570 interchange = {!!}