log

age author description
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