Mercurial > hg > Members > kono > Proof > category
changeset 725:bd371f36df9a
fill proofs
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 26 Nov 2017 14:33:12 +0900 |
| parents | df7697122d80 |
| children | e663c63cdf41 |
| files | monoidal.agda |
| diffstat | 1 files changed, 100 insertions(+), 14 deletions(-) [+] |
line wrap: on
line diff
--- a/monoidal.agda Sun Nov 26 10:59:38 2017 +0900 +++ b/monoidal.agda Sun Nov 26 14:33:12 2017 +0900 @@ -553,8 +553,9 @@ id x = x pure : {a : Obj Sets } → Hom Sets a ( FObj F a ) pure a = Applicative.pure mf a - pure→Fid : {a b : Obj Sets } → (x : FObj F a ) → FMap F id x ≡ pure id <*> x - pure→Fid {a} {b} x = sym ( begin + -- special case + F→pureid : {a b : Obj Sets } → (x : FObj F a ) → FMap F id x ≡ pure id <*> x + F→pureid {a} {b} x = sym ( begin pure id <*> x ≡⟨ IsApplicative.identity ismf ⟩ x @@ -586,8 +587,8 @@ FMap F f ∎ where open ≈-Reasoning Sets hiding ( _o_ ) - pure→F : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } → FMap F f x ≡ pure f <*> x - pure→F {a} {b} {f} {x} = sym ( begin + F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } → FMap F f x ≡ pure f <*> x + F→pure {a} {b} {f} {x} = sym ( begin pure f <*> x ≡⟨ ≡-cong ( λ k → k x ) (UniqunessOfFunctor F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x → IsApplicative.identity ismf ))) ⟩ FMap F f x @@ -595,26 +596,47 @@ where open Relation.Binary.PropositionalEquality open Relation.Binary.PropositionalEquality.≡-Reasoning + p*p : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) + p*p = IsApplicative.homomorphism ismf + car : { a b c : Obj Sets } { f : Hom Sets a (b → c) } { x : a } { y : FObj F b } + → ( (pure f <*> pure x ) <*> y ) ≡ ( pure (f x) <*> y ) + car = left ( IsApplicative.homomorphism ismf ) + cdr : { a b c d : Obj Sets } { f : Hom Sets a c } { x : a } { y : FObj F (c → d) } + → y <*> (pure f <*> pure x ) ≡ y <*> ( pure (f x) ) + cdr = right ( IsApplicative.homomorphism ismf ) + cdar : { a b c d : Obj Sets } { f : Hom Sets a (b → c) } { x : a } { y : FObj F b } { y1 : FObj F (c → d) } + → y1 <*> ( (pure f <*> pure x ) <*> y ) ≡ y1 <*> ( pure (f x) <*> y ) + cdar = right ( left ( IsApplicative.homomorphism ismf ) ) + cadr : { a b c d e : Obj Sets } { f : Hom Sets a c } { x : a } { y : FObj F (c → ( e → a )) } { y1 : FObj F e } + → (y <*> (pure f <*> pure x )) <*> y1 ≡ (y <*> ( pure (f x) )) <*> y1 + cadr = left (right ( IsApplicative.homomorphism ismf ) ) + comp = IsApplicative.composition ismf + inter = IsApplicative.interchange ismf comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x comm00 {a} {b} {(f , g)} (x , y) = begin ( FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ( φ (x , y) ) ≡⟨⟩ - FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y) ≡⟨⟩ + FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y) + ≡⟨⟩ FMap F (map f g) ((FMap F (λ j k → j , k) x) <*> y) - ≡⟨ {!!} ⟩ + ≡⟨ F→pure ⟩ + (pure (map f g) <*> (FMap F (λ j k → j , k) x <*> y)) + ≡⟨ right ( left F→pure ) ⟩ (pure (map f g)) <*> ((pure (λ j k → j , k) <*> x) <*> y) ≡⟨ sym ( IsApplicative.composition ismf ) ⟩ (( pure _・_ <*> (pure (map f g))) <*> (pure (λ j k → j , k) <*> x)) <*> y ≡⟨ left ( sym ( IsApplicative.composition ismf )) ⟩ ((( pure _・_ <*> (( pure _・_ <*> (pure (map f g))))) <*> pure (λ j k → j , k)) <*> x) <*> y - ≡⟨ {!!} ⟩ + ≡⟨ trans ( trans (left ( left (left (right p*p )))) ( left ( left ( left p*p)))) (left (left p*p)) ⟩ (pure (( _・_ (( _・_ ((map f g))))) (λ j k → j , k)) <*> x) <*> y ≡⟨⟩ (pure (λ j k → f j , g k) <*> x) <*> y - ≡⟨ {!!} ⟩ + ≡⟨⟩ ( pure ((_・_ (( _・_ ( ( λ h → h g ))) ( _・_ ))) ((λ j k → f j , k))) <*> x ) <*> y - ≡⟨ {!!} ⟩ + ≡⟨ sym ( trans (left (left (left p*p))) (left ( left p*p)) ) ⟩ + ((((pure _・_ <*> pure ((λ h → h g) ・ _・_)) <*> pure (λ j k → f j , k)) <*> x) <*> y) + ≡⟨ sym (trans ( left ( left ( left (right (left p*p) )))) (left ( left (left (right p*p ))))) ⟩ (((pure _・_ <*> (( pure _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ ))) <*> (pure (λ j k → f j , k))) <*> x ) <*> y ≡⟨ left ( ( IsApplicative.composition ismf )) ⟩ ((( pure _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ )) <*> (pure (λ j k → f j , k) <*> x )) <*> y @@ -624,7 +646,7 @@ (( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) <*> pure g) <*> y ≡⟨ IsApplicative.composition ismf ⟩ (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y) - ≡⟨ {!!} ⟩ + ≡⟨ sym ( trans (left F→pure ) ( right F→pure ) ) ⟩ (FMap F (λ j k → f j , k) x) <*> (FMap F g y) ≡⟨ ≡-cong ( λ k → k x <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F )) ⟩ (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y) @@ -643,8 +665,52 @@ φ (( id □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) ≡⟨⟩ (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c) - ≡⟨ sym (IsApplicative.composition ismf) ⟩ - ((pure _・_ <*> (FMap F (λ j k → j , k) a)) <*> (FMap F (λ j k → j , k) b)) <*> c + ≡⟨ {!!} ⟩ + (pure (λ j k → j , k) <*> a) <*> ( (pure (λ j k → j , k) <*> b) <*> c) + ≡⟨ {!!} ⟩ + ( ( 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 + ≡⟨ {!!} ⟩ + (( ( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k) <*> a))) <*> (pure (λ j k → j , k))) <*> b) <*> c + ≡⟨ {!!} ⟩ + (( ( pure _・_ <*> (( (pure _・_ <*> pure _・_ ) <*> (pure (λ j k → j , k))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c + ≡⟨ {!!} ⟩ + (( ( 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 + ≡⟨ {!!} ⟩ + ((((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 + ≡⟨ {!!} ⟩ + (((pure (λ f → f (λ j k → j , k))) <*> ((pure (λ f g x y → f , g x y)) <*> a) ) <*> b) <*> c + ≡⟨ {!!} ⟩ + (((( pure _・_ <*> (pure (λ f → f (λ j k → j , k)))) <*> (pure (λ f g x y → f , g x y))) <*> a ) <*> b) <*> c + ≡⟨ {!!} ⟩ + ((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 + ≡⟨ {!!} ⟩ + ((((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 + ≡⟨ {!!} ⟩ + (((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 + ≡⟨ {!!} ⟩ + ((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 + ≡⟨ {!!} ⟩ + ((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 + ≡⟨ {!!} ⟩ + ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*> + (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b))) <*> c + ≡⟨ {!!} ⟩ + pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) <*> ( (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b)) <*> c) ≡⟨ {!!} ⟩ 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) ≡⟨⟩ @@ -666,12 +732,23 @@ FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (pure OneObj)) ≡⟨ ≡-cong ( λ k → FMap F proj₁ k) ( IsApplicative.interchange ismf ) ⟩ FMap F proj₁ ((pure (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x)) - ≡⟨ {!!} ⟩ + ≡⟨ ( trans F→pure (right ( right F→pure )) ) ⟩ + pure proj₁ <*> ((pure (λ f → f OneObj)) <*> (pure (λ j k → j , k) <*> x)) + ≡⟨ sym ( right comp ) ⟩ + pure proj₁ <*> (((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k)) <*> x) + ≡⟨ sym comp ⟩ + ( ( pure _・_ <*> (pure proj₁ ) ) <*> ((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k))) <*> x + ≡⟨ trans ( trans ( trans ( left ( left p*p)) ( left ( right (left p*p) ))) (left (right p*p) ) ) (left p*p) ⟩ + pure ( ( _・_ proj₁ ) ((_・_ ((λ f → f OneObj))) (λ j k → j , k))) <*> x + ≡⟨⟩ + pure id <*> x + ≡⟨ IsApplicative.identity ismf ⟩ x ≡⟨⟩ Iso.≅→ (mρ-iso isM) (x , OneObj) ∎ where + open Relation.Binary.PropositionalEquality open Relation.Binary.PropositionalEquality.≡-Reasoning comm2 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o @@ -684,12 +761,21 @@ (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) ) ≡⟨⟩ FMap F proj₂ ((FMap F (λ j k → j , k) (pure OneObj)) <*> x) - ≡⟨ {!!} ⟩ + ≡⟨ ( trans F→pure (right ( left F→pure )) ) ⟩ + pure proj₂ <*> ((pure (λ j k → j , k) <*> (pure OneObj)) <*> x) + ≡⟨ sym comp ⟩ + ((pure _・_ <*> (pure proj₂)) <*> (pure (λ j k → j , k) <*> (pure OneObj))) <*> x + ≡⟨ trans (trans (left (left p*p )) (left ( right p*p)) ) (left p*p) ⟩ + pure ((_・_ proj₂) ((λ j k → j , k) OneObj)) <*> x + ≡⟨⟩ + pure id <*> x + ≡⟨ IsApplicative.identity ismf ⟩ x ≡⟨⟩ Iso.≅→ (mλ-iso isM) ( OneObj , x ) ∎ where + open Relation.Binary.PropositionalEquality open Relation.Binary.PropositionalEquality.≡-Reasoning comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]