| 2017-10-30 |
Shinji KONO |
fix
|
| 2017-10-30 |
Shinji KONO |
remove comp from limit-to
|
| 2017-10-30 |
Shinji KONO |
fix completeness
|
| 2017-10-30 |
Shinji KONO |
SetCompleteness done!
|
| 2017-10-27 |
Shinji KONO |
...
|
| 2017-10-23 |
Shinji KONO |
...
|
| 2017-10-22 |
Shinji KONO |
...
|
| 2017-10-22 |
Shinji KONO |
...
|
| 2017-10-22 |
Shinji KONO |
introducd HeterogeneousEquality
|
| 2017-08-12 |
Shinji KONO |
move InitialObject to cat-utility
|
| 2017-07-19 |
Shinji KONO |
maybe monad done
|
| 2017-07-19 |
Shinji KONO |
add maybe-monad
|
| 2017-07-16 |
Shinji KONO |
fix
|
| 2017-07-06 |
Shinji KONO |
adjoint functor theorem done
|
| 2017-07-06 |
Shinji KONO |
on going ...
|
| 2017-07-06 |
Shinji KONO |
fix
|
| 2017-07-05 |
Shinji KONO |
universal mapping
|
| 2017-07-05 |
Shinji KONO |
uniquness
|
| 2017-07-05 |
Shinji KONO |
solution
|
| 2017-07-05 |
Shinji KONO |
rewritw solution
|
| 2017-07-04 |
Shinji KONO |
id of Functor F
|
| 2017-07-04 |
Shinji KONO |
fix
|
| 2017-07-04 |
Shinji KONO |
module introdued
|
| 2017-07-04 |
Shinji KONO |
use module
|
| 2017-07-03 |
Shinji KONO |
functorF and η
|
| 2017-07-03 |
Shinji KONO |
add adjunction
|
| 2017-07-03 |
Shinji KONO |
start adjoint
|
| 2017-07-03 |
Shinji KONO |
representability theorem done.
|
| 2017-07-03 |
Shinji KONO |
add more lemma
|
| 2017-07-02 |
Shinji KONO |
on going ..
|
| 2017-07-02 |
Shinji KONO |
add revU
|
| 2017-07-02 |
Shinji KONO |
add more lemma
|
| 2017-07-01 |
Shinji KONO |
...
|
| 2017-07-01 |
Shinji KONO |
creating nat
|
| 2017-06-30 |
Shinji KONO |
if K{*}↓U has initial Obj, U is representable done.
|
| 2017-06-30 |
Shinji KONO |
on going ...
|
| 2017-06-30 |
Shinji KONO |
introduce U preserving
|
| 2017-06-28 |
Shinji KONO |
fix
|
| 2017-06-27 |
Shinji KONO |
add equalizer
|
| 2017-06-27 |
Shinji KONO |
add compleness
|
| 2017-06-26 |
Shinji KONO |
introduce fArrow
|
| 2017-06-26 |
Shinji KONO |
fix
|
| 2017-06-26 |
Shinji KONO |
fix
|
| 2017-06-26 |
Shinji KONO |
remove arrow's yellow
|
| 2017-06-25 |
Shinji KONO |
fix
|
| 2017-06-23 |
Shinji KONO |
on going ...
|
| 2017-06-23 |
Shinji KONO |
initialObject done
|
| 2017-06-23 |
Shinji KONO |
introduce one element set
|
| 2017-06-23 |
Shinji KONO |
One
|
| 2017-06-23 |
Shinji KONO |
fix
|
| 2017-06-21 |
Shinji KONO |
add desciptive lemma
|
| 2017-06-20 |
Shinji KONO |
on going ..
|
| 2017-06-20 |
Shinji KONO |
on going ...
|
| 2017-06-20 |
Shinji KONO |
fix
|
| 2017-06-19 |
Shinji KONO |
initital obj uniquness done
|
| 2017-06-14 |
Shinji KONO |
on going ..
|
| 2017-06-14 |
Shinji KONO |
initial Object's arrow found
|
| 2017-06-13 |
Shinji KONO |
Representational Functor preserve limit done
|
| 2017-06-13 |
Shinji KONO |
t0f=t0 done
|
| 2017-06-13 |
Shinji KONO |
fix
|
| 2017-06-12 |
Shinji KONO |
natural transformation in representable functor
|
| 2017-06-12 |
Shinji KONO |
on going ...
|
| 2017-06-12 |
Shinji KONO |
on goging
|
| 2017-06-12 |
Shinji KONO |
freyd2
|
| 2017-06-08 |
Shinji KONO |
fix
|
| 2017-06-08 |
Shinji KONO |
fix for new agda
|
| 2017-06-08 |
Shinji KONO |
another snat-cong approach
|
| 2017-06-05 |
Shinji KONO |
comm2
|
| 2017-06-05 |
Shinji KONO |
two field again ...
|
| 2017-06-05 |
Shinji KONO |
makeEqu/makeProd does not woek
|
| 2017-06-05 |
Shinji KONO |
prove fe=ge in limit-to
|
| 2017-06-03 |
Shinji KONO |
Set Completeness unfinished
|
| 2017-06-02 |
Shinji KONO |
fix
|
| 2017-06-02 |
Shinji KONO |
try two field again
|
| 2017-05-24 |
Shinji KONO |
on going ...
|
| 2017-05-23 |
Shinji KONO |
lemma-equ retry
|
| 2017-05-23 |
Shinji KONO |
dead end
|
| 2017-05-22 |
Shinji KONO |
fix
|
| 2017-05-21 |
Shinji KONO |
fix
|
| 2017-05-15 |
Shinji KONO |
on going ..
|
| 2017-05-14 |
Shinji KONO |
slid rewrite
|
| 2017-05-14 |
Shinji KONO |
on going ...
|
| 2017-05-14 |
Shinji KONO |
dead end
|
| 2017-05-12 |
Shinji KONO |
fix
|
| 2017-05-12 |
Shinji KONO |
on going ...
|
| 2017-05-11 |
Shinji KONO |
on going ..
|
| 2017-05-11 |
Shinji KONO |
on oging ...
|
| 2017-05-11 |
Shinji KONO |
cequ introduced
|
| 2017-05-03 |
Shinji KONO |
anothter approach
|
| 2017-05-03 |
Shinji KONO |
close
|
| 2017-05-01 |
Shinji KONO |
another approach
|
| 2017-04-29 |
Shinji KONO |
to case for equ lemma
|
| 2017-04-28 |
Shinji KONO |
...
|
| 2017-04-28 |
Shinji KONO |
one yelllow
|
| 2017-04-28 |
Shinji KONO |
dead end
|
| 2017-04-27 |
Shinji KONO |
sproj approach
|
| 2017-04-27 |
Shinji KONO |
look like dead end
|
| 2017-04-25 |
Shinji KONO |
...
|
| 2017-04-25 |
Shinji KONO |
fix
|
| 2017-04-24 |
Shinji KONO |
fix
|
| 2017-04-24 |
Shinji KONO |
fix
|
| 2017-04-24 |
Shinji KONO |
yelloow remains
|
| 2017-04-24 |
Shinji KONO |
lemma-equ
|
| 2017-04-24 |
Shinji KONO |
last one problem in SetCompleteness
|
| 2017-04-24 |
Shinji KONO |
on going ...
|
| 2017-04-24 |
Shinji KONO |
on going ...
|
| 2017-04-24 |
Shinji KONO |
on going ...
|
| 2017-04-24 |
Shinji KONO |
on ging ...
|
| 2017-04-23 |
Shinji KONO |
try id equalizer
|
| 2017-04-10 |
Shinji KONO |
dead end again ...
|
| 2017-04-10 |
Shinji KONO |
on going ...
|
| 2017-04-10 |
Shinji KONO |
on going ...
|
| 2017-04-09 |
Shinji KONO |
dead end
|
| 2017-04-09 |
Shinji KONO |
on going ...
|
| 2017-04-09 |
Shinji KONO |
close
|
| 2017-04-09 |
Shinji KONO |
give up this approach
|
| 2017-04-09 |
Shinji KONO |
on going ...
|
| 2017-04-09 |
Shinji KONO |
equ version on going ...
|
| 2017-04-08 |
Shinji KONO |
on going ...
|
| 2017-04-08 |
Shinji KONO |
equalizer approach
|
| 2017-04-05 |
Shinji KONO |
fix ...
|
| 2017-04-05 |
Shinji KONO |
close this
|
| 2017-04-05 |
Shinji KONO |
snmeqeqt
|
| 2017-04-05 |
Shinji KONO |
fix
|
| 2017-04-04 |
Shinji KONO |
on going ...
|
| 2017-04-04 |
Shinji KONO |
on going
|
| 2017-04-01 |
Shinji KONO |
fix
|
| 2017-04-01 |
Shinji KONO |
fix
|
| 2017-04-01 |
Shinji KONO |
fix
|
| 2017-03-31 |
Shinji KONO |
bad
|
| 2017-03-31 |
Shinji KONO |
fix
|
| 2017-03-30 |
Shinji KONO |
on going ...
|
| 2017-03-30 |
Shinji KONO |
fix
|
| 2017-03-30 |
Shinji KONO |
locally small
|
| 2017-03-30 |
Shinji KONO |
fix
|
| 2017-03-30 |
Shinji KONO |
add iso1
|
| 2017-03-30 |
Shinji KONO |
on going ....
|
| 2017-03-29 |
Shinji KONO |
introducing snat
|
| 2017-03-29 |
Shinji KONO |
use sequ
|
| 2017-03-29 |
Shinji KONO |
equalizer does not fit
|
| 2017-03-28 |
Shinji KONO |
on going ...
|
| 2017-03-28 |
Shinji KONO |
on going ...
|
| 2017-03-28 |
Shinji KONO |
fix
|
| 2017-03-28 |
Shinji KONO |
fix
|
| 2017-03-28 |
Shinji KONO |
fix ...
|
| 2017-03-28 |
Shinji KONO |
Small Category for Sets Limit
|
| 2017-03-27 |
Shinji KONO |
on going ...
|
| 2017-03-26 |
Shinji KONO |
on going ..
|
| 2017-03-26 |
Shinji KONO |
fix
|
| 2017-03-26 |
Shinji KONO |
Equalizer in Sets done
|
| 2017-03-22 |
Shinji KONO |
only yellow remains in uniquness
|
| 2017-03-22 |
Shinji KONO |
k-cong done
|
| 2017-03-21 |
Shinji KONO |
try hom equality in uniquness
|
| 2017-03-21 |
Shinji KONO |
fix
|
| 2017-03-21 |
Shinji KONO |
on going ..
|
| 2017-03-21 |
Shinji KONO |
yellow remains ...
|
| 2017-03-21 |
Shinji KONO |
on going ...
|
| 2017-03-21 |
Shinji KONO |
on going ...
|
| 2017-03-21 |
Shinji KONO |
on going ...
|
| 2017-03-20 |
Shinji KONO |
on going ...
|
| 2017-03-19 |
Shinji KONO |
fix
|
| 2017-03-19 |
Shinji KONO |
equalizer in Sets , uniquness remains
|
| 2017-03-18 |
Shinji KONO |
IProduct in Sets done
|
| 2017-03-18 |
Shinji KONO |
IProduct is written in Sets
|
| 2017-03-17 |
Shinji KONO |
fix
|
| 2017-03-17 |
Shinji KONO |
fix
|
| 2017-03-17 |
Shinji KONO |
on going ...
|
| 2017-03-17 |
Shinji KONO |
on going...
|
| 2017-03-17 |
Shinji KONO |
on going ...
|
| 2017-03-16 |
Shinji KONO |
on going ..
|
| 2017-03-16 |
Shinji KONO |
Sets completeness failed
|
| 2017-03-15 |
Shinji KONO |
try to make prodcut and equalizer in Sets
|
| 2017-03-15 |
Shinji KONO |
prove only limit preserving on co yoneda functor's obj
|
| 2017-03-15 |
Shinji KONO |
UpreseveLimit detailing
|
| 2017-03-15 |
Shinji KONO |
add if U is iso to representable functor then preserve limit
|
| 2017-03-14 |
Shinji KONO |
fix
|
| 2017-03-14 |
Shinji KONO |
fryed1 done
|
| 2017-03-14 |
Shinji KONO |
unique direction 2 done
|
| 2017-03-14 |
Shinji KONO |
on going using limit-uniquness directly
|
| 2017-03-13 |
Shinji KONO |
on going..
|
| 2017-03-13 |
Shinji KONO |
comma-a0 commuativity remains
|
| 2017-03-13 |
Shinji KONO |
commaNat done
|
| 2017-03-12 |
Shinji KONO |
on going ..
|
| 2017-03-12 |
Shinji KONO |
commaLimit done, commaNat trying..
|
| 2017-03-12 |
Shinji KONO |
found limit in freyd
|
| 2017-03-12 |
Shinji KONO |
add some lemma but no use
|
| 2017-03-11 |
Shinji KONO |
on going ...
|
| 2017-03-11 |
Shinji KONO |
fix Limit pu a0 and t0 in record definition
|
| 2017-03-11 |
Shinji KONO |
add NIC
|
| 2017-03-10 |
Shinji KONO |
on going ...
|
| 2017-03-10 |
Shinji KONO |
Completeness of Comma Category begin
|
| 2017-03-10 |
Shinji KONO |
add Comma1
|
| 2017-03-09 |
Shinji KONO |
Comma Category with A B C
|
| 2017-03-09 |
Shinji KONO |
Comma category
|
| 2017-03-08 |
Shinji KONO |
add Comma category
|
| 2017-03-07 |
Shinji KONO |
add README
|
| 2017-03-07 |
Shinji KONO |
add license
|
| 2017-03-06 |
Shinji KONO |
clean up
|
| 2017-03-06 |
Shinji KONO |
close this
|
| 2017-03-06 |
Shinji KONO |
discrete equality as a dom equality
|
| 2017-03-06 |
Shinji KONO |
fix
|
| 2017-03-06 |
Shinji KONO |
discrete should have Set based Obj
|
| 2017-03-06 |
Shinji KONO |
discrete f ≡ refl should be passed, but it doesn't
|
| 2017-03-06 |
Shinji KONO |
discrete category and product from a limit
|
| 2017-03-05 |
Shinji KONO |
clean up
|
| 2017-03-04 |
Shinji KONO |
clean up
|
| 2017-03-04 |
Shinji KONO |
clean up
|
| 2017-03-04 |
Shinji KONO |
document clean up
|
| 2017-03-04 |
Shinji KONO |
document clean up
|
| 2017-03-04 |
Shinji KONO |
clean up fix
|
| 2017-03-04 |
Shinji KONO |
clean up
|
| 2017-03-03 |
Shinji KONO |
limit-to done
|
| 2017-03-02 |
Shinji KONO |
freyd trbouled again
|
| 2017-03-02 |
Shinji KONO |
fix comment
|
| 2017-03-02 |
Shinji KONO |
limit-to and discrete clean up
|
| 2017-03-02 |
Shinji KONO |
limit with nat
|
| 2017-03-02 |
Shinji KONO |
on going ...
|
| 2017-03-02 |
Shinji KONO |
fix
|
| 2017-03-02 |
Shinji KONO |
try incomplete pattern for discrete
|
| 2017-02-28 |
Shinji KONO |
negnat
|
| 2017-02-28 |
Shinji KONO |
add negation example
|
| 2017-02-27 |
Shinji KONO |
bottom
|
| 2017-01-02 |
Shinji KONO |
on goinhg ...
|
| 2017-01-02 |
Shinji KONO |
discrete again with negation
|
| 2016-10-15 |
Shinji KONO |
complete connection dead end
|
| 2016-10-14 |
Shinji KONO |
bad case on distr
|
| 2016-10-14 |
Shinji KONO |
cont..
|
| 2016-10-14 |
Shinji KONO |
complete connection for finite category
|
| 2016-09-04 |
Shinji KONO |
fix IsEqualizer
|
| 2016-09-01 |
Shinji KONO |
fix
|
| 2016-08-30 |
Shinji KONO |
preinital full subcategory done
|
| 2016-08-30 |
Shinji KONO |
fix limit
|
| 2016-08-29 |
Shinji KONO |
equ
|
| 2016-08-29 |
Shinji KONO |
clean up
|
| 2016-08-29 |
Shinji KONO |
add rest of equation
|
| 2016-08-29 |
Shinji KONO |
initialFullSubCategory
|
| 2016-08-28 |
Shinji KONO |
f=g if equalizer k has right inverse
|
| 2016-03-27 |
Shinji KONO |
add discrete
|
| 2016-03-26 |
Shinji KONO |
functor constraint does not work well on distribution law
|
| 2016-03-26 |
Shinji KONO |
add another method as a comment
|
