In order to better understand how Glue types work, I reproved uaOver using Glue directly instead of using path composition. Is this a worthwhile addition to the library? The normalised term is about as big as the term obtained by hcomp, but I made sure to add a few lines of comments that explain what's going on.
In order to better understand how
Gluetypes work, I reproveduaOverusingGluedirectly instead of using path composition. Is this a worthwhile addition to the library? The normalised term is about as big as the term obtained byhcomp, but I made sure to add a few lines of comments that explain what's going on.