Mercurial > hg > Members > kono > Proof > category

comparison comparison-functor.agda @ 465:d3cd28a71b3f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Mar 2017 16:26:57 +0900
parents 93cf0a6c21fe
children a5f2ca67e7c5
comparison
equal deleted inserted replaced
464:037af9cf038c 465:d3cd28a71b3f
25 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) } 25 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
26 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } 26 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor }
27 { μ_K' : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } 27 { μ_K' : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) }
28 ( AdjK : Adjunction A B U_K F_K η_K ε_K ) 28 ( AdjK : Adjunction A B U_K F_K η_K ε_K )
29 ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K'} AdjK ) 29 ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K'} AdjK )
30 where 30 where
31 31
32 open import adj-monad 32 open import adj-monad
33 33
34 T_K = U_K ○ F_K 34 T_K = U_K ○ F_K
35 35