Week 29 - 2021
The weeknote for 7/19 - 7/25. You can edit this page (on github) if you find any error.
This week we found that our baby was a boy.
ベビ澤さんは男の子でした🥳🎉 pic.twitter.com/sMRJSgK8Q5— あずき (@okomekirai) July 21, 2021
24th of July was Iyo-chan's birthday. We went to Hermès in Ginza and bought a watch which Iyo-chan wanted for a long time, and also had birthday lunch in Shiseido parlour.
誕生日プレゼントをゲットしてご満悦のパートナー pic.twitter.com/fITtOE7gVR— Yoshiya Hinosawa (@kt3k) July 24, 2021
おひるはカレーステーキという最強の食べ物を食べました pic.twitter.com/Y3s1WemTb1— あずき (@okomekirai) July 24, 2021
お誕生日会をしている pic.twitter.com/XEEedXUmp2— あずき (@okomekirai) July 24, 2021
This week I started learning ETCS, Elementary Theory of Category of Sets. This is a category-theoretical version of set theory, which is usually presented as ZFC axioms. ZFC is often considered as one of the standard of the foundation of mathematics, but ETCS is another approach to the foundation of mathematics. During learning the axioms in ETCS, the definition of limit in category theoretical sense was so difficult. I'm still in the middle of the process of understanding it. The definition requires other definitions such as diagrams, natural transformations, etc. It's overwhelmingly difficult.
I've been learning it in order to decide which theory to choose as the basis of the proover language I'm going to build in the future. I first naively planned to use ZFC as the basics, but after learning about versions of theorem proovers such as HOL, Coq, Lean, Metamath, Mizar, Isabelle, Idris, Twelf, etc, I feel ZFC is probably an unnatural choice as a foundation. So now I'm looking for an alternative theory for my proover language.
See any mistakes? Please fix!