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.