Mercurial > hg > Members > kono > Proof > category

changeset 716:35457f9568f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
composition done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Nov 2017 13:20:14 +0900
parents 1be42267eeee
children a41b2b9b0407
files monoidal.agda
diffstat 1 files changed, 71 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/monoidal.agda	Fri Nov 24 11:32:41 2017 +0900
+++ b/monoidal.agda	Fri Nov 24 13:20:14 2017 +0900
@@ -560,15 +560,47 @@
              ∎  )
            where
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
-          unit→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u 
-          unit→F {a} {u} =  sym ( ≡-cong ( λ k → k u ) ( IsFunctor.identity ( isFunctor F ) ) )
+          u→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u 
+          u→F {a} {u} =  sym ( ≡-cong ( λ k → k u ) ( IsFunctor.identity ( isFunctor F ) ) )
+          φunitr : {a : Obj Sets } {u : FObj F a} → φ ( unit , u) ≡ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
+          φunitr {a} {u} = sym ( begin 
+                  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 ) )) ⟩
+                  (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 ) ) ⟩
+                  id ( φ ( unit , u) )
+               ≡⟨⟩
+                  φ ( unit , u)
+             ∎  )
+           where
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+          φunitl : {a : Obj Sets } {u : FObj F a} → φ ( u , unit ) ≡ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
+          φunitl {a} {u} = sym ( begin 
+                  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 ) )) ⟩
+                  (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 ) ) ⟩
+                  id ( φ ( u , unit ) )
+               ≡⟨⟩
+                  φ ( u , unit )
+             ∎  )
+           where
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
           open IsMonoidal
           identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a )  <*> u ≡ u
           identity {a} {u} = begin 
                  pure id <*> u
                ≡⟨⟩
                  ( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ (  FMap F ( λ y → id ) unit  , u ) )
-               ≡⟨   ≡-cong ( λ k → ( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ ( FMap F ( λ y → id ) unit  ,  k  ))) unit→F  ⟩
+               ≡⟨   ≡-cong ( λ k → ( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ ( FMap F ( λ y → id ) unit  ,  k  ))) u→F  ⟩
                  ( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ (  FMap F ( λ y → id ) unit  , FMap F id u ) )
                ≡⟨ φ→F ⟩
                    FMap F (λ x → proj₂ x ) (φ (unit , u ) )
@@ -584,57 +616,54 @@
           composition {a} {b} {c} {u} {v} {w} = begin
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
                    (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , u)) , v)) , w))
-                ≡⟨  {!!} ⟩
+                ≡⟨  ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , k)) , v)) , w))  ) u→F  ⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
-                   (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , FMap F id u)) , FMap F id v)) , FMap F id w))
-                ≡⟨  {!!} ⟩
+                   (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , FMap F id u )) , v)) , w))
+                ≡⟨  ≡-cong ( λ k →  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( k  , v)) , w))  ) φ→F ⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
-                   (FMap F (λ r → proj₁ r (proj₂ r)) (FMap F (map (λ y f g x → f (g x)) id ) (φ ( unit , u))) , FMap F id v)) , FMap F id w))
-                ≡⟨  {!!} ⟩
+                   (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , v)) , w))
+                ≡⟨  ≡-cong ( λ k → ( FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
+                   (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) k , v)) , w))  ) ) φunitr ⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
-                   (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , FMap F id v)) , FMap F id w))
+                   ( (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w))
+                ≡⟨  ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
+                   (k u , v)) , w)) )  (sym ( IsFunctor.distr (isFunctor F )))  ⟩
+                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
+                   ( FMap F (λ x → ((λ y f g x₁ → f (g x₁)) unit x) ) u , v)) , w))
                 ≡⟨⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
-                   (FMap F ( λ y → (λ f g x → f (g x)) (proj₂ y ) ) (φ ( unit , u)) , FMap F id v)) , FMap F id w))
-                ≡⟨  {!!} ⟩
-                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (
-                   FMap F ( map (  λ y → (λ f g x → f (g x)) (proj₂ y ) ) id ) ( φ ( φ ( unit , u) , v))) , FMap F id w))
-                ≡⟨  {!!} ⟩
-                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (
-                     FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((  map (  λ y → (λ f g x → f (g x)) (proj₂ y ) ) id ) x)) ( φ ( φ ( unit , u) , v))
-                       , FMap F id w))
+                   ( FMap F (λ x g h → x (g h) ) u , v)) , w))
+                ≡⟨  ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( FMap F (λ x g h → x (g h) ) u , k)) , w))   ) u→F  ⟩
+                     FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x g h → x (g h)) u , FMap F id v)) , w))
+                ≡⟨  ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w))  )  φ→F  ⟩
+                     FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x g h → x (g h)) id) (φ (u , v)) , w))
                 ≡⟨⟩
