Mercurial > hg > Members > kono > Proof > category

diff comparison-functor.agda @ 152:5435469c6cf0

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 Sat, 17 Aug 2013 21:08:33 +0900
parents 5f331dfc000b
children d6a6dd305da2
line wrap: on
line diff
--- a/comparison-functor.agda	Sat Aug 17 20:59:31 2013 +0900
+++ b/comparison-functor.agda	Sat Aug 17 21:08:33 2013 +0900
@@ -40,7 +40,7 @@
 -- M =  Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
 M =  Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
 
-open import nat {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } 
+open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } 
 
 open Functor
 open NTrans