Still not allowed back to the office due to CORVID-19 close-down. Working from home has its perks – such as playing music on the loudspeakers, not having to sit with headset. But overall I wish the kindergartens would go back to normal opening hours and sit quietly in my office.
Our new phd student, Elisabeth, has had to delay her comming to Bergen due to the close-down, but I hope she will be arriving soon. Meanwhile she started working from Stockholm, which I think is working quite well for her.
Agda is a dependently typed programming language and proof-assistant, which means that you can write formal proofs as programs in it and get them verified by the Agda compiler.
A few years ago I made a formalisation of set theory in HoTT-agda. But when I tried compiling it last year I found that the Agda compiler no longer could compile the HoTT-agda code I was using. In the last few months I have been hoping that HoTT-agda would be updated to the latest version so that I could continue from there. But as far as I can tell the situation is still that the latest Agda will not compile the latest HoTT-agda.
Today, I decided I could not wait any longer. So, I started updating the HoTT-agda code I use. Luckly, there is a note in the description of my previous formalisation work saying which commit of HoTT-agda I had used, and I could start fixing only the stuff I actually need.
It turned out the part of HoTT-agda I used was mostly OK, just a few identifiers (〈-1〉 and 〈-2〉) which were no longer allowed by Agda. But some of my code has gotten some “unsolved metas” – which means that some terms which could be inferred by the unifier in previous Agda versions cannot be found by the most recent version. So, finding those is where I will start tomorrow.
Snow in the air when we woke up today. During the day it cleared up, and even the occasional sun beam reached us – before the real snowfall started. My wife had just gone outside when it started, so she got to enjoy it in its entirety. I was not unhappy to stay inside, working.
In my diary entries from last May, the last snowfall mentioned was 6th of May. But it is not unheard of that it snows on 17th of May.
In Oslo for the weekend, with my oldest. To the natural history museeum. Visited my sister. Good times.
Currently, I have no face online. At least, if you do an image search for my name, my face is not among the ones which show up. It is true that I know a lot of the people who do show up when you search for my name. Relatives, friends, collegues. But there is no picture of me.
I think there are images including my face you could find if you looked hard enough1, but no search engine has connected them to my name. This can of course change. Either because some search engine connects the dots, or because some new picture is posted somewhere clearly connected to me.
There has been some close calls. One of the pictures which shows up when searching for me, shows the winners of the Stockholm Mathematics Center prizes for excellent doctorial dissatations in mathematics. I was given one of these prizes, but did not pay attention when they told me to go for a photo shoot, and went for the cakes in stead. Thus, Olof Bergvall’s picture will show up when you search for my name.
This situation has not really been my intention. I am not so shy that I would be upset if my face showed up online. But I think it is a consequence of my cautious approach to sharing on the Internet. I like sharing ideas, interests and even some personal stuff online. But I like to control the things I share (host it myself). There is also wish of making my own person – and certainly not my look – the center of attention.
How common is this? I guess some people have names so common that they drown out in all their name-siblings. But my father has a unique name, and the closest you get to seeing him when doing an image search for his name is a preset generated cartoon drawing. On the other hand, the first two images when searching for my mother is her along with collegues and an satelite photo of their house.
A lot of people are required to put their images on their employer’s website. Some people have been interviewed for something some time.
Faces are important in human communication. People like to look at faces, and using your face is a powerful tool – weather you are teaching or sellling. But your face is yours. It is not easily changed. It will identify you on surveillence cameras.
Of course, the government has access your face. You give it up in exchange for an identity card, a driver’s licence or a passport. This is a demonstration of the state power. If you enter the US, even for a holiday, your face – along with your fingerprint – is the first thing they take. “Look into the camera, please!”
For instance on Facebook, where I am sure people have put my picture, even though I never had an account there.↩︎
Expecting a comment section? Feel free to e-mail me your comments, or otherwise contact me to discuss the content of this site. See my contact info. You can also write your opinion on your own website, and link back here! ☺