I’m pretty sure I had actually read the HIITs paper before, but I’d completely forgotten about it. Reading back through it it’s kind of amazing that I had, considering how much it manages to do very simply. I’d also read the QIITs paper, but, like I did with the IITs paper, gotten lost in the category-theoretical brushes, and ended up missing the fact that a quotient construction would require AC, though I'm not entirely surprised by that, I kind of figured it might. I did further know about the construction by Lumsdaine and Shulman, but I wasn't entirely certain if that applied to my construction, it's been a while since I've read that section of the paper, but as far as I can recall they didn't provide the actual definition of the HIT, so while I knew that it would be impossible to construct any HIT from quotients, I thought that the subset I had created a Mu type for might still be constructible, and not contain their HIT.

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 if they're meant to be computation rules, it should compute from the left down to the right, and because of that it

feels like it ought to go from the simple application of induction to the path, down to a more complex expression. Additionally, as one last little nitpick, my name's Fardal not Fardar, as

comment 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.