Life started on Earth 4.5 billion years ago. Or maybe 3.5 billion years? It doesn't matter.
Let's write this in full: 4,500,000,000.
It eventually produced e.g. humans, among other equally or more interesting living beings.
Being generous, the first human being appeared about 300,000 years ago.
Compare the numbers:
4,500,000,000
00000300,000
Can you see how recent this is? An insignificant fraction of the history of life on earth.
Now, in just a few years, we have AGI as a prospect for the next year or so, after we have AI.
Let's be generous, and pretend the quest for AI started in the 19th century, with Babbage with the idea of the computer, and then in the 20th century with Turing's ideas improving this (and also his AI ideas).
4,500,000,000
00000300,000
00000300,100
Congratulations, academics and corporations for doing what took 4.5 billion years in just an insignificant fraction of the time.
Nobody understands the human brain, as people who research it will tell you themselves.
People after AGI are just in the most delusional state anybody can be.
We don't even understand well enough how our bodies work, let alone our brains.
I think I had assumed, unconsciously, for a long time, that international news is cumulative.
However, the news coming from the US, which, sadly, have influence in everything else, are always changing randomly back and forth, so that I lost the motivation to follow them daily.
On the bright side, the frees up some time for me to do something else rather than checking the news. What is the point of reading what is happening today, if tomorrow it will be something else randomly.
Injective types in constructive HoTT/UF.
This is a very long thread, written in the style of a blog post, but split into chunks so that people can ask questions or make remarks about specific things I say or ask. I will unlist all but this initial post to avoid clutter in your timeline.
Motivation. Very often we want to extend functions to larger domains of definition. This may or may not possible.
The notion of injectivity is about the possibility of extensions, as we shall see when I eventually give the definition of injective type.
(I don't know where the terminology "injective", for mathematical objects rather than functions, comes from. Who were the first people to use and define it? I am sure this was used before the notion was defined explicitly, as is often the case.)
1/