From: Ulrik Buchholtz <ulrikbu...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Identity versus equality
Date: Sun, 10 May 2020 08:35:17 -0700 (PDT) [thread overview]
Message-ID: <7b9eb7c9-040a-46e8-b470-28958f8d7713@googlegroups.com> (raw)
In-Reply-To: <CA+AZBBovtP9H9rLhZOFio2dj+83uYvwmb9dd76JrMGM3gz30sQ@mail.gmail.com>
[-- Attachment #1.1: Type: text/plain, Size: 2008 bytes --]
On Sunday, May 10, 2020 at 4:27:30 PM UTC+2, Nicolai Kraus wrote:
>
> I agree with Mike - sorry Ulrik :-)
> For me, "everything is based on sets" would mean that every fibrant type
> can be written as the realization of a (semi-) simplicial type, or
> something like this.
>
No need to apologize: I know I was being slightly provocative by
juxtaposing a question about sets cover (SC) and a comment on 2-level type
theory in this context, in order to provoke some discussion :-)
Wouldn't you agree, however, that even though basic 2LTT is conservative
over HoTT, from a certain point of view, 2LTT privileges the “ground floor”
exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you
decorate the inner (fibrant, endo-) types as special, and leave the
exotypes undecorated, privileging the latter. While from a user's
perspective, however, it's the (inner) types that are
standard/mathematical, and the exotypes that are special.
And regardless of the decorations, the mere fact that we bring in the
exoset level makes the theory harder to justify from the philosophical
position that general homotopy types are not reducible to sets. One can in
fact see the conservativity result as foundational reduction (in the sense
of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5) from
a system justified by the principle that everything is based on sets to a
system justified by a framework where that isn't the case.
Another connection is that it seems it should be easier to find an axiom,
which might imply SC, that would allow us to construct the type of
semi-simplicial types, rather than such an axiom that doesn't imply SC. But
I don't know any such axiom statable in book HoTT either way.
BTW, you probably meant “simplicial set” above. And yes, that kind of axiom
would be the strongest expression of “everything is based sets”, and it
currently needs 2LTT to even be stated.
Cheers,
Ulrik
[-- Attachment #1.2: Type: text/html, Size: 2371 bytes --]
next prev parent reply other threads:[~2020-05-10 15:35 UTC|newest]
Thread overview: 61+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-05-05 8:47 Ansten Mørch Klev
2020-05-06 16:02 ` [HoTT] " Joyal, André
2020-05-06 19:01 ` Steve Awodey
2020-05-06 19:18 ` Michael Shulman
2020-05-06 19:31 ` Steve Awodey
2020-05-06 20:30 ` Joyal, André
2020-05-06 22:52 ` Thorsten Altenkirch
2020-05-06 22:54 ` Thorsten Altenkirch
2020-05-06 23:29 ` Joyal, André
2020-05-07 6:11 ` Egbert Rijke
2020-05-07 6:58 ` Thorsten Altenkirch
2020-05-07 9:04 ` Ansten Mørch Klev
2020-05-07 10:09 ` Thomas Streicher
2020-05-07 16:13 ` Joyal, André
2020-05-07 21:41 ` David Roberts
2020-05-07 23:43 ` Joyal, André
2020-05-07 23:56 ` David Roberts
2020-05-08 6:40 ` Thomas Streicher
2020-05-08 21:06 ` Joyal, André
2020-05-08 23:44 ` Steve Awodey
2020-05-09 2:46 ` Joyal, André
2020-05-09 3:09 ` Jon Sterling
[not found] ` <CADZEZBY+3z6nrRwsx9p-HqYuTxAnwMUHv7JasHy8aoy1oaGPcw@mail.gmail.com>
2020-05-09 2:50 ` Steve Awodey
2020-05-09 8:28 ` Thomas Streicher
2020-05-09 15:53 ` Joyal, André
2020-05-09 18:43 ` Thomas Streicher
2020-05-09 20:18 ` Joyal, André
2020-05-09 21:27 ` Jon Sterling
2020-05-10 2:19 ` Joyal, André
2020-05-10 3:04 ` Jon Sterling
2020-05-10 9:09 ` Thomas Streicher
2020-05-10 11:59 ` Thorsten Altenkirch
2020-05-10 11:46 ` Thorsten Altenkirch
2020-05-10 14:01 ` Michael Shulman
2020-05-10 14:20 ` Nicolai Kraus
2020-05-10 14:34 ` Michael Shulman
2020-05-10 14:52 ` Nicolai Kraus
2020-05-10 15:16 ` Michael Shulman
2020-05-10 15:23 ` Nicolai Kraus
2020-05-10 16:13 ` Nicolai Kraus
2020-05-10 16:28 ` Michael Shulman
2020-05-10 18:18 ` Nicolai Kraus
2020-05-10 19:15 ` Thorsten Altenkirch
2020-05-10 19:20 ` Thorsten Altenkirch
2020-05-10 12:53 ` Ulrik Buchholtz
2020-05-10 14:01 ` Michael Shulman
2020-05-10 14:27 ` Nicolai Kraus
2020-05-10 15:35 ` Ulrik Buchholtz [this message]
2020-05-10 16:30 ` Michael Shulman
2020-05-10 18:56 ` Nicolai Kraus
2020-05-10 18:04 ` Joyal, André
2020-05-11 7:33 ` Thomas Streicher
2020-05-11 14:54 ` Joyal, André
2020-05-11 16:37 ` stre...
2020-05-11 16:42 ` Michael Shulman
2020-05-11 17:27 ` Thomas Streicher
2020-05-10 16:51 ` Nicolai Kraus
2020-05-10 18:57 ` Michael Shulman
2020-05-10 19:18 ` Nicolai Kraus
2020-05-10 20:22 ` Michael Shulman
2020-05-10 22:08 ` Joyal, André
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=7b9eb7c9-040a-46e8-b470-28958f8d7713@googlegroups.com \
--to="ulrikbu..."@gmail.com \
--cc="HomotopyT..."@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).