April 2020

2020–04–06, Saturday

Day a lot of the CORVID-19 close-down. Gave up on making a note every day of the close-down. Getting into some kind of workable routine at home, but there is still no hope for working at full speed under these conditions.

On a positive note, I got very constructive feedback on my article on non-wellfounded sets in Homotopy Type Theory, through a referee report. As noted previously, I finished a first version of the article, and put it on arXiv. The idea had been bubbling around in my head for a while, but the write-up was done in a hurry and during quite a stressful time. But the referee feedback was very constructive and I will put in a good effort to improve it before the final submission.

Apart from various fixes and suggestions for improvement, the referee pointed out that one of the definitions (Definition 5 in the first version) was not obviously well-formed – internally, because of size considerations. Motivated by this I will go ahead and (if possible) formalise that part in Agda to make sure that it is actually sound.

The referee is of course anonymous, and I will not speculate whom they be – although I probably know them – but they were very polite and nice in their report. They sugested that in the worst case the size issue could be solved with a super universe. That is definitately doable, but I hope that by being a bit carefull, it can be spelled out without that.

2020–04–18, Saturday

Still undergoing CORVID-19 close-down. Awesome spring weather today – a chance to wear the leather jacket I got for Christmas.

Today my wife and I celebrated our fifth weddding aniversary by ordering sushi, eating it with some oolong.

jack_mixer default MIDI controls

I really like jack_mixer – a MIDI controlled graphical mixer for JACK. It does what it is supposed to quite well, and nothing else. I have it connected to my FAD.9 MIDI controller, from Omnitronic, and thus I have a very convenient way of mixing all the sound on my computer.

There is however one thing which annoys me, and that is that there is no way to change the CC numbers for the MAIN output: volume is 7 and balance is 8. These correspond to faders 5 and 6 on my MIDI controller, but I would like to use another fader (CC 11) and an knob(CC 22):

The simplest solution I could find was to use a Python library called mididings which allows filtering and modificaitons of MIDI signal. The following Python-script remaps the controls how I would like:

from mididings import *
config(
    backend='jack-rt',
    client_name='remap_midi',
)
run([CtrlFilter(11,22) >> CtrlMap(11, 7) >> CtrlMap(22, 8), 
     CtrlFilter( 7, 8) >> CtrlMap( 7,11) >> CtrlMap( 8,22),
     -CtrlFilter(7,8,11,22)])

The syntax is perhaps not self explaining. But the idea is that run executes the list in parallell, and the >> operator runs filters and actions in sequence.

So this filter has three parallell components:

• CtrlFilter(11,22) >> CtrlMap(11, 7) >> CtrlMap(22,8) matches CC 11 and CC 22, but remaps them to CC 7 and CC 8
• CtrlFilter(7,8) >> CtrlMap(7,11) >> CtrlMap(8,22) matches CC 7 and CC 8, but remaps them to CC 11 and CC 22.
• -CtrlFilter(7,8,11,22) lets all other signals through.

Thus, the net effect is that CC 7 is swapped with CC 11 and CC 8 is swapped with 22, keeping all the other signals intact. This solves the problem illustrated above, and wires the right fader to the right volume knob.

2020–04–24, Friday

Still undergoing CORVID-19 close-down. The good weather is still with us – and it has been a great relief for the children in kindergarten, where they are social distancing by being outside a lot more – but the forecast for Monday shows 🌧.

Taking a picture of The Evening Star.

I have never been much of a star watcher. But tonight the stars were very visible from our balcony, and on a whim I decided to take a picture of The Evening Star.

The Evening Star is not a star at all, but rather the planet Venus when it appears over the western horizon. But with the naked eye it is difficult to see that it is in fact a planet lit by the Sun, not a powerful, far away star. So that is what I wanted to see if I could capture it with my camera, in a way that would make it more visible that the little shiny dot in the sky is actually a planet.

My camera is a Canon EOS 500D, and I have two lenses for it: the kit lens 18–200mm super zoom and a Sigma EX 30mm “prime lens”. The prime lens would be of no help here, but a 200 milimeter lense might just be able to make out the outline of the planet.

So, a bit of fidling with the exposure settings, and a few failed attempts later, and I got the following picture:

If you zoom in on this picture, you can see that Venus does not appear to be completely round. This is because Venus is lit by the Sun only on one half at the time, and therfore has phases – just like the moon!

A 200mm lens gives quite a bit of magnification, but even so Venus, whose diameter is about 6052km, is only about 10 pixels wide in the picture. Or to put it differently, the picture has about 0.000000042 DPI (dots per inch)!

Here is a cropped and scaled up, and thus very blurry, version of venus from the above:

2020–04–25, Saturday

My friend John¹ invited me for some boargames online today. Together with his wife and his brother and his girlfried, we played Carcassonne.

Carcassonne is a classic board game, where you build cities, roads and churches in order to get points. But I hadn’t looked up the city Carcassonne, which the board game is named after, before. But this time I did, and found that the tiles actually look like the city does, even today: