Mercurial > hg > Members > kono > Proof > category
changeset 726:e663c63cdf41
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 26 Nov 2017 16:00:54 +0900 |
| parents | bd371f36df9a |
| children | ea84cc6c1797 |
| files | monoidal.agda |
| diffstat | 1 files changed, 20 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/monoidal.agda Sun Nov 26 14:33:12 2017 +0900 +++ b/monoidal.agda Sun Nov 26 16:00:54 2017 +0900 @@ -665,53 +665,54 @@ φ (( id □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) ≡⟨⟩ (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c) - ≡⟨ {!!} ⟩ + ≡⟨ trans (left F→pure) (right (left F→pure) ) ⟩ (pure (λ j k → j , k) <*> a) <*> ( (pure (λ j k → j , k) <*> b) <*> c) - ≡⟨ {!!} ⟩ + ≡⟨ sym comp ⟩ ( ( pure _・_ <*> (pure (λ j k → j , k) <*> a)) <*> (pure (λ j k → j , k) <*> b)) <*> c - ≡⟨ {!!} ⟩ - (( ( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k) <*> a))) <*> (pure (λ j k → j , k))) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ sym ( left comp ) ⟩ (( ( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k) <*> a))) <*> (pure (λ j k → j , k))) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ sym ( left ( left ( left (right comp )))) ⟩ (( ( pure _・_ <*> (( (pure _・_ <*> pure _・_ ) <*> (pure (λ j k → j , k))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ trans (left ( left (left ( right (left ( left p*p )))))) (left ( left ( left (right (left p*p))))) ⟩ (( ( pure _・_ <*> ((pure ((_・_ ( _・_ )) ((λ j k → j , k)))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ sym (left ( left ( left comp ) )) ⟩ (((( ( pure _・_ <*> (pure _・_ )) <*> (pure ((_・_ ( _・_ )) ((λ j k → j , k))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ trans (left ( left ( left (left (left p*p))))) (left ( left ( left (left p*p )))) ⟩ ((((pure ( ( _・_ (_・_ )) (((_・_ ( _・_ )) ((λ j k → j , k)))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c ≡⟨⟩ ((((pure (λ f g x y → f , g x y)) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ left ( left inter ) ⟩ (((pure (λ f → f (λ j k → j , k))) <*> ((pure (λ f g x y → f , g x y)) <*> a) ) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ sym ( left ( left comp )) ⟩ (((( pure _・_ <*> (pure (λ f → f (λ j k → j , k)))) <*> (pure (λ f g x y → f , g x y))) <*> a ) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ trans (left ( left (left (left p*p) ))) (left (left (left p*p ) )) ⟩ ((pure (( _・_ (λ f → f (λ j k → j , k))) (λ f g x y → f , g x y)) <*> a ) <*> b) <*> c ≡⟨⟩ (((pure (λ f g h → f , g , h)) <*> a) <*> b) <*> c ≡⟨⟩ ((pure ((_・_ ((_・_ ((_・_ ( (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) (( _・_ ( _・_ ((λ j k → j , k)))) (λ j k → j , k))) <*> a) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ sym (trans ( left ( left ( left (left (right (right p*p))) ) )) (trans (left (left( left (left (right p*p))))) + (trans (left (left (left (left p*p)))) (trans ( left (left (left (right (left (right p*p )))))) + (trans (left (left (left (right (left p*p))))) (trans (left (left (left (right p*p)))) (left (left (left p*p)))) ) ) ) + ) ) ⟩ ((((pure _・_ <*> ((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) <*> (( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k))) <*> a) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ left (left comp ) ⟩ (((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))) <*> ((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a)) <*> b) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ left comp ⟩ ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> (((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a) <*> b)) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ left ( right (left comp )) ⟩ ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> ((( pure _・_ <*> (pure (λ j k → j , k))) <*> (pure (λ j k → j , k) <*> a)) <*> b)) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ left ( right comp ) ⟩ ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b))) <*> c - ≡⟨ {!!} ⟩ + ≡⟨ comp ⟩ pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) <*> ( (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b)) <*> c) - ≡⟨ {!!} ⟩ + ≡⟨ sym ( trans ( trans F→pure (right (left F→pure ))) ( right ( left (right (left F→pure ))))) ⟩ 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) ≡⟨⟩ ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c)))