Mercurial > hg > Members > kono > Proof > category
changeset 710:359f34ed60ff
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 23 Nov 2017 11:40:12 +0900 |
| parents | 2807335e3fa0 |
| children | bb5b028489dc |
| files | monoidal.agda |
| diffstat | 1 files changed, 37 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/monoidal.agda Thu Nov 23 10:47:46 2017 +0900 +++ b/monoidal.agda Thu Nov 23 11:40:12 2017 +0900 @@ -352,7 +352,7 @@ mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x mρiso (_ , OneObj ) = refl - +≡-cong = Relation.Binary.PropositionalEquality.cong record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) : Set (suc (suc c₁)) where @@ -369,8 +369,8 @@ ; isMonodailFunctor = record { φab = record { TMap = λ x → φ x ; isNTrans = record { commute = comm0 } } ; associativity = comm1 - ; unitarity-idr = comm2 - ; unitarity-idl = comm3 + ; unitarity-idr = λ {a b} → comm2 {a} {b} + ; unitarity-idl = λ {a b} → comm3 {a} {b} } } where open Monoidal @@ -384,13 +384,45 @@ _□_ f g = FMap (m-bi M) ( f , g ) φ : (x : Obj (Sets × Sets) ) → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x) φ _ z = HaskellMonoidalFunctor.φ mf z + 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 φ a ]) x ≡ (Sets [ φ b 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) ) ((φ a) (x , y)) + ≡⟨⟩ + (FMap F ( f □ g ) ) ((φ a) (x , y)) + ≡⟨⟩ + FMap F ( map f g ) ((φ a) (x , y)) + ≡⟨ {!!} ⟩ + (φ b ) ( FMap F f x , FMap F g y ) + ≡⟨⟩ + (φ b ) ( ( FMap F f □ FMap F g ) (x , y) ) + ≡⟨⟩ + (φ b ) ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) ) + ∎ + where + open import Relation.Binary.PropositionalEquality + open ≡-Reasoning comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ a ] ≈ Sets [ φ b o FMap (Functor● Sets Sets MonoidalSets F) f ] ] - comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → {!!} ) + comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x ) + comm10 : {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ (a , (b ⊗ c)) o Sets [ id1 Sets (FObj F a) □ φ (b , c) o Iso.≅→ (mα-iso isM) ] ]) x ≡ + (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ ((a ⊗ b) , c) o φ (a , b) □ id1 Sets (FObj F c) ] ]) x + comm10 {x} {y} {f} ((a , b) , c ) = begin + ( φ (x , (y ⊗ f))) (( id1 Sets (FObj F x) □ φ (y , f) ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) + ≡⟨⟩ + ( φ (x , (y ⊗ f))) ( a , φ (y , f) (b , c)) + ≡⟨ {!!} ⟩ + ( FMap F (Iso.≅→ (mα-iso isM))) (( φ ((x ⊗ y) , f) ) (( φ (x , y) (a , b)) , c )) + ≡⟨⟩ + ( FMap F (Iso.≅→ (mα-iso isM))) (( φ ((x ⊗ y) , f) ) (( φ (x , y) □ id1 Sets (FObj F f) ) ((a , b) , c))) + ∎ + where + open import Relation.Binary.PropositionalEquality + open ≡-Reasoning comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ (a , (b ⊗ c)) o Sets [ (id1 Sets (FObj F a) □ φ (b , c)) o Iso.≅→ (mα-iso isM) ] ] ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ (a ⊗ b , c) o (φ (a , b) □ id1 Sets (FObj F c)) ] ] ] - comm1 {a} {b} {c} = extensionality Sets ( λ x → {!!} ) + comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x ) comm2 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ (a , m-i MonoidalSets) o FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]