Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 710:359f34ed60ff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 23 Nov 2017 11:40:12 +0900
parents 2807335e3fa0
children bb5b028489dc
comparison
equal deleted inserted replaced
709:2807335e3fa0 710:359f34ed60ff
350 mρ← : {a : Obj Sets} → Hom Sets a ( a ⊗ One ) 350 mρ← : {a : Obj Sets} → Hom Sets a ( a ⊗ One )
351 mρ← a = ( a , OneObj ) 351 mρ← a = ( a , OneObj )
352 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x 352 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x
353 mρiso (_ , OneObj ) = refl 353 mρiso (_ , OneObj ) = refl
354 354
355 355 ≡-cong = Relation.Binary.PropositionalEquality.cong
356 356
357 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) 357 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
358 : Set (suc (suc c₁)) where 358 : Set (suc (suc c₁)) where
359 field 359 field
360 unit : FObj f One 360 unit : FObj f One
367 MF = F 367 MF = F
368 ; ψ = λ _ → HaskellMonoidalFunctor.unit mf 368 ; ψ = λ _ → HaskellMonoidalFunctor.unit mf
369 ; isMonodailFunctor = record { 369 ; isMonodailFunctor = record {
370 φab = record { TMap = λ x → φ x ; isNTrans = record { commute = comm0 } } 370 φab = record { TMap = λ x → φ x ; isNTrans = record { commute = comm0 } }
371 ; associativity = comm1 371 ; associativity = comm1
372 ; unitarity-idr = comm2 372 ; unitarity-idr = λ {a b} → comm2 {a} {b}
373 ; unitarity-idl = comm3 373 ; unitarity-idl = λ {a b} → comm3 {a} {b}
374 } 374 }
375 } where 375 } where
376 open Monoidal 376 open Monoidal
377 open IsMonoidal hiding ( _■_ ; _□_ ) 377 open IsMonoidal hiding ( _■_ ; _□_ )
378 M = MonoidalSets 378 M = MonoidalSets
382 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y 382 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
383 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d ) 383 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
384 _□_ f g = FMap (m-bi M) ( f , g ) 384 _□_ f g = FMap (m-bi M) ( f , g )
385 φ : (x : Obj (Sets × Sets) ) → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x) 385 φ : (x : Obj (Sets × Sets) ) → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
386 φ _ z = HaskellMonoidalFunctor.φ mf z 386 φ _ z = HaskellMonoidalFunctor.φ mf z
387 comm00 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
388 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ a ]) x ≡ (Sets [ φ b o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
389 comm00 {a} {b} {(f , g)} (x , y) = begin
390 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ((φ a) (x , y))
391 ≡⟨⟩
392 (FMap F ( f □ g ) ) ((φ a) (x , y))
393 ≡⟨⟩
394 FMap F ( map f g ) ((φ a) (x , y))
395 ≡⟨ {!!} ⟩
396 (φ b ) ( FMap F f x , FMap F g y )
397 ≡⟨⟩
398 (φ b ) ( ( FMap F f □ FMap F g ) (x , y) )
399 ≡⟨⟩
400 (φ b ) ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) )
401 ∎
402 where
403 open import Relation.Binary.PropositionalEquality
404 open ≡-Reasoning
387 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ a ] 405 comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ a ]
388 ≈ Sets [ φ b o FMap (Functor● Sets Sets MonoidalSets F) f ] ] 406 ≈ Sets [ φ b o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
389 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → {!!} ) 407 comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
408 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 ≡
409 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ ((a ⊗ b) , c) o φ (a , b) □ id1 Sets (FObj F c) ] ]) x
410 comm10 {x} {y} {f} ((a , b) , c ) = begin
411 ( φ (x , (y ⊗ f))) (( id1 Sets (FObj F x) □ φ (y , f) ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
412 ≡⟨⟩
413 ( φ (x , (y ⊗ f))) ( a , φ (y , f) (b , c))
414 ≡⟨ {!!} ⟩
415 ( FMap F (Iso.≅→ (mα-iso isM))) (( φ ((x ⊗ y) , f) ) (( φ (x , y) (a , b)) , c ))
416 ≡⟨⟩
417 ( FMap F (Iso.≅→ (mα-iso isM))) (( φ ((x ⊗ y) , f) ) (( φ (x , y) □ id1 Sets (FObj F f) ) ((a , b) , c)))
418 ∎
419 where
420 open import Relation.Binary.PropositionalEquality
421 open ≡-Reasoning
390 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ (a , (b ⊗ c)) 422 comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ (a , (b ⊗ c))
391 o Sets [ (id1 Sets (FObj F a) □ φ (b , c)) o Iso.≅→ (mα-iso isM) ] ] 423 o Sets [ (id1 Sets (FObj F a) □ φ (b , c)) o Iso.≅→ (mα-iso isM) ] ]
392 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ (a ⊗ b , c) o (φ (a , b) □ id1 Sets (FObj F c)) ] ] ] 424 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ (a ⊗ b , c) o (φ (a , b) □ id1 Sets (FObj F c)) ] ] ]
393 comm1 {a} {b} {c} = extensionality Sets ( λ x → {!!} ) 425 comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x )
394 comm2 : {a b : Obj Sets} → Sets [ Sets [ 426 comm2 : {a b : Obj Sets} → Sets [ Sets [
395 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ (a , m-i MonoidalSets) o 427 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ (a , m-i MonoidalSets) o
396 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] 428 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
397 comm2 {a} {b} = extensionality Sets ( λ x → {!!} ) 429 comm2 {a} {b} = extensionality Sets ( λ x → {!!} )
398 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o 430 comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o