13th Nov 2020 (Things I learned)
-Classical and constructive mathematics consists of a wide range of mathematical
 "universes" (what does that mean) as foundations to pick from. - Andrej Bauer
       https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4
- Metamath is super picky about parentheses hmph
- Writing your own `mynat` in Lean is really worth the effort! no fancy notation
- sigh, i think there is no escaping category theory.. i'll postpone it as much
  as possible tho ... hehe i wonder if i'd regret this in the future

hmm I have some questions which are really bugging me and I just wanna ask
someone like MC for help. How do you know that definitions in metamath
doesn't strengthen the system? must the verifier somehow prove this? idts...
The fact that they can be effectively reduced to simpler terms is kinda
understandable, but maybe that it doesn't add to the system needs to be
proved. Also, is there like a simple informal way of explaining all the
universe stuff. I hear words like homotopy and toposes and category and my
brain kinda shuts down.. Hmm, but i think this one is good to figure out by
yourself and not ask anyone.