Diary – December 2019

2019–12–01, Sunday

Finished up the first version of my article on non-wellfounded sets in HoTT. Hopefully I will have time to also put it on arXiv next week.

2019–12–03, Tuesday

Discussed how to apply dependent types to GUI specifications with Jaakko and his master student, Knut¹. Jaakko is on a mission to improve how GUIs are written. He has a JS library, HotDrink, which provides a way to generate GUI based on a specification and implementing some contstraints. He has also taken on multiselection. We are currently trying to see if we can get some leverage out of dependent types in HoTDrink-kinds of specifications.

2019–12–08, Sunday

Visiting UiO in the upcoming week, to collaborate with Henrik. We are exploring theories of presheaf type.

Today I have also been playing Minecraft. I started playing Minecraft in 2010, when it was still at a very early stage of development. We had a multiplayer server for many years, but while we had a lot of cool stuff there, the landscape got very fragmented when they changed the generation algorithms. So when I picked it up again this summer I started a new world.

The world is a large biome world and players start out several kilometers from each other. I am pretty happy with my current building, which is a large mansion/castle in the woods. After all the players have visited me, I might post pictures of it here. There are some really cool features, which I want the others to see in-game before they see it here.

As the server admin I have been experimenting with command blocks for various functions. Best so far is teleportation buttons from one player’s base to another, provided that they first walk there themselves. Also, everyone gets a teleport button to “Civilisation”, which is a common area near the center of the world. I protected Civilisation with a wall and plenty of light, so that it can be fun hangout for everyone. Inna has set up a shop there, and we also built a hut with bookshelves and an enchantment table. A nether portal gives a different way of comming to town.

2019–12–23, Monday

More Minecraft over the weekend.