Mercurial > hg > Members > kono > Proof > category

comparison 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
comparison
equal deleted inserted replaced
151:3bd5109c83f3 152:5435469c6cf0
38 38
39 M : Monad A (U_K ○ F_K ) η_K μ_K 39 M : Monad A (U_K ○ F_K ) η_K μ_K
40 -- M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK 40 -- M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
41 M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK 41 M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
42 42
43 open import nat {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } 43 open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M }
44 44
45 open Functor 45 open Functor
46 open NTrans 46 open NTrans
47 open KleisliHom 47 open KleisliHom
48 open Adjunction 48 open Adjunction