Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
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!


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).

  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:

* 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" ?' \


* 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).