14th Week

Writing the paper

I have started writing the extension to other types for the elaboration section, starting with sigma types and lists. I am not sure how to continue after this, an approach could be to use the W-types encoding to have a simple presentation, but with this approach we do not bring home the main advantage of the Fuss-Free presentation, which can deal with user-defined inductives in all generality. The issue is that introducing a theory of signatures and everything would take too much space, and diverges from the point we are making at presenting a simplifying approach. Maybe presenting the example of W-types formally and then discussing informally a more general approach to inductive types would be a good balance ?

read more

12th Week

The Fuss-Free hierarchy and more general types

I have been reflecting about the Fuss-Free hierarchy and how to use it on general Inductives, or even on user defined types. My original idea was to allow the user to do things like $\mathsf{UserDefinedType}(…)@i$ to indicate that we are asking for the corresponding small type, which we can elaborate in the fuss-free hierarchy by coding and decoding. For instance, if we define a type of lists, then $\mathsf{List}(A)@i$ is a small type, given that $A$ is one. Pushing this further, we can effectively do this for virtually any type, and we only have to add the corresponding rule for closure under smallness, which mimicks the formation rule with the smallness predicate instead of the well-formed type judgement.

read more

10th Week

Elaboration of cumulative universes

This week, I have been reviewing the rules I had written a while ago for the elaboration to the Fuss-Free hierarchy. Those rules had evolved quite a bit over the past few months, as we introduced an explicit casting mechanism to get rid of the problems related with unification. However, now that we went back to a system with no explicit casts, and with the experience of implementing the elaboration in practice, I think that we needed to revisit the rules.

read more

More

9th Week

8th Week

7th Week

6th Week