Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 712:9092874a0633

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 12:37:22 +0900
parents bb5b028489dc
children 5e101ee6dab9
comparison
equal deleted inserted replaced
711:bb5b028489dc 712:9092874a0633
409 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x 409 (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 410 comm10 {x} {y} {f} ((a , b) , c ) = begin
411 φ (( id1 Sets (FObj F x) □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) 411 φ (( id1 Sets (FObj F x) □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
412 ≡⟨⟩ 412 ≡⟨⟩
413 φ ( a , φ (b , c)) 413 φ ( a , φ (b , c))
414 ≡⟨ {!!} ⟩ 414 ≡⟨ {!!} ⟩
415 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ (a , b)) , c )) 415 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ (a , b)) , c ))
416 ≡⟨⟩ 416 ≡⟨⟩
417 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c))) 417 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c)))
418 ∎ 418 ∎
419 where 419 where
421 open ≡-Reasoning 421 open ≡-Reasoning
422 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ 422 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ
423 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] 423 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)) ] ] ] 424 ≈ 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 ) 425 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x )
426 comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [
427 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
429 comm20 {a} {b} (x , OneObj ) = begin
430 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ( x , unit ) )
431 ≡⟨ {!!} ⟩
432 x
433 ≡⟨⟩
434 Iso.≅→ (mρ-iso isM) ( x , OneObj )
435 ∎
436 where
437 open import Relation.Binary.PropositionalEquality
438 open ≡-Reasoning
426 comm2 : {a b : Obj Sets} → Sets [ Sets [ 439 comm2 : {a b : Obj Sets} → Sets [ Sets [
427 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o 440 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
428 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] 441 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
429 comm2 {a} {b} = extensionality Sets ( λ x → begin 442 comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x )
430 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ( proj₁ x , unit ) ) 443 comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [
444 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
446 comm30 {a} {b} ( OneObj , x) = begin
447 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) )
431 ≡⟨ {!!} ⟩ 448 ≡⟨ {!!} ⟩
432 Iso.≅→ (mρ-iso isM) x 449 x
433 ∎ ) 450 ≡⟨⟩
451 Iso.≅→ (mλ-iso isM) ( OneObj , x )
452 ∎
434 where 453 where
435 open import Relation.Binary.PropositionalEquality 454 open import Relation.Binary.PropositionalEquality
436 open ≡-Reasoning 455 open ≡-Reasoning
437 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o 456 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
438 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] 457 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
439 comm3 {a} {b} = extensionality Sets ( λ x → begin 458 comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x )
440 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , proj₂ x) )
441 ≡⟨ {!!} ⟩
442 Iso.≅→ (mλ-iso isM) x
443 ∎ )
444 where
445 open import Relation.Binary.PropositionalEquality
446 open ≡-Reasoning
447
448 459
449 460
450 record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) 461 record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
451 : Set (suc (suc c₁)) where 462 : Set (suc (suc c₁)) where
452 field 463 field