Re: [HoTT] Re: 1D Mu Type

["András Kovács" <puttamalac@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 6428 bytes --]

>
> my name's Fardal not Fardar


Sorry, fixed it.

First of all, is the Empty constructor necessary?


Fair point, it isn't necessary, I removed it now.

 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?


The last component of Section is just the weak (propositional) beta rule
for path constructors. If every point computation rule held definitionally,
then the path beta would be simply
(apd (Fˢ Id Xˢ) (paths gx) ≡ pathsᴰ gx (Fˢ g Xˢ gx))), which has the form
we usually see when people use HITs (with definitional point beta). Since
path beta rules are generally only well-typed up to point beta rules, we
need to refer to Tmˢ t and Tmˢ u to make it well-typed, so the left side is
wrapped in an extra composition. It's an arbitrary choice whether to
compose with point beta rules on the left side of the equation or the right
side, since the two versions are equivalent.

The names
> of the sections sound algebraic, but I'm actually not quite sure what they
> mean


It follows the terminology we use in the followup draft
<https://github.com/AndrasKovacs/misc-stuff/blob/master/publications/ConstructingQIITs-draft.pdf>
to
the HIIT stuff. In the HIIT paper we used "constructors", "motives/methods"
and "eliminators", but the new terminology is much better.  I think Mike
Shulman previously used the terms "algebra", "dependent algebra", and
"dependent algebra section". We use "displayed" instead of "dependent"
because displayed algebras generalize Ahrens and Lumsdaine's displayed
categories, in a rather precise way.

In general, semantics for a inductive types should include constructing a
category of algebras for each syntactic declaration, where algebra
homomorphisms are the morphisms. However, if we only have a category, we
can only talk about initiality (unique recursion), but not about induction,
because that needs a notion of dependent object/family/fibration. So we
need to have a category with a notion of dependent objects. In the draft
paper we use CwF (category with families) where displayed algebras and
sections form the "F" part, but there are probably other workable choices
as well.

Corlin Fardal <fardalcorlin@gmail.com> ezt írta (időpont: 2018. aug. 22.,
Sze, 3:49):

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

-- 
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 #2: Type: text/html, Size: 10447 bytes --]