TODO

TODO:

• Merge compU into master to use the more efficient algorithm for composition in the universe.

• Remove the constraint that glue takes a five-tuple, it should be possible to give it a variable which refers to an iso. (Didn't we have this at some point?)

• Introduce both glue and glueIso so that we can easily experiment with glueing with equivs and isos.

• Add split as an expression (with an extra argument for the type). This should simplify some examples as we can use nested splits again.

• Rename Id into Path.

• Merge the Id types branch and prove univalence for Id. (Maybe Simon already did this?)

• Clean and add more examples.

• Rewrite to use partial elements as in the paper. Maybe more efficient?

• Explicit support to optimize the code.

• Better error messages.

• Generate better names for dimensions and make sure that we print things so that they can be parsed back and typechecked?

• Add an option to normalize and parse+typecheck the output?

• Add a flag to run the code in batch mode (ie just typecheck a file without entering the REPL loop).

• Correct the program for HITs

• Rewrite Guillaume's pi4s3 example

Finished: