Week 29  2021
The weeknote for 7/19  7/25.
Life
Baby

This week we found that our baby was a boy.
ベビ澤さんは男の子でした🥳🎉 pic.twitter.com/sMRJSgK8Q5
— あずき (@okomekirai) July 21, 2021
Iyochan's Birthday

24th of July was Iyochan's birthday. We went to Hermès in Ginza and bought a watch which Iyochan 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
Hobby
ETCS

This week I started learning ETCS, Elementary Theory of Category of Sets. This is a categorytheoretical 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.