Re: [HoTT] "Identifications" ?

[Thomas Streicher <stre...@mathematik.tu-darmstadt.de>]

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