[FOM] A Meaning Explanation for HoTT?

[Stephen Gaito]

Dimitris,

Please continue, I need to understand better where you are heading.

On Thu, 14 Apr 2016 18:16:14 -0400
Dimitris Tsementzis <dtsement at princeton.edu> wrote:

> BASIC IDEA: The rules of HoTT are instructions for constructing new
> shapes from old.

[...]

> B. JUDGMENTS AS OBSERVATIONS

[...]

> A feature of this set-up which may already appear striking is the
> absence of any mention of “truth". This is both intentional and, to a
> certain extent, inevitable. The ``observations'' of the four basic
> types (1)-(4) above are best understood within a
> ``problems-and-constructions'' view of mathematics, closer in spirit
> to the Euclid than to Russell. A notion of truth can then be
> recovered as a degenerate notion of construction, namely when we
> ignore all details of the construction itself and retain only the
> information that it exists (or that it is possible). 

I find that I am not so far out on a limb as I once
thought and that we might be heading in similar directions.

If I am correct that we are heading in a similar direction, then I am
very confident that we *can* answer Harvey Friedman's requested
elaboration:

> We now need to see 1-4 in action with some baby examples. Perhaps a
> bit like
> 
> nothing
> just emptyset
> just emptyset, {emptyset}
> just emptyset, {emptyset}, {{emptyset}}, {emptyset, {emptyset}}.
> just those obvious 16 obvious sets.

BUT before I/we can do that I need to understand more about where you
are going...

SO PLEASE continue!

Regards,

Stephen Gaito