-                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (
-                     FMap F ( λ z → ((( λ f g x → f (g x)) (proj₂ (proj₁ z))) ( proj₂ z ))) ( φ ( φ ( unit , u) , v))
-                       , FMap F id w))
+                     FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w))
+                ≡⟨  ≡-cong ( λ k →  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k))  ) u→F  ⟩
+                     FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , FMap F id w))
+                ≡⟨  φ→F  ⟩
+                     FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id) (φ (φ (u , v) , w))
                 ≡⟨⟩
-                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (
-                     FMap F ( λ z → ( λ x → (proj₂ (proj₁ z)) (( proj₂ z ) x ))) ( φ ( φ ( unit , u) , v))
-                       , FMap F id w))
-                ≡⟨  {!!} ⟩
-                 FMap F (λ r → proj₁ r (proj₂ r)) (
-                     FMap F ( map ( λ z → ( λ x → (proj₂ (proj₁ z)) (( proj₂ z ) x ))) id ) ( φ ( φ ( φ ( unit , u) , v) , w )))
-                ≡⟨  {!!} ⟩
-                 FMap F ( λ y → (λ r → proj₁ r (proj₂ r)) (
-                     ( map ( λ z → ( λ x → (proj₂ (proj₁ z)) (( proj₂ z ) x ))) id ) y))  ( φ ( φ ( φ ( unit , u) , v) , w ))
+                    FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w))
+                ≡⟨  ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)) )) (sym (IsFunctor.identity (isFunctor F ))) ⟩
+                    FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F id (φ (φ (u , v) , w)) )
+                ≡⟨  ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F k (φ (φ (u , v) , w)) )  ) (sym (Iso.iso→ (mα-iso isM)))  ⟩
+                    FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F ( (Iso.≅← (mα-iso isM)) o  (Iso.≅→ (mα-iso isM))) (φ (φ (u , v) , w)) )
+                ≡⟨  ≡-cong ( λ k →  FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)))) ( IsFunctor.distr (isFunctor F ))  ⟩
+                    FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F  (Iso.≅← (mα-iso isM)) ( FMap F  (Iso.≅→ (mα-iso isM)) (φ (φ (u , v) , w)) ))
+                ≡⟨ ≡-cong ( λ k →   FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F  (Iso.≅← (mα-iso isM)) k) ) (sym ( IsHaskellMonoidalFunctor.assocφ mono ) ) ⟩
+                     FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w))))
                 ≡⟨⟩
-                 FMap F ( λ y → (( λ z → ( λ x → (proj₂ (proj₁ z)) (( proj₂ z ) x ))) (proj₁ y)) (proj₂ y) )
-                      ( φ ( φ ( φ ( unit , 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 ))) ⟩
+                      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 ( λ x → (proj₂ (proj₁ (proj₁ x))) (( proj₂ (proj₁ x) ) (proj₂ x))) ( φ ( φ ( φ ( unit , u) , v) , w ))
-                ≡⟨ {!!} ⟩
-                 FMap F ( λ x → (proj₁ (proj₁ x)) (( proj₂ (proj₁ x) ) (proj₂ x))) ( φ ( φ ( u , v) , w ))
-                ≡⟨ {!!} ⟩
-                   {!!}
-                ≡⟨ ≡-cong ( λ k → (FMap F ( λ x → (proj₁ x) ((proj₁ (proj₂ x) )(proj₂ (proj₂ x)))) ) k )  ( sym ( IsHaskellMonoidalFunctor.assocφ mono ) ) ⟩
-                 FMap F ( λ x → (proj₁ x) ((proj₁ (proj₂ x) )(proj₂ (proj₂ x))))  ( φ ( u , (φ (v , w))))
+                     FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w)))
                 ≡⟨⟩
                  FMap F ( λ x → (proj₁ x) ((λ r → proj₁ r (proj₂ r)) (  proj₂ x)))  ( φ ( u , (φ (v , w))))
-                ≡⟨  {!!} ⟩
-                 FMap F (λ r → proj₁ r (proj₂ r)) (FMap F (map id (λ r → proj₁ r (proj₂ r))) ( φ ( u , (φ (v , w)))))
-                ≡⟨  {!!} ⟩
+                ≡⟨ sym φ→F ⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
-                ≡⟨  {!!} ⟩
+                ≡⟨   ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) ) (sym u→F ) ⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
               ∎ 
            where