Mercurial > hg > Members > kono > Proof > category
changeset 721:a8b595fb4905
use FMap F f x ≡ pure f <*> x
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 25 Nov 2017 16:40:17 +0900 |
| parents | 13cef2bfa5c8 |
| children | 69f01b82dfc9 |
| files | monoidal.agda |
| diffstat | 1 files changed, 55 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/monoidal.agda Sat Nov 25 11:34:22 2017 +0900 +++ b/monoidal.agda Sat Nov 25 16:40:17 2017 +0900 @@ -541,20 +541,58 @@ _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d ) _□_ f g = FMap (m-bi M) ( f , g ) - right : {n : Level} { a b : Set n} → { x y : a → b } { h : a } → ( x ≡ y ) → x h ≡ y h - right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x) φ x = Applicative.<*> mf (FMap F (λ j k → (j , k)) (proj₁ x )) (proj₂ x) _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b _<*>_ = Applicative.<*> mf + left : {a b : Obj Sets} → {x y : FObj F ( a → b )} → {h : FObj F a } → ( x ≡ y ) → x <*> h ≡ y <*> h + left {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k <*> h ) eq + right : {a b : Obj Sets} → {h : FObj F ( a → b )} → {x y : FObj F a } → ( x ≡ y ) → h <*> x ≡ h <*> y + right {_} {_} {h} {_} {_} eq = ≡-cong ( λ k → h <*> k ) eq + id : { a : Obj Sets } → a → a + id x = x pure : {a : Obj Sets } → Hom Sets a ( FObj F a ) pure a = Applicative.pure mf a + 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 + pure f <*> x + ≡⟨ {!!} ⟩ + FMap F f x + ∎ ) + where + open Relation.Binary.PropositionalEquality + open Relation.Binary.PropositionalEquality.≡-Reasoning + 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 (map f g) ((FMap F (λ j k → j , k) x) <*> y) + ≡⟨ {!!} ⟩ + (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 + ≡⟨ {!!} ⟩ + (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 + ≡⟨ {!!} ⟩ + (((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 + ≡⟨ left (IsApplicative.composition ismf ) ⟩ + ( pure ( λ h → h g ) <*> ( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) ) <*> y + ≡⟨ left (sym (IsApplicative.interchange ismf )) ⟩ + (( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) <*> pure g) <*> y + ≡⟨ IsApplicative.composition ismf ⟩ + (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y) ≡⟨ {!!} ⟩ (FMap F (λ j k → f j , k) x) <*> (FMap F g y) ≡⟨ ≡-cong ( λ k → k x <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F )) ⟩ @@ -563,6 +601,7 @@ φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) ) ∎ where + open Relation.Binary.PropositionalEquality open Relation.Binary.PropositionalEquality.≡-Reasoning comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] @@ -570,7 +609,7 @@ 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 ≡ (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x comm10 {x} {y} {f} ((a , b) , c ) = begin - φ (( id1 Sets (FObj F x) □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) + φ (( 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) ⟩ @@ -647,11 +686,11 @@ pure {a} x = FMap F ( λ y → x ) (unit ) _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b _<*>_ {a} {b} x y = FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ ( x , y )) - -- left does not work right it makes yellows. why? - -- left : {n : Level} { a b : Set n} → { x y : a } { h : a → b } → ( x ≡ y ) → h x ≡ h y - -- left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq - right : {n : Level} { a b : Set n} → { x y : a → b } { h : a } → ( x ≡ y ) → x h ≡ y h - right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq + -- right does not work right it makes yellows. why? + -- right : {n : Level} { a b : Set n} → { x y : a } { h : a → b } → ( x ≡ y ) → h x ≡ h y + -- right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq + left : {n : Level} { a b : Set n} → { x y : a → b } { h : a } → ( x ≡ y ) → x h ≡ y h + left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq open Relation.Binary.PropositionalEquality FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d } { f : Hom Sets (c * d) e } @@ -673,11 +712,11 @@ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) ( φ ( unit , u) ) ) - ≡⟨ right ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ + ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ (FMap F ( (Iso.≅← (IsMonoidal.mλ-iso isM)) o (Iso.≅→ (IsMonoidal.mλ-iso isM)))) ( φ ( unit , u) ) ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( unit , u) )) (Iso.iso→ ( (IsMonoidal.mλ-iso isM) )) ⟩ FMap F id ( φ ( unit , u) ) - ≡⟨ right ( IsFunctor.identity ( isFunctor F ) ) ⟩ + ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ id ( φ ( unit , u) ) ≡⟨⟩ φ ( unit , u) @@ -689,11 +728,11 @@ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) ( φ ( u , unit ) ) ) - ≡⟨ right ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ + ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ (FMap F ( (Iso.≅← (IsMonoidal.mρ-iso isM)) o (Iso.≅→ (IsMonoidal.mρ-iso isM)))) ( φ ( u , unit ) ) ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( u , unit ) )) (Iso.iso→ ( (IsMonoidal.mρ-iso isM) )) ⟩ FMap F id ( φ ( u , unit ) ) - ≡⟨ right ( IsFunctor.identity ( isFunctor F ) ) ⟩ + ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ id ( φ ( u , unit ) ) ≡⟨⟩ φ ( u , unit ) @@ -761,7 +800,7 @@ FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w)))) ≡⟨⟩ FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) (φ (u , φ (v , w)))) - ≡⟨ right (sym ( IsFunctor.distr (isFunctor F ))) ⟩ + ≡⟨ left (sym ( IsFunctor.distr (isFunctor F ))) ⟩ FMap F (λ y → (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) ((λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) y )) (φ (u , φ (v , w))) ≡⟨⟩ FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w))) @@ -787,7 +826,7 @@ FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit) ≡⟨⟩ FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit) - ≡⟨ right ( sym ( IsFunctor.distr (isFunctor F ))) ⟩ + ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F ))) ⟩ FMap F (λ y → f x) unit ≡⟨⟩ pure (f x) @@ -807,11 +846,11 @@ FMap F (λ r → proj₁ r x) (φ (u , unit)) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r x) k ) φunitl ⟩ FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u ) - ≡⟨ right ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩ + ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩ FMap F (( λ r → proj₁ r x) o ((Iso.≅← (mρ-iso isM) ))) u ≡⟨⟩ FMap F (( λ r → proj₂ r x) o ((Iso.≅← (mλ-iso isM) ))) u - ≡⟨ right ( IsFunctor.distr (isFunctor F )) ⟩ + ≡⟨ left ( IsFunctor.distr (isFunctor F )) ⟩ FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩ FMap F (λ r → proj₂ r x) (φ (unit , u))