Mercurial > hg > Members > kono > Proof > category

changeset 715:1be42267eeee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some tools
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Nov 2017 11:32:41 +0900
parents bc21e89cd273
children 35457f9568f3
files monoidal.agda
diffstat 1 files changed, 79 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/monoidal.agda	Thu Nov 23 20:18:09 2017 +0900
+++ b/monoidal.agda	Fri Nov 24 11:32:41 2017 +0900
@@ -363,12 +363,12 @@
   isM = Monoidal.isMonoidal MonoidalSets 
   open IsMonoidal
   field
-          law1 : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d  }
+          natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d  }
              → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
-          law2 : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
+          assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
              → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c))
-          law3 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
-          law4 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
+          idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
+          idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
 
 --   http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
 -- naturality of φ       fmap(f × g)(φ u v) = φ ( fmap f u) ( fmap g v )
@@ -417,7 +417,7 @@
                  (FMap F ( f □ g ) ) (φ  (x , y))
              ≡⟨⟩
                  FMap F ( map f g ) (φ  (x , y))
-             ≡⟨ IsHaskellMonoidalFunctor.law1 ismf ⟩
+             ≡⟨ IsHaskellMonoidalFunctor.natφ ismf ⟩
                  φ (  FMap F  f x , FMap F g  y )
              ≡⟨⟩
                  φ ( (  FMap F  f □ FMap F g ) (x , y) )
@@ -435,7 +435,7 @@
                   φ  (( id1 Sets (FObj F x) □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
                ≡⟨⟩
                   φ  ( a , φ  (b , c)) 
-               ≡⟨ IsHaskellMonoidalFunctor.law2 ismf ⟩
+               ≡⟨ IsHaskellMonoidalFunctor.assocφ ismf ⟩
                  ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  (a , b)) , c ))
                ≡⟨⟩
                  ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  □  id1 Sets (FObj F f) ) ((a , b) , c)))
@@ -451,7 +451,7 @@
              FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x  ≡ Iso.≅→ (mρ-iso isM) x
       comm20 {a} {b} (x , OneObj ) =  begin 
                  (FMap F (Iso.≅→ (mρ-iso isM))) ( φ  ( x , unit ) )
-               ≡⟨ IsHaskellMonoidalFunctor.law3 ismf ⟩
+               ≡⟨ IsHaskellMonoidalFunctor.idrφ ismf ⟩
                  x
                ≡⟨⟩
                  Iso.≅→ (mρ-iso isM) ( x , OneObj )
@@ -467,7 +467,7 @@
              FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x  ≡ Iso.≅→ (mλ-iso isM) x
       comm30 {a} {b} ( OneObj , x) =  begin 
                  (FMap F (Iso.≅→ (mλ-iso isM))) ( φ  ( unit , x ) )
-               ≡⟨ IsHaskellMonoidalFunctor.law4 ismf ⟩
+               ≡⟨ IsHaskellMonoidalFunctor.idlφ ismf ⟩
                  x
                ≡⟨⟩
                  Iso.≅→ (mλ-iso isM) (  OneObj , x )
@@ -517,15 +517,14 @@
      pure  :  {a : Obj Sets} → Hom Sets a ( FObj F a )
      pure {a} x = FMap F ( λ y → x ) (unit mono)
      <*> :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b        --  ** mono  x y 
-     <*> {a} {b} x y = FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  (φ mono ( x , y ))
+     <*> {a} {b} x y = FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ mono ( x , y ))
 
-open Relation.Binary.PropositionalEquality
 
 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
       ( unit  : FObj F One )
       ( φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) ) )
       ( mono : IsHaskellMonoidalFunctor F unit φ ) 
-         → IsApplicative F (λ x →  FMap F ( λ y → x ) unit) (λ x y → FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  (φ ( x , y )))
+         → IsApplicative F (λ x →  FMap F ( λ y → x ) unit) (λ x y → FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ ( x , y )))
 HaskellMonoidal→Applicative {c₁} F unit φ mono = record {
           identity = identity 
         ; composition = composition
@@ -537,30 +536,45 @@
           id x = x
           isM  : IsMonoidal (Sets {c₁}) One SetsTensorProduct  
           isM = Monoidal.isMonoidal MonoidalSets 
-          open IsMonoidal
           pure  :  {a : Obj Sets} → Hom Sets a ( FObj F a )
           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 ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  (φ ( x , y ))
+          _<*>_ {a} {b} x y = FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ ( x , y ))
           _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
           _・_ f g = λ x → f ( g x ) 
