changeset 774:f3a493da92e8

add simple category version
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 13 Jun 2018 12:56:38 +0900
parents 60942538dc41
children 06a7831cf6ce
files stdalone-kleisli.agda
diffstat 1 files changed, 558 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/stdalone-kleisli.agda	Wed Jun 13 12:56:38 2018 +0900
@@ -0,0 +1,558 @@
+module stdalone-kleisli where
+
+open import Level
+open import Relation.Binary
+open import Relation.Binary.Core
+
+--        h       g       f
+--     a ---→ b ---→ c ---→ d
+--
+
+record IsCategory {l : Level} (  Obj : Set (suc l) ) (Hom : Obj → Obj → Set l )
+     ( _o_ : { a b c : Obj } → Hom b c  → Hom a b →  Hom a c )
+     ( id : ( a  : Obj ) → Hom a a )
+         : Set (suc l) where
+  field
+       idL : { a b : Obj } { f : Hom a b } → ( id b o f ) ≡ f
+       idR : { a b : Obj } { f : Hom a b } → ( f o id a ) ≡ f
+       assoc : { a b c d : Obj } { f : Hom c d }{ g : Hom b c }{ h : Hom a b } →  f o ( g  o h ) ≡ ( f  o g )  o h
+
+record Category {l : Level} : Set (suc (suc l)) where
+  field
+       Obj : Set (suc l)
+       Hom : Obj → Obj → Set l
+       _o_ : { a b c : Obj } → Hom b c  → Hom a b →  Hom a c
+       id : ( a  : Obj ) → Hom a a
+       isCategory : IsCategory Obj Hom _o_ id
+
+Sets : Category
+Sets = record {
+       Obj = Set 
+    ;  Hom =  λ a b → a → b
+    ;  _o_ = λ f g x → f ( g x )
+    ;  id = λ A  x → x
+    ;  isCategory = record {
+           idL = refl
+         ; idR = refl
+         ; assoc = refl
+       }
+   }
+
+
+open Category
+
+_[_o_] :  {l : Level} (C : Category {l} ) → {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c
+C [ f o g ] = Category._o_ C f g
+
+--
+--           f        g
+--       a ----→ b -----→ c
+--       |        |         |
+--      T|       T|        T|
+--       |        |         |
+--       v        v         v
+--      Ta ----→ Tb ----→ Tc
+--           Tf       Tg
+
+
+record IsFunctor {l : Level} (C D : Category {l} )
+                 (FObj : Obj C → Obj D)
+                 (FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B))
+                 : Set (suc l ) where
+  field
+    identity : {A : Obj C} →  FMap (id C A) ≡ id D (FObj A)
+    distr : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
+      → FMap ( C [ g o f ])  ≡ (D [ FMap g o FMap f ] )
+
+record Functor {l : Level} (domain codomain : Category {l} )
+  : Set (suc l) where
+  field
+    FObj : Obj domain → Obj codomain
+    FMap : {A B : Obj domain} → Hom domain A B → Hom codomain (FObj A) (FObj B)
+    isFunctor : IsFunctor domain codomain FObj FMap
+
+open Functor
+
+idFunctor : {l : Level } { C : Category {l} } → Functor C C
+idFunctor = record {
+        FObj = λ x → x
+     ;  FMap = λ f → f
+     ;  isFunctor = record {
+           identity = refl
+         ; distr = refl
+       }
+  }
+
+open  import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+
+_●_ : {l : Level} { A B C : Category {l} }  → ( S : Functor B C ) ( T : Functor A B ) →  Functor A C
+_●_ {l} {A} {B} {C} S T  = record {
+        FObj = λ x → FObj S ( FObj T x )
+     ;  FMap = λ f → FMap S ( FMap T f )
+     ;  isFunctor = record {
+           identity = λ {a} → identity a
+         ; distr = λ {a} {b} {c} {f} {g} → distr
+       }
+   } where
+       identity :  (a : Obj A) → FMap S (FMap T (id A a)) ≡ id C (FObj S (FObj T a))
+       identity a = let open ≡-Reasoning in begin
+              FMap S (FMap T (id A a))
+           ≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.identity (isFunctor T )  ) ⟩
+              FMap S (id B (FObj T a) )
+           ≡⟨ IsFunctor.identity (isFunctor S )   ⟩
+              id C (FObj S (FObj T a))
+           ∎
+       distr : {a b c : Obj A} { f : Hom A a b } { g : Hom A b c } → FMap S (FMap T (A [ g o f ])) ≡ (C [ FMap S (FMap T g) o FMap S (FMap T f) ])
+       distr {a} {b} {c} {f} {g} =  let open ≡-Reasoning in begin
+               FMap S (FMap T (A [ g o f ]))
+           ≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.distr (isFunctor T )  ) ⟩
+               FMap S (  B [ FMap T g o FMap T f ] )
+           ≡⟨  IsFunctor.distr (isFunctor S )    ⟩
+              C [ FMap S (FMap T g) o FMap S (FMap T f) ]
+           ∎
+
+
+--  {A : Set c₁ } {B : Set c₂ } → { f g : A → B }   →  f x  ≡ g x → f  ≡ g
+postulate extensionality : { c₁ c₂ : Level}  → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+
+--
+--            t a 
+--      F a -----→ G a
+--        |           |
+--    Ff  |           | Gf
+--        v           v
+--      F b ------→ G b
+--            t b
+--
+
+record IsNTrans  { l : Level } (D C : Category {l} ) ( F G : Functor D C )
+                 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
+                 : Set (suc l) where
+  field
+    commute : {a b : Obj D} {f : Hom D a b} 
+      →  C [ (  FMap G f ) o  ( TMap a ) ]  ≡ C [ (TMap b ) o  (FMap F f)  ] 
+
+record NTrans  {l : Level} {domain codomain : Category {l} } (F G : Functor domain codomain )
+       : Set (suc l) where
+  field
+    TMap :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
+    isNTrans : IsNTrans domain codomain F G TMap
+
+
+
+open NTrans
+
+--
+--
+--    η   : 1 ------→ T
+--    μ   : TT -----→ T
+--
+--        η                       μT
+--    T -----→ TT          TTT ------→ TT
+--    |         |            |           |
+-- Tη |         |μ        Tμ |           |Tμ
+--    v         |            v           v
+--   TT -----→ T           TT -------→ T
+--        μ                       μT
+
+
+record IsMonad {l : Level} { C : Category {l} } (T : Functor C C) ( η :  NTrans idFunctor T ) ( μ :  NTrans (T ● T) T )
+      : Set (suc l) where
+   field 
+       assoc  : {a : Obj C} → C [ TMap μ a o TMap μ ( FObj T a ) ] ≡  C [  TMap μ a o FMap T (TMap μ a) ] 
+       unity1 : {a : Obj C} → C [ TMap μ a o TMap η ( FObj T a ) ] ≡ id C (FObj T a) 
+       unity2 : {a : Obj C} → C [ TMap μ a o (FMap T (TMap η a ))] ≡ id C (FObj T a) 
+
+
+record Monad {l : Level} { C : Category {l} } (T : Functor C C) : Set (suc l) where
+   field 
+      η : NTrans idFunctor T
+      μ :  NTrans (T ● T) T 
+      isMonad : IsMonad T η μ
+
+record KleisliHom { c : Level} { A : Category {c} } { T : Functor A A } (a : Obj A)  (b : Obj A)
+      : Set c where
+    field
+        KMap :  Hom A a ( FObj T b )
+
+open KleisliHom
+
+                          
+left : {l : Level} (C : Category {l} ) {a b c : Obj C } {f f' : Hom C b c } {g : Hom C a b } →  f ≡ f' → C [ f  o g ] ≡ C [ f'  o g ]
+left {l} C {a} {b} {c} {f} {f'} {g} refl = cong ( λ z → C [ z  o g  ] ) refl
+
+right : {l : Level} (C : Category {l} ) {a b c : Obj C } {f : Hom C b c } {g g' : Hom C a b } →  g ≡ g' → C [ f  o g ] ≡ C [ f  o g' ]
+right {l} C {a} {b} {c} {f} {g} {g'} refl = cong ( λ z → C [ f  o z  ] ) refl
+
+Assoc : {l : Level} (C : Category {l} ) {a b c d : Obj C } {f : Hom C c d } {g : Hom C b c } { h : Hom C a b }
+   → C [ f  o C [ g  o h ] ]  ≡ C [ C [ f   o g ] o h ]
+Assoc {l} C = IsCategory.assoc ( isCategory C )
+
+
+Kleisli : {l : Level} (C : Category {l} ) (T : Functor C C ) ( M : Monad T ) → Category {l}
+Kleisli C T M = record {
+       Obj = Obj C 
+    ;  Hom = λ a b → KleisliHom {_} {C} {T} a b
+    ;  _o_ = λ {a} {b} {c} f g  → join {a} {b} {c} f g
+    ;  id = λ a  → record { KMap = TMap (Monad.η M) a }
+    ;  isCategory = record {
+            idL = idL
+          ; idR = idR
+          ; assoc = assoc
+       }
+  } where
+      join : { a b c : Obj C } → KleisliHom b c → KleisliHom a b → KleisliHom a c
+      join {a} {b} {c} f g = record { KMap =  ( C [ TMap (Monad.μ M) c o  C [ FMap T ( KMap f ) o  KMap g  ] ] ) } 
+      idL : {a b : Obj C} {f : KleisliHom a b} → join (record { KMap = TMap (Monad.η M) b }) f ≡ f
+      idL {a} {b} {f} =  let open ≡-Reasoning in begin
+              record { KMap = C [  TMap (Monad.μ M) b o C [  FMap T (TMap (Monad.η M) b) o KMap f ] ] }
+           ≡⟨ cong ( λ z → record { KMap = z } ) ( begin
+                C [  TMap (Monad.μ M) b o C [  FMap T (TMap (Monad.η M) b) o KMap f ] ]
+             ≡⟨ IsCategory.assoc ( isCategory C ) ⟩
+                C [  C [ TMap (Monad.μ M) b o  FMap T (TMap (Monad.η M) b) ] o KMap f  ]
+             ≡⟨ cong ( λ z → C [ z  o KMap f ] ) ( IsMonad.unity2 (Monad.isMonad M )  )   ⟩
+                C [ id C (FObj T b) o KMap f  ]
+             ≡⟨ IsCategory.idL ( isCategory C ) ⟩
+                KMap f
+             ∎ ) ⟩
+              record { KMap = KMap f }
+            ∎
+      idR : {a b : Obj C} {f : KleisliHom a b} → join f (record { KMap = TMap (Monad.η M) a }) ≡ f
+      idR {a} {b} {f} =  let open ≡-Reasoning in begin
+              record { KMap =  C [ TMap (Monad.μ M) b o C [ FMap T (KMap f) o TMap (Monad.η M) a ] ]  }
+           ≡⟨ cong ( λ z → record { KMap = z } ) ( begin
+                C [ TMap (Monad.μ M) b o C [ FMap T (KMap f) o TMap (Monad.η M) a ] ]
+             ≡⟨  cong ( λ z → C [ TMap (Monad.μ M) b  o z ] ) ( IsNTrans.commute (isNTrans  (Monad.η M) ))  ⟩
+                C [ TMap (Monad.μ M) b o C [ TMap (Monad.η M) (FObj T b) o  KMap f  ] ]
+             ≡⟨  IsCategory.assoc ( isCategory C )  ⟩
+                C [ C [ TMap (Monad.μ M) b o TMap (Monad.η M) (FObj T b) ] o  KMap f  ] 
+             ≡⟨ cong ( λ z → C [ z  o KMap f ] ) ( IsMonad.unity1 (Monad.isMonad M )  )  ⟩
+                C [ id C  (FObj T b)  o  KMap f  ] 
+             ≡⟨ IsCategory.idL ( isCategory C )  ⟩
+                KMap f
+             ∎ ) ⟩
+              record { KMap = KMap f }
+           ∎
+      --
+      --        TMap (Monad.μ M) d ・ (  FMap T (KMap f) ・ (  TMap (Monad.μ M) c ・ (  FMap T (KMap g) ・ KMap h ) ) ) ) 
+      --
+      --      h                T g                       μ c          
+      --   a ---→ T b -----------------→ T T c -------------------------→ T c 
+      --            |                       |                                |
+      --            |                       |                                |
+      --            |                       | T T f     NAT μ                | T f
+      --            |                       |                                |
+      --            |                       v            μ (T d)             v  
+      --            |      distr T       T T T d -------------------------→ T T d 
+      --            |                       |                                |
+      --            |                       |                                |
+      --            |                       | T μ d     Monad-assoc          | μ d
+      --            |                       |                                |
+      --            |                       v                                v
+      --            +------------------→ T T d -------------------------→ T d 
+      --               T (μ d・T f・g)                   μ d
+      --
+      --        TMap (Monad.μ M) d ・ (  FMap T (( TMap (Monad.μ M) d ・ (  FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) )  
+      --
+      _・_ : {a b c : Obj C } ( f : Hom C b c ) ( g : Hom C a b ) → Hom C a c
+      f ・ g  = C [ f  o g ]
+      assoc :  {a b c d : Obj C} {f : KleisliHom c d} {g : KleisliHom b c} {h : KleisliHom a b} → join f (join g h) ≡ join (join f g) h
+      assoc {a} {b} {c} {d} {f} {g} {h} =  let open ≡-Reasoning in begin
+            join f (join g h)
+         ≡⟨⟩
+            record { KMap =  TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・  KMap h ))) }
+         ≡⟨ cong ( λ z → record { KMap = z } ) ( begin
+                 (  TMap (Monad.μ M) d ・ (  FMap T (KMap f) ・ (  TMap (Monad.μ M) c ・ (  FMap T (KMap g) ・ KMap h ) ) ) ) 
+             ≡⟨ right C ( right C (Assoc C)) ⟩
+                 (  TMap (Monad.μ M) d ・ (  FMap T (KMap f) ・ (  ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) ) ) 
+             ≡⟨  Assoc C  ⟩
+                 ( (  TMap (Monad.μ M) d ・  FMap T (KMap f) ) ・  ( ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) ) 
+             ≡⟨  Assoc C  ⟩
+                 ( ( ( TMap (Monad.μ M) d ・  FMap T (KMap f) ) ・  ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) )  ・ KMap h  ) 
+             ≡⟨ sym ( left  C (Assoc C )) ⟩
+                 ( (  TMap (Monad.μ M) d  ・ (  FMap T (KMap f)  ・  ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ) )  ・ KMap h  ) 
+             ≡⟨ left C ( right C (Assoc C)) ⟩
+                 ( (  TMap (Monad.μ M) d  ・ ( ( FMap T (KMap f)   ・  TMap (Monad.μ M) c )  ・  FMap T (KMap g)  ) ) ・ KMap h  ) 
+             ≡⟨ left C (Assoc C)⟩
+                 ( (  ( TMap (Monad.μ M) d  ・  ( FMap T (KMap f)   ・  TMap (Monad.μ M) c ) )  ・  FMap T (KMap g)  ) ・ KMap h  ) 
+             ≡⟨ left C ( left C ( right C  ( IsNTrans.commute (isNTrans  (Monad.μ M) )  ) ))  ⟩
+                ( ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ) ・ FMap T (KMap g) ) ・ KMap h )
+             ≡⟨ sym ( left  C (Assoc C)) ⟩
+                ( ( TMap (Monad.μ M) d ・ ( ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ・ FMap T (KMap g) ) ) ・ KMap h )
+             ≡⟨ sym ( left C ( right  C (Assoc C))) ⟩
+                ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ ( FMap (T ● T) (KMap f) ・ FMap T (KMap g) ) ) ) ・ KMap h )
+             ≡⟨ sym ( left C ( right C (right C (IsFunctor.distr (isFunctor T ) ) ) )) ⟩
+                ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ) ・ KMap h )
+             ≡⟨ left C (Assoc C)  ⟩
+                ( ( ( TMap (Monad.μ M) d ・ TMap (Monad.μ M) (FObj T d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h )
+             ≡⟨ left C (left C ( IsMonad.assoc (Monad.isMonad M ) ) ) ⟩
+                ( ( ( TMap (Monad.μ M) d ・ FMap T (TMap (Monad.μ M) d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h )
+             ≡⟨ sym ( left C (Assoc C)) ⟩
+                ( ( TMap (Monad.μ M) d ・ ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ) ・ KMap h )
+             ≡⟨ sym (Assoc C) ⟩
+                ( TMap (Monad.μ M) d ・ ( ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) )
+             ≡⟨ sym (right C ( left C (IsFunctor.distr (isFunctor T ))))  ⟩
+                 (  TMap (Monad.μ M) d ・ (  FMap T (( TMap (Monad.μ M) d ・ (  FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) )  
+             ∎ ) ⟩
+            record { KMap = (  TMap (Monad.μ M) d ・ (  FMap T (( TMap (Monad.μ M) d ・ (  FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) )  }
+         ≡⟨⟩
+            join (join f g) h
+         ∎
+
+--
+--       U : Kleisli Sets
+--       F : Sets Kleisli   
+--
+--       Hom Klei  a    b     ←---→ Hom Sets a (U●F b )
+--
+--       Hom Klei (F a) (F b) ←---→ Hom Sets a (U●F b )
+--
+--       Hom Klei (F a) b     ←---→  Hom Sets a U(b)                 Hom Klei (F a) b     ←---→  Hom Sets a U(b) 
+--           |                       |                                |                             |
+--         Ff|                      f|                                |f                            |Uf
+--           |                       |                                |                             |
+--           ↓                       ↓                                ↓                             ↓
+--       Hom Klei (F (f a)) b ←---→  Hom Sets (f a) U(b)             Hom Klei (F a) (f b) ←---→  Hom Sets a U(f b) 
+--
+--
+
+record UnityOfOppsite ( Kleisli : Category )  ( U : Functor Kleisli Sets ) ( F : Functor Sets Kleisli ) : Set (suc zero) where
+     field
+         hom-right  : {a : Obj Sets} { b : Obj Kleisli } → Hom Sets a ( FObj U b ) → Hom Kleisli (FObj F a) b
+         hom-left   : {a : Obj Sets} { b : Obj Kleisli } → Hom Kleisli (FObj F a) b   → Hom Sets a ( FObj U b )
+         hom-right-injective : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Sets a (FObj U b) }  → hom-left ( hom-right f ) ≡ f 
+         hom-left-injective  : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Kleisli (FObj F a) b }  → hom-right ( hom-left f ) ≡ f 
+         ---  naturality of Φ
+         hom-left-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } →
+                       { f : Hom Kleisli (FObj F a) b }  → { k : Hom Kleisli b b' } →
+                        hom-left ( Kleisli [ k o  f ] )  ≡ Sets [ FMap U k o hom-left f  ] 
+         hom-left-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } →
+                       { f : Hom Kleisli (FObj F a) b }  → { h : Hom Sets a' a } →
+                        hom-left ( Kleisli [ f  o  FMap F h ] )  ≡  Sets [ hom-left f o h ] 
+     hom-right-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } →
+                       { g : Hom Sets a (FObj U b)}  → { k : Hom Kleisli b b' } →
+                         Kleisli [ k o  hom-right g ]    ≡ hom-right ( Sets [ FMap U k o g  ] ) 
+     hom-right-commute1 {a} {b} {b'} {g} {k} =  let open  ≡-Reasoning  in begin
+            Kleisli [ k o  hom-right g ] 
+         ≡⟨ sym hom-left-injective  ⟩
+            hom-right ( hom-left ( Kleisli [ k o  hom-right g ] ) )
+         ≡⟨ cong ( λ z → hom-right z  ) hom-left-commute1 ⟩
+            hom-right (Sets [ FMap U k o hom-left (hom-right g) ])
+         ≡⟨ cong ( λ z →  hom-right ( Sets [ FMap U k o z ]  ))   hom-right-injective    ⟩
+            hom-right ( Sets [ FMap U k o g  ] )
+         ∎
+     hom-right-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } →
+                       { g : Hom Sets a (FObj U b) }  → { h : Hom Sets a' a } →
+                         Kleisli [ hom-right g  o  FMap F h ]    ≡  hom-right ( Sets [ g o h ] ) 
+     hom-right-commute2 {a} {a'} {b} {g} {h} =  let open  ≡-Reasoning  in begin
+            Kleisli [ hom-right g o FMap F h ]
+         ≡⟨  sym hom-left-injective  ⟩
+            hom-right (hom-left (Kleisli [ hom-right g o FMap F h ]))
+         ≡⟨ cong ( λ z →  hom-right z ) hom-left-commute2  ⟩
+              hom-right (Sets [ hom-left (hom-right g) o h ])
+         ≡⟨ cong ( λ z →  hom-right ( Sets [ z  o h ] )) hom-right-injective   ⟩
+            hom-right (Sets [ g o h ])
+         ∎
+
+
+
+
+_・_ : {a b c : Obj Sets } ( f : Hom Sets b c ) ( g : Hom Sets a b ) → Hom Sets a c
+f ・ g  = Sets [ f  o g ]
+
+U :  ( T : Functor Sets Sets ) → { m : Monad T } → Functor (Kleisli  Sets T m)  Sets
+U T {m} = record {
+       FObj = FObj T
+     ; FMap = λ {a} {b} f x → TMap ( μ m ) b ( FMap T ( KMap f ) x )
+     ; isFunctor = record { identity =  IsMonad.unity2 (isMonad m)  ; distr = distr }
+  } where
+      open Monad
+      distr :  {a b c : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) a b} {g : Hom (Kleisli Sets T m) b c} → 
+           (λ x → TMap (μ m) c (FMap T (KMap (Kleisli Sets T m [ g o f ])) x))
+               ≡ (Sets [ (λ x → TMap (μ m) c (FMap T (KMap g) x)) o (λ x → TMap (μ m) b (FMap T (KMap f) x)) ])  
+      distr {a} {b} {c} {f} {g}  = let open ≡-Reasoning in begin
+            Sets [ TMap (μ m) c o FMap T (KMap (Kleisli Sets T m [ g o f ])) ]
+         ≡⟨⟩
+            Sets [ TMap (μ m) c o FMap T ( Sets [ TMap (μ m) c  o Sets [ FMap T ( KMap g ) o KMap f ] ] ) ]
+         ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} {_} {_} ( IsFunctor.distr (Functor.isFunctor T) )  ⟩
+            Sets [ TMap (μ m) c  o Sets [  FMap T ( TMap (μ m) c) o FMap T ( Sets [ FMap T (KMap g)  o KMap f ] ) ] ] 
+         ≡⟨ sym ( left Sets  (IsMonad.assoc (isMonad m )))  ⟩
+           Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o (FMap T (Sets [ FMap T (KMap g) o KMap f ])) ]
+         ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} ( right Sets {_} {_} {_} {TMap (μ m) (FObj T c)} ( IsFunctor.distr (Functor.isFunctor T) ) ) ⟩
+           Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o Sets [ FMap T ( FMap T (KMap g)) o FMap T ( KMap f ) ] ]
+         ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} ( left Sets (IsNTrans.commute ( NTrans.isNTrans (μ m))))) ⟩
+            Sets [ Sets [ TMap (μ m) c o FMap T (KMap g) ] o Sets [ TMap (μ m) b o FMap T (KMap f) ] ] 
+         ∎
+
+
+F :  ( T : Functor Sets Sets ) → {m : Monad T} → Functor Sets ( Kleisli Sets T m)
+F T {m} = record {
+       FObj = λ a → a ; FMap = λ {a} {b} f → record { KMap = λ x →  TMap (η m) b (f x) }  
+     ; isFunctor = record { identity = refl ; distr = distr }
+  } where
+      open Monad
+      distr : {a b c : Obj Sets} {f : Hom Sets a b} {g : Hom Sets b c} → record { KMap = λ x → TMap (η m) c ((Sets [ g o f ]) x) } ≡
+          Kleisli Sets T m [ record { KMap = λ x → TMap (η m) c (g x) } o record { KMap = λ x → TMap (η m) b (f x) } ]
+      distr {a} {b} {c} {f} {g}  = let open ≡-Reasoning in ( cong ( λ z → record { KMap = z } ) ( begin
+           Sets [ TMap (η m) c o Sets [ g o f ] ]
+         ≡⟨ left Sets {_} {_} {_} {Sets [ TMap (η m) c o g ] } ( sym ( IsNTrans.commute ( NTrans.isNTrans (η m) ) ))  ⟩
+           Sets [ Sets [ FMap T g  o TMap (η m) b ]  o f ]
+         ≡⟨ sym ( IsCategory.idL ( Category.isCategory Sets )) ⟩
+           Sets [ ( λ x → x ) o Sets [ Sets [ FMap T g  o TMap (η m) b ]  o f ] ]
+         ≡⟨ sym ( left Sets  (IsMonad.unity2 (isMonad m ))) ⟩
+            Sets [ Sets [ TMap (μ m) c o FMap T (TMap (η m) c) ] o Sets [ FMap T g o  Sets [ TMap (η m) b o f ] ] ]
+         ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} {_} ( left Sets {_} {_} {_} { FMap T (Sets [ TMap (η m) c  o g ] )} ( IsFunctor.distr (Functor.isFunctor T) )))  ⟩
+           Sets [ TMap (μ m) c o ( Sets [  FMap T (Sets [ TMap (η m) c  o g ] ) o Sets [ TMap (η m) b  o f ] ] ) ]
+         ∎ ))
+
+--
+--   Hom Sets     a         (FObj U b)   = Hom Sets a (T b)
+--   Hom Kleisli (FObj F a) b            = Hom Sets a (T b)
+--
+
+lemma→ :  ( T : Functor Sets Sets ) → (m : Monad T ) → UnityOfOppsite (Kleisli Sets T m) (U T {m} ) (F T {m})
+lemma→ T m =
+     let open Monad in
+      record {
+          hom-right  = λ {a} {b} f → record { KMap = f }
+       ;  hom-left   = λ {a} {b} f x → TMap (μ m) b ( TMap ( η m ) (FObj T b) ( (KMap f) x ) )
+       ;  hom-right-injective = hom-right-injective
+       ;  hom-left-injective = hom-left-injective
+       ;  hom-left-commute1 = hom-left-commute1
+       ;  hom-left-commute2 =  hom-left-commute2 
+     } where
+         open Monad 
+         hom-right-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)}
+                {f : Hom Sets a (FObj (U T {m}) b)} → (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (f x))) ≡ f
+         hom-right-injective {a} {b} {f} = let open ≡-Reasoning in begin
+             Sets [ TMap (μ m) b  o Sets [ TMap (η m) (FObj T b)  o f ] ]
+           ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m )  )  ⟩
+             Sets [ id Sets (FObj (U T {m}) b)  o f ] 
+           ≡⟨ IsCategory.idL ( isCategory Sets )  ⟩
+             f
+           ∎
+         hom-left-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b}
+            → record { KMap = λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x)) } ≡ f
+         hom-left-injective {a} {b} {f} = let open ≡-Reasoning in cong ( λ z → record { KMap = z } ) ( begin
+              Sets [ TMap (μ m) b  o Sets [ TMap (η m) (FObj T b)  o KMap f ] ]
+           ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m ) )  ⟩
+             KMap f
+           ∎ )
+         hom-left-commute1 : {a : Obj Sets} {b b' : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {k : Hom (Kleisli Sets T m) b b'} →
+               (λ x → TMap (μ m) b' (TMap (η m) (FObj T b') (KMap (Kleisli Sets T m [ k o f ]) x)))
+                  ≡ (Sets [ FMap (U T {m}) k o (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) ])
+         hom-left-commute1 {a} {b} {b'} {f} {k} = let open ≡-Reasoning in begin
+              Sets [ TMap (μ m) b'  o Sets [ TMap (η m) (FObj T b')  o KMap (Kleisli Sets T m [ k o f ] ) ] ]
+            ≡⟨⟩
+              TMap (μ m) b'  ・ ( TMap (η m) (FObj T b')  ・ ( TMap (μ m) b' ・ ( FMap T (KMap k)  ・ KMap f  )))
+            ≡⟨ left Sets  ( IsMonad.unity1 ( isMonad m ))  ⟩
+              TMap (μ m) b'  ・ ( FMap T (KMap k)  ・  KMap f  )
+            ≡⟨ right Sets {_} {_} {_} {TMap ( μ m ) b' ・ FMap T ( KMap k )} ( left Sets ( sym ( IsMonad.unity1 ( isMonad m )  )  ) )  ⟩
+              ( TMap ( μ m ) b' ・ FMap T ( KMap k ) ) ・ ( TMap (μ m) b  ・ ( TMap (η m) (FObj T b)  ・ KMap f ) ) 
+            ≡⟨⟩
+              Sets [ FMap (U T {m}) k o Sets [ TMap (μ m) b  o Sets [ TMap (η m) (FObj T b)  o KMap f ] ] ]
+            ∎ 
+         hom-left-commute2 :   {a a' : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {h : Hom Sets a' a} →
+                (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ]) x)))
+                    ≡ (Sets [ (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) o h ])
+         hom-left-commute2 {a} {a'} {b} {f} {h} = let open ≡-Reasoning in begin
+              TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ])))
+            ≡⟨⟩
+              TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ ( (TMap (μ m) b ・ FMap T  (KMap f) ) ・ ( TMap (η m) a ・ h )))
+            ≡⟨  left Sets (IsMonad.unity1 ( isMonad m ))  ⟩
+              (TMap (μ m) b ・ FMap T  (KMap f) ) ・ ( TMap (η m) a ・ h )
+            ≡⟨  right Sets {_} {_} {_} {TMap (μ m) b} ( left Sets ( IsNTrans.commute ( isNTrans (η m)  )))    ⟩
+              TMap (μ m) b ・ (( TMap (η m) (FObj T  b)・ KMap f ) ・ h )
+            ∎
+
+
+
+lemma← :  ( U F : Functor Sets Sets ) → UnityOfOppsite Sets U F → Monad ( U ● F )
+lemma← U F uo = record {
+       η = η
+    ;  μ = μ
+    ;  isMonad = record {
+            unity1 = unity1
+          ; unity2 = unity2
+          ; assoc = assoc
+       }
+  } where
+     open UnityOfOppsite
+     T =  U ● F
+     η-comm : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ FMap (U ● F) f o (λ x → hom-left uo (λ x₁ → x₁) x) ]
+               ≡ Sets [  (λ x → hom-left uo (λ x₁ → x₁) x) o FMap (idFunctor {_} {Sets} ) f ]
+     η-comm {a} {b} {f} = let open ≡-Reasoning in begin
+             FMap (U ● F) f ・ (hom-left uo (λ x₁ → x₁) )
+         ≡⟨ sym (hom-left-commute1 uo) ⟩
+             hom-left uo ( FMap F f ・ (λ x₁ → x₁) )
+         ≡⟨ hom-left-commute2 uo ⟩
+             hom-left uo (λ x₁ → x₁)  ・ FMap ( idFunctor {_} {Sets} ) f 
+         ∎
+     η :  NTrans (idFunctor {_} {Sets}) T
+     η =  record { TMap = λ a x → (hom-left uo) (λ x → x ) x ; isNTrans = record { commute = η-comm  } }
+     μ-comm : {a b : Obj Sets} {f : Hom Sets a b} → (Sets [ FMap T f o (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) ])
+         ≡ (Sets [ (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) o FMap (T ● T) f ])
+     μ-comm {a} {b} {f} = let open ≡-Reasoning in begin
+            FMap T f ・  FMap U (hom-right uo (λ x₁ → x₁)) 
+         ≡⟨⟩
+            FMap U (FMap F f ) ・  FMap U (hom-right uo (λ x₁ → x₁)) 
+         ≡⟨ sym ( IsFunctor.distr ( Functor.isFunctor U)) ⟩
+            FMap U (FMap F f  ・ hom-right uo (λ x₁ → x₁)) 
+         ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute1 uo) ⟩
+            FMap U ( hom-right uo (FMap U (FMap F f) ・ (λ x₁ → x₁) ) )
+         ≡⟨ sym ( cong ( λ z → FMap U z ) (hom-right-commute2 uo)) ⟩
+            FMap U ((hom-right uo (λ x₁ → x₁))  ・ (FMap F (FMap U (FMap F f ))))
+         ≡⟨  IsFunctor.distr ( Functor.isFunctor U) ⟩
+            FMap U (hom-right uo (λ x₁ → x₁))  ・ FMap U (FMap F (FMap U (FMap F f )))
+         ≡⟨⟩
+            FMap U (hom-right uo (λ x₁ → x₁))  ・ FMap (T ● T) f
+         ∎
+     μ :  NTrans (T ● T) T
+     μ = record { TMap = λ a x → FMap U ( hom-right uo  (λ x → x)) x ; isNTrans = record { commute = μ-comm  } }
+     unity1 : {a : Obj Sets} → (Sets [ TMap μ a o TMap η (FObj (U ● F) a) ]) ≡ id Sets (FObj (U ● F) a)
+     unity1 {a} =  let open ≡-Reasoning in begin
+            TMap μ a ・ TMap η (FObj (U ● F) a)
+         ≡⟨⟩
+             FMap U (hom-right uo (λ x₁ → x₁)) ・ hom-left uo (λ x₁ → x₁)
+         ≡⟨ sym  (hom-left-commute1 uo )  ⟩
+             hom-left uo ( hom-right uo (λ x₁ → x₁) ・ (λ x₁ → x₁) )
+         ≡⟨  hom-right-injective uo  ⟩
+            id Sets (FObj (U ● F) a)
+         ∎
+     unity2 : {a : Obj Sets} →  (Sets [ TMap μ a o FMap (U ● F) (TMap η a) ]) ≡ id Sets (FObj (U ● F) a)
+     unity2 {a} =  let open ≡-Reasoning in begin
+            TMap μ a ・ FMap (U ● F) (TMap η a)
+         ≡⟨⟩
+            FMap U (hom-right uo (λ x₁ → x₁)) ・  FMap U (FMap F (hom-left uo (λ x₁ → x₁)))
+         ≡⟨ sym ( IsFunctor.distr (isFunctor U))  ⟩
+            FMap U (hom-right uo (λ x₁ → x₁) ・  FMap F (hom-left uo (λ x₁ → x₁)))
+         ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute2  uo)  ⟩
+             FMap U (hom-right uo ((λ x₁ → x₁) ・ hom-left uo (λ x₁ → x₁) ))
+         ≡⟨ cong ( λ z → FMap U z ) (hom-left-injective  uo)  ⟩
+             FMap U ( id Sets (FObj F a) )
+         ≡⟨   IsFunctor.identity (isFunctor U) ⟩
+            id Sets (FObj (U ● F) a)
+         ∎
+     assoc : {a : Obj Sets} → (Sets [ TMap μ a o TMap μ (FObj (U ● F) a) ]) ≡ (Sets [ TMap μ a o FMap (U ● F) (TMap μ a) ])
+     assoc {a} =  let open ≡-Reasoning in begin
+            TMap μ a ・ TMap μ (FObj (U ● F) a)
+         ≡⟨⟩
+            FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (hom-right uo (λ x₁ → x₁))
+         ≡⟨ sym ( IsFunctor.distr (isFunctor U ))   ⟩  
+            FMap U (hom-right uo (λ x₁ → x₁) ・ hom-right uo (λ x₁ → x₁))
+         ≡⟨ cong ( λ z → FMap U z ) ( hom-right-commute1 uo  )   ⟩
+            FMap U (hom-right uo ((λ x₁ → x₁) ・ FMap U  (hom-right uo (λ x₁ → x₁))) ) 
+         ≡⟨ sym ( cong ( λ z → FMap U z ) ( hom-right-commute2 uo  )  ) ⟩
+            FMap U (hom-right uo (λ x₁ → x₁) ・ FMap F (FMap U (hom-right uo (λ x₁ → x₁))))
+         ≡⟨  IsFunctor.distr (isFunctor U )   ⟩
+            FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (hom-right uo (λ x₁ → x₁))))
+         ≡⟨⟩
+            TMap μ a ・ FMap (U ● F) (TMap μ a) 
+         ∎
+
+
+
+
+
+