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.
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! ☺