#HoTT #CubicalAgda
I'm trying to wrap my head around how `hcomp` works. In particular, does it have any definitional equalities? Would `hcomp {φ = i1} u u0` be definitionally equal to `u i1 1=1` for instance? I don't see a reference to any such reductions in the documentation.

Ok so the past few days a lot of criticism of indexed inductives in #cubicalagda #agda has been going in and this is just my two cents from a user perspective but I defined (a datatype for lists indexed by the multisets of their elements)[http://partiallyapplied.eu/correct-bialgebraic-sorting/DistrLaw.html#1275] and successfully used it to define intrinsically correct sorting algorithms using bialgebraic semantics.

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