+          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 
+          open Relation.Binary.PropositionalEquality
+          φ→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d }
+              { f : Hom Sets (c * d) e }
+                   { x :  FObj F a } { y :  FObj F b }
+              →  FMap F f ( φ ( FMap F g x , FMap F h y ) )  ≡  FMap F (  f o map g h ) ( φ ( x , y ) ) 
+          φ→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin
+                  FMap F (  f o map g h ) ( φ ( x , y ) ) 
+               ≡⟨  ≡-cong ( λ k → k ( φ ( x , y ))) ( IsFunctor.distr (isFunctor F) ) ⟩
+                  FMap F  f (( FMap F ( map g h ) ) ( φ ( x , y )))
+               ≡⟨  ≡-cong ( λ k → FMap F f k ) ( IsHaskellMonoidalFunctor.natφ mono )  ⟩
+                  FMap F f ( φ ( FMap F g x , FMap F h y ) )
+             ∎  )
+           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 ) ) )
+          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 ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ (  FMap F ( λ y → id ) unit  , u ) )
-               ≡⟨  sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ ( FMap F ( λ y → id ) unit  ,  k u )))
-                    (  IsFunctor.identity ( Functor.isFunctor F ) ) ) ⟩
-                 ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ (  FMap F ( λ y → id ) unit  , FMap F id u ) )
-               ≡⟨ sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) k  )  (  IsHaskellMonoidalFunctor.law1 mono  ) )  ⟩
-                   FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y → id) id) (φ (unit , u )))
-               ≡⟨  ≡-cong ( λ k → k  (φ (unit , u ) )) ( sym ( IsFunctor.distr ( Functor.isFunctor F ) ) )  ⟩
-                   FMap F (λ x →  (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y → id) id) x )) (φ (unit , 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  ⟩
+                 ( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ (  FMap F ( λ y → id ) unit  , FMap F id u ) )
+               ≡⟨ φ→F ⟩
                    FMap F (λ x → proj₂ x ) (φ (unit , u ) )
                ≡⟨⟩
                    FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u ))
-               ≡⟨  IsHaskellMonoidalFunctor.law4 mono   ⟩
+               ≡⟨  IsHaskellMonoidalFunctor.idlφ mono   ⟩
                   u
              ∎ 
            where
@@ -568,33 +582,60 @@
           composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
               → (( pure _・_ <*> u ) <*> v ) <*> w  ≡ u  <*> (v  <*> w)
           composition {a} {b} {c} {u} {v} {w} = begin
-                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
-                   (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ y f g x → f (g x)) unit , u)) , v)) , w))
+                 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))
                 ≡⟨  {!!} ⟩
-                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
-                   (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (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 (λ 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 (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
-                   (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y f g x → f (g x)) id ) (φ ( 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 (λ 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 (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
-                   (FMap F ( λ x → (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( 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 ( λ 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 (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
+                 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 (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (
+                 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 (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (
-                     FMap F ( λ x → (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((  map (  λ y → (λ f g x → f (g x)) (proj₂ y ) ) id ) x)) ( φ ( φ ( unit , u) , v))
+                 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 (λ 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 (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (
-                     FMap F ( λ z → ((( λ f g x → f (g x)) (proj₂ (proj₁ z))) ( proj₂ z ))) ( φ ( φ ( unit , u) , v))
+                 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 (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (u , FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (v , 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 ( λ y → (( λ z → ( λ x → (proj₂ (proj₁ z)) (( proj₂ z ) x ))) (proj₁ y)) (proj₂ y) )
+                      ( φ ( φ ( φ ( unit , 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 ( λ 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)))))
+                ≡⟨  {!!} ⟩
+                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
+                ≡⟨  {!!} ⟩
+                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
               ∎ 
            where
                   open Relation.Binary.PropositionalEquality.≡-Reasoning