Members/kono/Proof/category: monoidal.agda comparison

comparison monoidal.agda @ 715:1be42267eeee

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

comparison

equal deleted inserted replaced

-:bc21e89cd273
+:1be42267eeee
 : Set (suc (suc c₁)) where
 isM  : IsMonoidal (Sets {c₁}) One SetsTensorProduct
 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
+idrφ : {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
+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 )
 -- left identity         fmap snd (φ unit v) = v
 -- right identity        fmap fst (φ u unit) = u
 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) (φ  (x , y))
 ≡⟨⟩
 (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) )
 ≡⟨⟩
 φ ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) )
 (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)))
 ≡⟨⟩
 φ  ( 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)))
 ∎
 where
 comm20 : {a b : Obj Sets} ( x : FObj F a * One )  → (  Sets [
 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
 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 )
 ∎
 where
 comm30 : {a b : Obj Sets} ( x : One * FObj F b )  → (  Sets [
 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ  o
 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 )
 ∎
 where
 where
 open HaskellMonoidalFunctor
 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
 ; homomorphism = homomorphism
 ; interchange = interchange
 where
 id : { a : Obj Sets } → a → a
 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 ) )
+( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ (  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 )))
+≡⟨   ≡-cong ( λ k → ( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ ( FMap F ( λ y → id ) unit  ,  k  ))) unit→F  ⟩
-(  IsFunctor.identity ( Functor.isFunctor F ) ) ) ⟩
+( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ (  FMap F ( λ y → id ) unit  , FMap F id u ) )
-( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ (  FMap F ( λ y → id ) unit  , FMap F id u ) )
+≡⟨ φ→F ⟩
-≡⟨ 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 (λ x → proj₂ x ) (φ (unit , u ) )
 ≡⟨⟩
 FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u ))
-≡⟨  IsHaskellMonoidalFunctor.law4 mono   ⟩
+≡⟨  IsHaskellMonoidalFunctor.idlφ mono   ⟩
 u
 ∎
 where
 open Relation.Binary.PropositionalEquality.≡-Reasoning
 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 (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
-(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 (λ 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 (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
-(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 (λ 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 (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
-(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 (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 (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
-(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 ( λ 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 (λ r → proj₁ r (proj₂ r)) (φ (
-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 ( λ 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 (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (
+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)) (φ (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 ( λ 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 ( λ 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
 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
 homomorphism = {!!}

Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 715:1be42267eeee