[HoTT] Re: 1D Mu Type

[Corlin Fardal <fardalcorlin@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 3563 bytes --]

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

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 5965 bytes --]