2016-03-20 |
Shinji KONO |
...
|
2016-03-20 |
Shinji KONO |
maybe CAT
|
2016-03-17 |
Shinji KONO |
on going ...
|
2016-03-17 |
Shinji KONO |
Maybe Category to-limit
|
2016-03-16 |
Shinji KONO |
on going...
|
2016-03-16 |
Shinji KONO |
maybe category done
|
2016-03-16 |
Shinji KONO |
add Maybe Category
|
2016-03-16 |
Shinji KONO |
inconsistent distribution law on nil x arrow-g
|
2016-03-16 |
Shinji KONO |
non nil dead end...
|
2016-03-15 |
Shinji KONO |
bad distribution law
|
2016-03-15 |
Shinji KONO |
distribution law stacked
|
2016-03-15 |
Shinji KONO |
on going ..
|
2016-03-15 |
Shinji KONO |
trying ...
|
2016-03-15 |
Shinji KONO |
fix
|
2016-03-15 |
Shinji KONO |
null does not work
|
2016-03-15 |
Shinji KONO |
another try ...
|
2016-03-14 |
Shinji KONO |
on going ...
|
2016-03-14 |
Shinji KONO |
what is this ?
|
2016-03-14 |
Shinji KONO |
dead end
|
2016-03-14 |
Shinji KONO |
add level
|
2016-03-14 |
Shinji KONO |
tow-hom-iso in twocat
|
2016-03-13 |
Shinji KONO |
Maybe Arrow
|
2016-03-13 |
Shinji KONO |
maybe map
|
2016-03-12 |
Shinji KONO |
...
|
2016-03-12 |
Shinji KONO |
fix
|
2016-03-12 |
Shinji KONO |
step by step ...
|
2016-03-12 |
Shinji KONO |
add maybe in twocat
|
2016-03-11 |
Shinji KONO |
associative in twocat dead end?
|
2016-03-10 |
Shinji KONO |
fix
|
2016-03-06 |
Shinji KONO |
still trying ...
|
2016-03-06 |
Shinji KONO |
limit-to: indexFunctor distribution law cannot be proved
|
2016-03-05 |
Shinji KONO |
fix
|
2016-03-05 |
Shinji KONO |
add more lemma in limit-to
|
2016-03-05 |
Shinji KONO |
limit-to nat will be done
|
2016-03-05 |
Shinji KONO |
fix
|
2016-03-05 |
Shinji KONO |
simplify
|
2016-03-05 |
Shinji KONO |
add more parameter to nat in lim-to-equ
|
2016-03-05 |
Shinji KONO |
limit-to dead end...
|
2016-03-05 |
Shinji KONO |
...
|
2016-03-05 |
Shinji KONO |
...
|
2016-03-04 |
Shinji KONO |
Γ : Functor A A
|
2016-03-04 |
Shinji KONO |
two cat
|
2015-06-26 |
Shinji KONO |
member
|
2015-06-26 |
Shinji KONO |
fix
|
2015-06-26 |
Shinji KONO |
arrow
|
2015-06-26 |
Shinji KONO |
nat equalit
|
2015-05-13 |
Shinji KONO |
fix
|
2015-05-12 |
Shinji KONO |
fix
|
2015-05-11 |
Shinji KONO |
history to continuation
|
2015-05-11 |
Shinji KONO |
add DataCategory Universal mapping
|
2015-04-02 |
Shinji KONO |
fix
|
2015-04-01 |
Shinji KONO |
list representation of TwoCat Hom
|
2014-12-24 |
Shinji KONO |
bad approach
|
2014-12-24 |
Shinji KONO |
...
|
2014-12-24 |
Shinji KONO |
try equalizer from limit
|
2014-05-04 |
Shinji KONO |
fix
|
2014-05-03 |
Shinji KONO |
fix
|
2014-04-22 |
Shinji KONO |
list try ..
|
2014-04-19 |
Shinji KONO |
fix
|
2014-04-19 |
Shinji KONO |
fix on System F
|
2014-04-18 |
Shinji KONO |
ItInt on system F
|
2014-04-18 |
Shinji KONO |
free-monoid comment
|
2014-04-18 |
Shinji KONO |
free-monoid fix
|
2014-04-17 |
Shinji KONO |
minor fix on free monoid
|
2014-03-29 |
Shinji KONO |
ditr on system T
|
2014-03-29 |
Shinji KONO |
assoc in sysem-T
|
2014-03-29 |
Shinji KONO |
sym of sum and mul in system T
|
2014-03-24 |
Shinji KONO |
add Tree example ( not yet worked )
|
2014-03-23 |
Shinji KONO |
λ
|
2014-03-22 |
Shinji KONO |
fix
|
2014-03-22 |
Shinji KONO |
add : Int X -> Int X -> Int X
|
2014-03-22 |
Shinji KONO |
factorial still have a problem
|
2014-03-22 |
Shinji KONO |
factoral done.
|
2014-03-22 |
Shinji KONO |
fact
|
2014-03-22 |
Shinji KONO |
remove module level
|
2014-03-22 |
Shinji KONO |
no yellow on append example
|
2014-03-22 |
Shinji KONO |
Append
|
2014-03-22 |
Shinji KONO |
fix Emp commnet
|
2014-03-21 |
Shinji KONO |
fix
|
2014-03-20 |
Shinji KONO |
Tree
|
2014-03-20 |
Shinji KONO |
R lemma
|
2014-03-19 |
Shinji KONO |
fact error on R
|
2014-03-19 |
Shinji KONO |
Int
|
2014-03-19 |
Shinji KONO |
Emp with yellow
|
2014-03-17 |
Shinji KONO |
fix Emp
|
2014-03-17 |
Shinji KONO |
Emp in System F
|
2014-03-16 |
Shinji KONO |
fx
|
2014-03-16 |
Shinji KONO |
iota
|
2014-03-16 |
Shinji KONO |
Emp and Sum first try
|
2014-03-15 |
Shinji KONO |
System T and System F
|
2014-01-06 |
Shinji KONO |
on going...
|
2014-01-05 |
Shinji KONO |
???
|
2014-01-05 |
Shinji KONO |
is this right direction?
|
2014-01-05 |
Shinji KONO |
on going...
|
2014-01-05 |
Shinji KONO |
on going...
|
2014-01-05 |
Shinji KONO |
preinitial problem written
|
2014-01-05 |
Shinji KONO |
pre-initial
|
2014-01-05 |
Shinji KONO |
small full subcategory done.
|
2014-01-05 |
Shinji KONO |
Small Full Subcategory (underconstruction)
|
2014-01-05 |
Shinji KONO |
subset
|
2014-01-04 |
Shinji KONO |
Freyd Adjoint Functor Theorem
|
2013-11-04 |
Shinji KONO |
Limit form equalizer and product done.
|
2013-10-30 |
Shinji KONO |
looped.
|
2013-09-29 |
Shinji KONO |
fix
|
2013-09-29 |
Shinji KONO |
arrow and lambda fix
|
2013-09-29 |
Shinji KONO |
remove module parameter from yoneda functor
|
2013-09-25 |
Shinji KONO |
fix
|
2013-09-25 |
Shinji KONO |
limit preservation proved.
|
2013-09-25 |
Shinji KONO |
lemma1 will be proved
|
2013-09-25 |
Shinji KONO |
limit equation done.
|
2013-09-25 |
Shinji KONO |
limit1 done
|
2013-09-25 |
Shinji KONO |
limit defined.
|
2013-09-25 |
Shinji KONO |
on going
|
2013-09-25 |
Shinji KONO |
limit preserving ...
|
2013-09-25 |
Shinji KONO |
fix
|
2013-09-25 |
Shinji KONO |
move to iProduct axiom
|
2013-09-24 |
Shinji KONO |
give up ...
|
2013-09-23 |
Shinji KONO |
ion going
|
2013-09-23 |
Shinji KONO |
uum
|
2013-09-23 |
Shinji KONO |
commutativity continue...
|
2013-09-23 |
Shinji KONO |
comutativity remains
|
2013-09-23 |
Shinji KONO |
on going ...
|
2013-09-23 |
Shinji KONO |
limit on going...
|
2013-09-23 |
Shinji KONO |
limit from product and equalizer continue...
|
2013-09-23 |
Shinji KONO |
univ2limit done.
|
2013-09-22 |
Shinji KONO |
limit and prod/equalizer
|
2013-09-22 |
Shinji KONO |
univ2limit
|
2013-09-22 |
Shinji KONO |
2 yellow remains
|
2013-09-22 |
Shinji KONO |
yellow remains ...
|
2013-09-22 |
Shinji KONO |
on going ...
|
2013-09-22 |
Shinji KONO |
adjoint2limit problems are written
|
2013-09-22 |
Shinji KONO |
try adjoint2limit
|
2013-09-22 |
Shinji KONO |
adjunction to limit
|
2013-09-22 |
Shinji KONO |
limit2adjoint done
|
2013-09-22 |
Shinji KONO |
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
|
2013-09-22 |
Shinji KONO |
adjoint form limit
|
2013-09-22 |
Shinji KONO |
co universal mapping
|
2013-09-22 |
Shinji KONO |
Constancy Functor
|
2013-09-22 |
Shinji KONO |
iso on limit
|
2013-09-22 |
Shinji KONO |
add limit
|
2013-09-20 |
Shinji KONO |
pullback done
|
2013-09-20 |
Shinji KONO |
on going ..
|
2013-09-20 |
Shinji KONO |
uniqueness remains
|
2013-09-20 |
Shinji KONO |
pull back continue
|
2013-09-20 |
Shinji KONO |
pullback
|
2013-09-17 |
Shinji KONO |
add figure
|
2013-09-16 |
Shinji KONO |
simpler equalizer iso
|
2013-09-14 |
Shinji KONO |
fix
|
2013-09-14 |
Shinji KONO |
simpler proof
|
2013-09-14 |
Shinji KONO |
every equalizer is monic
|
2013-09-14 |
Shinji KONO |
equalizer fix
|
2013-09-11 |
Shinji KONO |
fix
|
2013-09-09 |
Shinji KONO |
comment
|
2013-09-09 |
Shinji KONO |
comment
|
2013-09-09 |
Shinji KONO |
equalizer iso done.
|
2013-09-09 |
Shinji KONO |
fix
|
2013-09-09 |
Shinji KONO |
fix
|
2013-09-09 |
Shinji KONO |
equalizer done.
|
2013-09-09 |
Shinji KONO |
cong-γ1 done, cong-δ1 remains
|
2013-09-09 |
Shinji KONO |
fix
|
2013-09-09 |
Shinji KONO |
fix
|
2013-09-08 |
Shinji KONO |
fix
|
2013-09-08 |
Shinji KONO |
fix
|
2013-09-08 |
Shinji KONO |
comments
|
2013-09-08 |
Shinji KONO |
fix
|
2013-09-07 |
Shinji KONO |
fix
|
2013-09-07 |
Shinji KONO |
Burrnoi to Equalizer problem written
|
2013-09-07 |
Shinji KONO |
fix
|
2013-09-07 |
Shinji KONO |
Burroni equational equalizer definition done.
|
2013-09-07 |
Shinji KONO |
passed let;s remove yellow
|
2013-09-07 |
Shinji KONO |
equalizer iso done.
|
2013-09-07 |
Shinji KONO |
e is now explict parameter
|
2013-09-07 |
Shinji KONO |
fix
|
2013-09-07 |
Shinji KONO |
reverse-e
|
2013-09-07 |
Shinji KONO |
fix
|
2013-09-06 |
Shinji KONO |
c in equalizer is equal up to iso done.
|
2013-09-05 |
Shinji KONO |
fix
|
2013-09-05 |
Shinji KONO |
fix
|
2013-09-05 |
Shinji KONO |
fix
|
2013-09-05 |
Shinji KONO |
comment
|
2013-09-05 |
Shinji KONO |
fix
|
2013-09-04 |
Shinji KONO |
fix
|
2013-09-04 |
Shinji KONO |
iso of equalizer
|
2013-09-04 |
Shinji KONO |
on going ...
|
2013-09-04 |
Shinji KONO |
eefg
|
2013-09-04 |
Shinji KONO |
on going ...
|
2013-09-04 |
Shinji KONO |
add equalizers
|
2013-09-04 |
Shinji KONO |
add equalizer+h
|
2013-09-03 |
Shinji KONO |
fix
|
2013-09-02 |
Shinji KONO |
equ6...
|
2013-09-02 |
Shinji KONO |
b4 remains.
|
2013-09-02 |
Shinji KONO |
on going
|
2013-09-02 |
Shinji KONO |
b2
|
2013-09-02 |
Shinji KONO |
b3
|
2013-09-02 |
Shinji KONO |
α b1
|
2013-09-02 |
Shinji KONO |
equalizer difinition
|
2013-09-02 |
Shinji KONO |
fix
|
2013-09-02 |
Shinji KONO |
Equalizer problems have written
|
2013-09-01 |
Shinji KONO |
on going
|
2013-09-01 |
Shinji KONO |
equalizer
|
2013-09-01 |
Shinji KONO |
embedding done?
|
2013-09-01 |
Shinji KONO |
on going ...
|
2013-09-01 |
Shinji KONO |
remove an extensionality
|
2013-08-31 |
Shinji KONO |
fix
|
2013-08-31 |
Shinji KONO |
exponential
|
2013-08-30 |
Shinji KONO |
fix
|
2013-08-30 |
Shinji KONO |
comment
|
2013-08-30 |
Shinji KONO |
clean up
|
2013-08-30 |
Shinji KONO |
give up injective on Object?
|
2013-08-30 |
Shinji KONO |
Nat2F→F2Nat done
|
2013-08-30 |
Shinji KONO |
F2Nat→Nat2F done
|
2013-08-30 |
Shinji KONO |
isomorphic problem written
|
2013-08-30 |
Shinji KONO |
F(a) → Nat(h_a,F) done
|
2013-08-30 |
Shinji KONO |
nat continue...
|
2013-08-29 |
Shinji KONO |
one to one nat
|
2013-08-29 |
Shinji KONO |
fix
|
2013-08-29 |
Shinji KONO |
Yoneda Functor Constructed
|
2013-08-28 |
Shinji KONO |
hint
|
2013-08-28 |
Shinji KONO |
y-nat (FMap of Yoneda Functor )
|
2013-08-28 |
Shinji KONO |
Yoneda join
|
2013-08-28 |
Shinji KONO |
oeration
|
2013-08-28 |
Shinji KONO |
Contravariant functor done
|
2013-08-28 |
Shinji KONO |
contravariant continue ...
|
2013-08-28 |
Shinji KONO |
contravariant functor
|
2013-08-28 |
Shinji KONO |
no yellow on co-Contravariant Functor
|
2013-08-28 |
Shinji KONO |
fix
|
2013-08-27 |
Shinji KONO |
Yoneda Functor
|
2013-08-25 |
Shinji KONO |
comment
|
2013-08-25 |
Shinji KONO |
hom set adjunction done.
|
2013-08-24 |
Shinji KONO |
hom-set to universal mapping done.
|
2013-08-24 |
Shinji KONO |
add more axiom on unity of oppsite
|
2013-08-23 |
Shinji KONO |
hmmmm
|
2013-08-23 |
Shinji KONO |
hmm
|
2013-08-23 |
Shinji KONO |
unity of oppsite
|
2013-08-21 |
Shinji KONO |
use functional extensionality in library
|
2013-08-21 |
Shinji KONO |
builtin extensionality
|
2013-08-20 |
Shinji KONO |
fix
|
2013-08-19 |
Shinji KONO |
Free Monoid and Universal mapping problem done.
|
2013-08-19 |
Shinji KONO |
two yellow remain...
|
2013-08-19 |
Shinji KONO |
fix
|
2013-08-19 |
Shinji KONO |
on going...
|
2013-08-19 |
Shinji KONO |
uniqueness continue...
|
2013-08-19 |
Shinji KONO |
mapping done
|
2013-08-18 |
Shinji KONO |
ok
|
2013-08-18 |
Shinji KONO |
hmmm
|
2013-08-18 |
Shinji KONO |
mmmm
|
2013-08-18 |
Shinji KONO |
um
|
2013-08-18 |
Shinji KONO |
solution of universal mapping for free monoid
|
2013-08-18 |
Shinji KONO |
list is monoid now.
|
2013-08-18 |
Shinji KONO |
Monoids done.
|
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),
|
2013-07-22 |
Shinji KONO |
trying...
|
2013-07-22 |
Shinji KONO |
add Adj to Universal Mapping
|
2013-07-22 |
Shinji KONO |
Adjoint
|
2013-07-22 |
Shinji KONO |
add universal mapping
|
2013-07-13 |
Shinji KONO |
fix
|
2013-07-13 |
Shinji KONO |
notation
|
2013-07-12 |
Shinji KONO |
fix
|
2013-07-12 |
Shinji KONO |
fix
|
2013-07-12 |
Shinji KONO |
join association finish
|
2013-07-12 |
Shinji KONO |
on going
|
2013-07-12 |
Shinji KONO |
on going
|
2013-07-12 |
Shinji KONO |
join assoc on going...
|
2013-07-12 |
Shinji KONO |
add some law
|
2013-07-12 |
Shinji KONO |
unity law 1
|
2013-07-12 |
Shinji KONO |
clean up list-nat
|
2013-07-12 |
Shinji KONO |
nat
|
2013-07-12 |
Shinji KONO |
reasoning worked.
|
2013-07-11 |
Shinji KONO |
not working yet
|
2013-07-09 |
Shinji KONO |
sss
|
2013-07-09 |
Shinji KONO |
list nat
|
2013-07-08 |
Shinji KONO |
not yet worked
|
2013-07-08 |
Shinji KONO |
Reasoning on going...
|
2013-07-07 |
Shinji KONO |
Reasoning complete!
|
2013-07-07 |
Shinji KONO |
reasoning test
|
2013-07-07 |
Shinji KONO |
reasoning
|
2013-07-07 |
Shinji KONO |
reasoning
|
2013-07-07 |
Shinji KONO |
refl and trans
|
2013-07-07 |
Shinji KONO |
Reasoning
|
2013-07-06 |
Shinji KONO |
add accessor
|
2013-07-06 |
Shinji KONO |
Kleisli Proposition
|
2013-07-05 |
Shinji KONO |
fix
|
2013-07-05 |
Shinji KONO |
Kleisli
|
2013-07-05 |
Shinji KONO |
unity1 unity2
|
2013-07-05 |
Shinji KONO |
Monad
|
2013-07-05 |
Shinji KONO |
category agda
|