2013-08-18 |
Shinji KONO |
on going
|
2013-08-17 |
Shinji KONO |
sync
|
2013-08-17 |
Shinji KONO |
fix
|
2013-08-17 |
Shinji KONO |
fix
|
2013-08-15 |
Shinji KONO |
clean up
|
2013-08-15 |
Shinji KONO |
clean up
|
2013-08-15 |
Shinji KONO |
no yellow on monoid monad
|
2013-08-14 |
Shinji KONO |
add comment
|
2013-08-14 |
Shinji KONO |
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
|
2013-08-14 |
Shinji KONO |
on going ..
|
2013-08-14 |
Shinji KONO |
on going...
|
2013-08-13 |
Shinji KONO |
on going ...
|
2013-08-13 |
Shinji KONO |
on going...
|
2013-08-13 |
Shinji KONO |
on going
|
2013-08-13 |
Shinji KONO |
fix
|
2013-08-13 |
Shinji KONO |
η and μ defined.
|
2013-08-13 |
Shinji KONO |
T as Sets -> Sets
|
2013-08-13 |
Shinji KONO |
dead end?
|
2013-08-13 |
Shinji KONO |
on ogoing...
|
2013-08-11 |
Shinji KONO |
on going...
|
2013-08-11 |
Shinji KONO |
M x A done
|
2013-08-11 |
Shinji KONO |
hom composition passed.
|
2013-08-11 |
Shinji KONO |
trying..
|
2013-08-11 |
Shinji KONO |
trying..
|
2013-08-08 |
Shinji KONO |
remove Kleisli record
|
2013-08-03 |
Shinji KONO |
monoid monad
|
2013-08-02 |
Shinji KONO |
Comparison Functor all done.
|
2013-08-02 |
Shinji KONO |
Comparison Functor for Eilenberg-Moore Category is constructed.
|
2013-08-02 |
Shinji KONO |
Algebra
|
2013-08-02 |
Shinji KONO |
on going (horizontal composition)
|
2013-08-01 |
Shinji KONO |
on going
|
2013-08-01 |
Shinji KONO |
problems written Comparison Functor on EM
|
2013-08-01 |
Shinji KONO |
no yellow on em-category
|
2013-08-01 |
Shinji KONO |
add Comparison functor for EM
|
2013-08-01 |
Shinji KONO |
EM Resolution complete
|
2013-08-01 |
Shinji KONO |
nat-μ
|
2013-08-01 |
Shinji KONO |
ε^T and μ^t
|
2013-08-01 |
Shinji KONO |
T ≃ (U^T ○ F^T)
|
2013-08-01 |
Shinji KONO |
F^T and U^T constructed
|
2013-08-01 |
Shinji KONO |
U^T and F^T problem written
|
2013-07-31 |
Shinji KONO |
EM Category constructed
|
2013-07-31 |
Shinji KONO |
field version
|
2013-07-31 |
Shinji KONO |
constructed but some yellow remains
|
2013-07-31 |
Shinji KONO |
Category._o_ /= Category.Category.Id
|
2013-07-31 |
Shinji KONO |
resp and assoc
|
2013-07-31 |
Shinji KONO |
idL, idR
|
2013-07-31 |
Shinji KONO |
on going...
|
2013-07-31 |
Shinji KONO |
no yellow. ready to define category
|
2013-07-31 |
Shinji KONO |
yellow...
|
2013-07-31 |
Shinji KONO |
on going...
|
2013-07-31 |
Shinji KONO |
problem written
|
2013-07-31 |
Shinji KONO |
on oging
|
2013-07-31 |
Shinji KONO |
on goning
|
2013-07-31 |
Shinji KONO |
on going ...
|
2013-07-30 |
Shinji KONO |
Eilenberg-Moore Category start
|
2013-07-29 |
Shinji KONO |
uniquness of comparison functor
|
2013-07-29 |
Shinji KONO |
generated version of comparison functor
|
2013-07-29 |
Shinji KONO |
seprate comparison functor
|
2013-07-29 |
Shinji KONO |
fix
|
2013-07-29 |
Shinji KONO |
nat-μ
|
2013-07-29 |
Shinji KONO |
Comparison Functor constructed
|
2013-07-28 |
Shinji KONO |
distr continue..
|
2013-07-28 |
Shinji KONO |
K_T identity
|
2013-07-28 |
Shinji KONO |
strange but worked.
|
2013-07-28 |
Shinji KONO |
on going
|
2013-07-28 |
Shinji KONO |
KtoT
|
2013-07-28 |
Shinji KONO |
on going
|
2013-07-27 |
Shinji KONO |
MEsolution
|
2013-07-27 |
Shinji KONO |
resosultion
|
2013-07-27 |
Shinji KONO |
Resoution?
|
2013-07-27 |
Shinji KONO |
record Resolution
|
2013-07-27 |
Shinji KONO |
Comparison Functor
|
2013-07-27 |
Shinji KONO |
fix
|
2013-07-27 |
Shinji KONO |
Resolution Adjoint proved.
|
2013-07-27 |
Shinji KONO |
Adjoint of U_T F_T
|
2013-07-26 |
Shinji KONO |
on going
|
2013-07-26 |
Shinji KONO |
on going
|
2013-07-26 |
Shinji KONO |
Resolution U_T, F_T
|
2013-07-26 |
Shinji KONO |
U done
|
2013-07-26 |
Shinji KONO |
Comparison Functor
|
2013-07-26 |
Shinji KONO |
Kleisli Category constructed
|
2013-07-26 |
Shinji KONO |
on going
|
2013-07-26 |
Shinji KONO |
stack overflow solved by moving implicit parameters to module parameters
|
2013-07-26 |
Shinji KONO |
Kleisli category problem written
|
2013-07-25 |
Shinji KONO |
Kleisli Category ...
|
2013-07-25 |
Shinji KONO |
generalized distr and assco1
|
2013-07-25 |
Shinji KONO |
join implicit parameter
|
2013-07-25 |
Shinji KONO |
cong-hom ?
|
2013-07-25 |
Shinji KONO |
distr
|
2013-07-25 |
Shinji KONO |
add pdf
|
2013-07-25 |
Shinji KONO |
hd add pdf
|
2013-07-25 |
Shinji KONO |
cleanup
|
2013-07-25 |
Shinji KONO |
assoc proved.
|
2013-07-24 |
Shinji KONO |
unity done
|
2013-07-24 |
Shinji KONO |
unity1
|
2013-07-24 |
Shinji KONO |
UεF
|
2013-07-24 |
Shinji KONO |
on going
|
2013-07-24 |
Shinji KONO |
nat and functor comp
|
2013-07-24 |
Shinji KONO |
add unitility
|
2013-07-23 |
Shinji KONO |
Adjoint proved. All done.
|
2013-07-23 |
Shinji KONO |
cleanup
|
2013-07-23 |
Shinji KONO |
start adjunction
|
2013-07-23 |
Shinji KONO |
nat-ε proved
|
2013-07-23 |
Shinji KONO |
on going...
|
2013-07-23 |
Shinji KONO |
on goging
|
2013-07-23 |
Shinji KONO |
naturality of ε
|
2013-07-22 |
Shinji KONO |
naturarity of η
|
2013-07-22 |
Shinji KONO |
F is Functor proved.
|
2013-07-22 |
Shinji KONO |
Functor cong done
|
2013-07-22 |
Shinji KONO |
uniq-univeralMapping from Adjunction
|
2013-07-22 |
Shinji KONO |
f replacement
|
2013-07-22 |
Shinji KONO |
uniqness
|
2013-07-22 |
Shinji KONO |
Functor Identity
|
2013-07-22 |
Shinji KONO |
isFunctor
|
2013-07-22 |
Shinji KONO |
Adjunction to Universal Mapping end
|
2013-07-22 |
Shinji KONO |
Reasoning
|
2013-07-22 |
Shinji KONO |
reasoning
|
2013-07-22 |
Shinji KONO |
universalMapping
|
2013-07-22 |
Shinji KONO |
isUniversalMapping
|
2013-07-22 |
Shinji KONO |
f∗ = ε(b)F(f),
|