From: Corlin Fardal <fardalcorlin@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Re: 1D Mu Type
Date: Tue, 21 Aug 2018 18:49:45 -0700 (PDT) [thread overview]
Message-ID: <c5f3ecf2-ecd9-49a1-b842-f9163cfab469@googlegroups.com> (raw)
In-Reply-To: <45604a7e-3ecd-4caa-90a9-ad8c5a257756@googlegroups.com>
[-- Attachment #1.1: Type: text/plain, Size: 3586 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 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.
[-- Attachment #1.2: Type: text/html, Size: 5537 bytes --]
next prev parent reply other threads:[~2018-08-22 1:49 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-08-18 21:30 [HoTT] " Corlin Fardal
2018-08-21 11:12 ` [HoTT] " Niels van der Weide
2018-08-21 11:20 ` András Kovács
2018-08-22 1:49 ` Corlin Fardal [this message]
2018-08-22 13:05 ` András Kovács
2018-08-22 2:27 ` Corlin Fardal
2018-08-22 23:54 ` Corlin Fardal
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=c5f3ecf2-ecd9-49a1-b842-f9163cfab469@googlegroups.com \
--to=fardalcorlin@gmail.com \
--cc=HomotopyTypeTheory@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).