Mercurial > hg > Members > kono > Proof > category

changeset 85:31e1dbbf8800

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Resoution?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Jul 2013 17:51:39 +0900
parents ee25f96ee8cc
children be4e3b073e0d
files nat.agda
diffstat 1 files changed, 4 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sat Jul 27 17:32:32 2013 +0900
+++ b/nat.agda	Sat Jul 27 17:51:39 2013 +0900
@@ -552,7 +552,10 @@
       { U_K : Functor B A } { F_K : Functor A B }
       { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
       { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } 
-      ( Adj : Adjunction A B U_K F_K η_K ε_K )
+      { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } 
+      ( MK :  Monad A (U_K ○ F_K) η_K μ_K )
+      ( AdjK : Adjunction A B U_K F_K η_K ε_K )
+      ( ResK : Resolution A B MK AdjK )
   where
 
         kfmap : {!!}