Mercurial > hg > Members > kono > Proof > category

changeset 58:f321a207f711

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Jul 2013 22:32:53 +0900
parents c6f66c21230c
children a6e31588e2a6
files nat.agda
diffstat 1 files changed, 13 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Wed Jul 24 21:19:27 2013 +0900
+++ b/nat.agda	Wed Jul 24 22:32:53 2013 +0900
@@ -258,19 +258,28 @@
 
 open Adjunction
 
+lemma11 :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'}
+                 ( U : Functor B A ) ( F : Functor A B ) -> NTrans A A ? ? -> NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
+lemma11 U F n = {!!}
+
+UεF :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+                 ( U : Functor B A )
+                 ( F : Functor A B )
+                 ( ε : NTrans B B  ( F ○  U ) identityFunctor ) → NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
+UεF A B U F ε =  lemma11 U F (
+     Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○  U} {identityFunctor} ε F)  )
+
 -- ( \b -> FMap U ( TMap ε ( FObj F b))  )
 Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  { U : Functor B A }
                  { F : Functor A B }
                  { η : NTrans A A identityFunctor ( U ○  F ) }
                  { ε : NTrans B B  ( F ○  U ) identityFunctor } →
-      Adjunction A B U F η ε  → Monad A (U ○  F) η {!!}
+      Adjunction A B U F η ε  → Monad A (U ○  F) η (UεF A B U F ε)
 Adj2Monad A B {U} {F} {η} {ε} adj = record {
          isMonad = record {
                     assoc = {!!};
                     unity1 = {!!};
                     unity2 = {!!}
               }
-      } where
-         UεF : {!!}
-         UεF = Functor*Nat B A U ( Nat*Functor ? {?} ? ε F)
+      }