```
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 Altenkirch2020-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

Be sure your reply has aReply 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-toswitches 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 \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader 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).