From: Andrej Bauer <andrej...@andrej.com>
Cc: Homotopy Type Theory <homotopyt...@googlegroups.com>,
Univalent Mathematics <univalent-...@googlegroups.com>
Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality
Date: Mon, 16 Oct 2017 01:42:54 +0200 [thread overview]
Message-ID: <CAB0nkh3E25ZQgc7_vEO-695rd2qeSf3sh8rOHig08Bt_VMRw-g@mail.gmail.com> (raw)
In-Reply-To: <20171014095243.GA29903@mathematik.tu-darmstadt.de>
> you are right in the sense that the free model of a certain type
> theory T is not trivially isomorphic the syntax modulo. The late
> Voevodsky suggested this to be an important problem and Peter
> Lumsdaine has worked on it for some time.
I absolutely agree with Vladimir's insisting that actually proving
good, robust, and general theorems about initiality of syntactic
models is not only important, but also an open problem. We have
*instances* of such theorems (with many thanks to you, Thomas), but no
general theory.
I would warn against repeating or spreading the opinion that such
general theorems either exist, or are somehow not worth proving, or
worse, that they are easy. And the reason for this is that I am
working with Peter on them, and it's really not as easy or as boring
as many would seem to presume.
> It feels a bit like a non-mathematical problem in the sense of being
> more organizational or CS like.
Call it what you like. Isn't all of logic organizational?
With kind regards,
Andrej
P.S. Why are we cross-posting everything between HoTT and Univalent
mathematics lists?
next prev parent reply other threads:[~2017-10-15 23:42 UTC|newest]
Thread overview: 47+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-10-12 18:43 Dimitris Tsementzis
2017-10-12 22:31 ` [HoTT] " Michael Shulman
2017-10-13 4:30 ` Dimitris Tsementzis
2017-10-13 15:41 ` Michael Shulman
2017-10-13 21:51 ` Dimitris Tsementzis
2017-10-13 0:09 ` Steve Awodey
2017-10-13 0:44 ` Alexander Altman
2017-10-13 15:50 ` Michael Shulman
2017-10-13 16:17 ` Steve Awodey
2017-10-13 16:23 ` Michael Shulman
2017-10-13 16:36 ` Matt Oliveri
2017-10-14 14:56 ` Gabriel Scherer
2017-10-15 7:45 ` Thomas Streicher
2017-10-15 8:37 ` Thierry Coquand
2017-10-15 9:26 ` Thomas Streicher
2017-10-16 5:30 ` Andrew Polonsky
2017-10-15 10:12 ` Michael Shulman
2017-10-15 13:57 ` Thomas Streicher
2017-10-15 14:53 ` Michael Shulman
2017-10-15 16:00 ` Michael Shulman
2017-10-15 21:00 ` Matt Oliveri
2017-10-16 5:09 ` Michael Shulman
2017-10-16 12:30 ` Neel Krishnaswami
2017-10-16 13:35 ` Matt Oliveri
2017-10-16 15:00 ` Michael Shulman
2017-10-16 16:34 ` Matt Oliveri
2017-10-16 13:45 ` Matt Oliveri
2017-10-16 15:05 ` Michael Shulman
2017-10-16 16:20 ` Matt Oliveri
2017-10-16 16:37 ` Michael Shulman
2017-10-16 10:01 ` Thomas Streicher
2017-10-15 20:06 ` Matt Oliveri
2017-10-13 8:03 ` Peter LeFanu Lumsdaine
2017-10-13 8:10 ` Thomas Streicher
2017-10-14 7:33 ` Thorsten Altenkirch
2017-10-14 9:37 ` Andrej Bauer
2017-10-14 9:52 ` Thomas Streicher
2017-10-14 10:51 ` SV: " Erik Palmgren
2017-10-15 23:42 ` Andrej Bauer [this message]
2017-10-15 10:42 ` Thorsten Altenkirch
2017-10-13 22:05 ` Dimitris Tsementzis
2017-10-13 14:12 ` Robin Adams
[not found] <B14E498C-FA19-41D2-B196-42FAF85F8CD8@princeton.edu>
2017-10-14 9:55 ` [HoTT] " Alexander Altman
2017-10-16 10:21 Thorsten Altenkirch
2017-10-16 10:42 ` Andrew Polonsky
2017-10-16 14:12 ` Thorsten Altenkirch
2017-10-16 10:21 Thorsten Altenkirch
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=CAB0nkh3E25ZQgc7_vEO-695rd2qeSf3sh8rOHig08Bt_VMRw-g@mail.gmail.com \
--to="andrej..."@andrej.com \
--cc="homotopyt..."@googlegroups.com \
--cc="univalent-..."@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).