diff --git a/.gitignore b/.gitignore index e8593bf..b182198 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,4 @@ lake-packages/ .lake/ **/.DS_Store .i18n/**/*.mo +*~ diff --git a/vid_script.txt~ b/vid_script.txt~ deleted file mode 100644 index 2073e53..0000000 --- a/vid_script.txt~ +++ /dev/null @@ -1,15 +0,0 @@ -How I made the natural number game. - -Peter Johnstone taught me that 0 was {}, 1 was {{}}, 2 was {{},{{}}} and so on. But what about all the people who didn't go to that class? - -Set theory is *one way of doing mathematics*. - -Type theory is *another way of doing mathematics* - -In mathematics, when you say "let G be a group" what you mean is that G is a set, and G has elements, and the elements are all individual "atoms", and that it is impossible to split the atom. - - -A theorem -Load of old nonsense. - -IDeas: geometry game,