It's time to get started on my master thesis! I don't have a precise topic yet, but I'm thinking of formalising something type-system-y in #agda / #cubicalagda. I haven't worked with cubical Agda or #HoTT yet, so I think I'll dive into it with somethin like 1Lab or the HoTT book to get a rough understanding of the area. Hopefully then I'll be able to formulate a precise topic I like soon. I would also love ideas or tips, by the way :D