From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de> To: Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> Cc: "homotopyt...@googlegroups.com" <homotopyt...@googlegroups.com> Subject: Re: [HoTT] "Identifications" ? Date: Mon, 4 May 2020 14:39:39 +0200 [thread overview] Message-ID: <20200504123938.GA15963@mathematik.tu-darmstadt.de> (raw) In-Reply-To: <31C5A7B0-8512-4ABD-8DAA-EF3A1FA0EEFF@nottingham.ac.uk> Hi Thorsten, > But I am not "interpreting HoTT in SSet". I am just working in HoTT. You are doing Metamathematics, I am just talking about Mathematics. > > Sure when you consider models of your theory you can say that certain equalities are just metatheoretic equalities and others are non-trivial equalities. I am not sure what you really mean but I guess you refer to the distinction between what is provable in HoTT and what holds or exists in particular models. Of couse, Nicolai"s vexing example is model dependent (at least in my reconstruction!) But that is the same in set theory. Most of the time you are model independent, i.e. provable in ZFC or actually much weaker systems. But there are quite a few things which heavily depend on the model. Continuum Hypothesis for example but many other things as well. Modern set theory is essentially about independences... And if you consider ZF the notions of finite and Dedekind finite are different. That is in my opinion an example where incompleteness strikes already on a very basic level! Thomas PS But I agree that this is "metamathematical" but so what. Mathematics is not one fixed game but rather pluralist even classically. Even more so constructively where things branch much earlier. As a (categorical) logician one is interested in constructive mathematics precisely because of this excessive pluralism! I never understood why constructive math is used in the singular since it is even false for classical maths. And adding strong principles doesn't mean one gets nonalgorithmic. Adding to HA all true Pi^0_1 sentences doesn't allow you to construct functions on N which are not recursive (as follow from number realizability).
next prev parent reply other threads:[~2020-05-04 12:39 UTC|newest] Thread overview: 26+ messages / expand[flat|nested] mbox.gz Atom feed top 2020-05-04 9:35 Thorsten Altenkirch 2020-05-04 10:59 ` [HoTT] " stre... 2020-05-04 11:04 ` Steve Awodey 2020-05-04 11:17 ` Thorsten Altenkirch 2020-05-04 11:42 ` Nicolai Kraus 2020-05-04 12:04 ` Thorsten Altenkirch 2020-05-04 12:06 ` Thomas Streicher 2020-05-04 12:12 ` Thorsten Altenkirch 2020-05-04 12:39 ` Thomas Streicher [this message] 2020-05-04 13:16 ` Michael Shulman 2020-05-04 14:17 ` Thorsten Altenkirch 2020-05-04 14:48 ` Stefan Monnier 2020-05-04 15:46 ` Nicolai Kraus 2020-05-04 15:57 ` Thorsten Altenkirch 2020-05-04 15:59 ` Michael Shulman 2020-05-04 16:07 ` Steve Awodey 2020-05-04 16:17 ` Thorsten Altenkirch 2020-05-04 16:53 ` Steve Awodey 2020-05-04 17:25 ` Thorsten Altenkirch 2020-05-04 17:43 ` Michael Shulman 2020-05-04 17:55 ` Steve Awodey 2020-05-04 16:21 ` Peter LeFanu Lumsdaine 2020-05-04 16:16 ` Joyal, André 2020-05-04 20:38 ` Joyal, André 2020-05-07 19:43 ` Martín Hötzel Escardó 2020-05-08 10:41 ` [HoTT] " 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=20200504123938.GA15963@mathematik.tu-darmstadt.de \ --to="stre..."@mathematik.tu-darmstadt.de \ --cc="Thorsten...."@nottingham.ac.uk \ --cc="homotopyt..."@googlegroups.com \ --subject='Re: [HoTT] "Identifications" ?' \ /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
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).