From: Corlin Fardal <fardalcorlin@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Re: 1D Mu Type
Date: Wed, 22 Aug 2018 16:54:58 -0700 (PDT) [thread overview]
Message-ID: <6f8e170d-0c46-4b2f-a606-2a5ffb5ae3a4@googlegroups.com> (raw)
In-Reply-To: <45604a7e-3ecd-4caa-90a9-ad8c5a257756@googlegroups.com>
[-- Attachment #1.1: Type: text/plain, Size: 868 bytes --]
I could tell that the path algebra was doing something similar to my
original coerce function, I was just curious how exactly it worked, with
perhaps a breakdown of what each part is doing, and how you even came up
with the term in the first place, it seems non-obvious to me, to say the
very least. Also, I knew that the choice of putting it on the left or the
right was equivalent, I tried to say as much, but seeing as it aligns with
what you do in the HIITs paper, I was curious if there was a particular
reason you seem to prefer the left over the right.
--
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: 1051 bytes --]
prev parent reply other threads:[~2018-08-22 23:55 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
2018-08-22 13:05 ` András Kovács
2018-08-22 2:27 ` Corlin Fardal
2018-08-22 23:54 ` Corlin Fardal [this message]
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=6f8e170d-0c46-4b2f-a606-2a5ffb5ae3a4@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).