I have a few questions/comments about Kovács' version. First of all, is the Empty constructor necessary? It seems like we could replace it with Const empty, and replace exfalso with a lifted function. Additionally I'm kind of
struggling to understand what the path algebra in the definition of Section is actually doing, is there a simple explanation? Also, though this doesn't really matter, why is the path
algebra on the left side of the equation, instead of the right? It feels like the computation rules essentially define induction, so it feels like the left side should say "this is the application
of the function," and the right should say "this is the value of that application". Additionally, as one last little nitpick, my name's Fardal not Fardar, as thecomment at the top of the file
says, though that really doesn't matter much. However, despite all of my nitpicks/confusions, I really like your version of it. The reformulation of the lambda term feels obvious but
clever, and I'm kind of mad at myself for not coming up with it, seeing as one of the problems I was having was defining a quotient type in my version. I also like the connection made
between the all function and the coerce function, I didn't realize the connection there, as, at the very least, the two functions needed to finish the computation rules. In general I like the
method of building from the algebras to the displayed algebras to the sections, it gives the Mu type at the end a very nice definition. The names of the sections sound algebraic, but I'm
actually not quite sure what they mean. I mean, I know what an algebra is, I'm relatively well versed in the categorical semantics of at least simple inductive types, but what are
displayed algebras, or displayed algebra sections? Displayed algebras seem to have at least some connection to the fibred algebras of the Higher Inductive Types as Homotopy-Initial
Algebras paper, and I have some idea of what sections are, but is there anything deeper that I don't know about?
Now, if you'll excuse me, I'm going to go mess around with the HIIT paper's system and Kovác's version of my system to see if I can't understand both of them more, along with HITs
in general.