Week 29 - 2021

The weeknote for 7/19 - 7/25.

Life

This week we found that our baby was a boy.

ベビ澤さんは男の子でした🥳🎉 pic.twitter.com/sMRJSgK8Q5
— あずき (@okomekirai) July 21, 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.