Mercurial > hg > Members > kono > Proof > category

changeset 739:ce83d3c28790

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bad case 1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 05 Dec 2017 00:32:54 +0900
parents 15ded3383319
children e3a39aa76368
files monad→monoidal.agda
diffstat 1 files changed, 5 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/monad→monoidal.agda	Mon Dec 04 17:55:40 2017 +0900
+++ b/monad→monoidal.agda	Tue Dec 05 00:32:54 2017 +0900
@@ -29,6 +29,7 @@
          ;   unitarity-idl = {!!}
       }
   } where
+     open import Category.Cat
      T = Monad.T M
      μ = TMap ( Monad.μ M )
      η = TMap ( Monad.η M )
@@ -36,8 +37,11 @@
      _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal Mono) ) x y
      _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d )
      _□_ f g = FMap (Monoidal.m-bi Mono) ( f , g )
+     --                                                        ( T x , T y ) → T ( x , y )
      φab  : (a : Obj (C × C)) → Hom C (FObj (Functor● C C Mono (Monad.T M)) a) (FObj (Functor⊗ C C Mono (Monad.T M)) a)
-     φab (x , y ) = C [ μ (x ⊗ y) o {!!}   ]
+     φab (x , y) =  C [ μ ( x ⊗ y ) o C [ FMap T ( FMap T  ( {!!} □ {!!}  ) ) o  ? ] ]
+     --                     μ
+     --      T (( x , y) ) <-  T ( T (x ,y ) ) <- T (  T (x ,y ), T (1 , 1 ) ) <- ( T (x, 1 ) , T (1, y ) )
 
 import Relation.Binary.PropositionalEquality