Last week, I continued reading about pattern unification and tried to figure things out by reading Andras' code for “Observing definitional equality”. I am slowly trying to integrate it to my code, but for now this is clearly at an early stage, and I am a bit struggling to figure things out from Andras’ code as there is a lot going on there, with a lot of features implemented all at once. I will continue working on this more thoroughly this week.
I’ve been working on finding a concise way to formulate the natural universe hierarchy, such that all the structural rules follow from functoriality and naturality condition. The idea is to work in a logical framework to specify the signature of our theory in a categorical way. This was a lot of fun ! Maybe there are also interesting ideas to get from the paper A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism, that I should probably try to read at some point.
I have been continuing my implementation of the fuss-free hierarchy this week, Last week, I added synthesis rule for Pi and U, but that is not necessary if we write another function ‘checkTy’ which corresponds to a new judgment in the bidirectional typing algorithm, which checks a term against Type. We can also add an optional size to this judgement, which tells the elaborator to check it against $Small_i$ and produces a small type. I have implemented all of that, and it seems to be working! I still need to put my implementation to more tests though.