VojtechStep

The abstract and slides for our TYPES talk "Generating morphism types using parametricity and Trocq" are now available on my website, check them out! This is joint work with Cyril Cohen and Assia Mahboubi.

https://vojtechstep.eu/

My doctoral school organizes an internal "doctorand day" where doctoral students from different domains are supposed to present their ideas to each other. As far as I know nobody really sees the value of this but participation is mandatory.

The program committee assigns every participant either a talk or a poster. A talk means you talk for 10 minutes and then you go home (/back to work). A poster means you need to be there the whole day.

Now, I got assigned a poster. I can't make them give me a talk, but I can try to make them regret giving me a poster (spite is a strong motivator for me, and I like to think I use it constructively).

So since I'm already recycling my topic from my TYPES talk, I decided to recycle the slides as well. Fortunately I had 8 of those, so perfect for just laying them out in a 2x4 grid. I now have both the slides and the poster importing the same slides-contents.typ file which defines all the text and revealing behavior. I'm only overriding polylux's alternatives-match function to work with handout mode, and everything else just works. I'm pretty happy with it!

LB:

In an unexpected turn of events, this evening turned very disappointing (and I haven't even received any news on my FSCD submission). For context, this is what "no consensus" looks like:

Original proposed policy, closed: https://github.com/agda/agda/pull/8456
Current proposed policy:
https://github.com/agda/agda/pull/8507

UIP stands for Uomotopy Iype Pheory

Oh how I wish my server with the IRC bouncer hadn't died while I was in a different country

@whitequark@social.treehouse.systems do the 88x31 buttons from grebedoc's website exist for git-pages?

Proof assistant called mikan

Implements cubicalTT instead of globularTT

This is what happens when you stray away from the path of the birb

(the FSCD paper got rejected)