Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman <shu...@sandiego.edu>]

On Wed, May 30, 2018 at 5:05 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> Set theory is untyped and conceptually misleading, to
> talk about all natural numbers you quantify over all sets singling those out
> that represent natural numbers. Untyped thinking leads to non-structural
> Mathematics, to mathematical hacking and a lack of abstraction. Indeed, the
> impossibility to hide anything in an untyped universe is one of the diseases
> of contemporary Mathematics.
>
> ...
>
> The problem is that people still use untyped Mathematics.

I agree entirely with this.  Some set theorists like to say that the
untypedness of set theory is not a problem because one can still do
"structural" (i.e. typed) mathematics inside set theory.  This is true
-- IF you know what "structural/typed mathematics" means and you know
what you are doing!  The real problem is that if you learn untyped set
theory as "the" foundation of mathematics, then it requires an extra
step of *learning* to work structurally, i.e. to "forget about" the
ability to do untyped things.  Personally, I have noticed this problem
most when I am refereeing papers -- it seems to be a frequent source
of errors to, for instance, make a non-structural definition and then
use it in ways that would only make sense if it were structural.

However, the "typedness of mathematics" is for me a *semantic*
statement: the "real objects" of mathematics are typed, but that
doesn't necessarily mean that the *language we use to talk about them*
must (or even can) be typed.  There are "more semantic" notions of
"typed syntax", but ultimately what we actually write down is untyped,
so somewhere there is a necessary step of "typechecking" it.

Moreover, I currently still believe that we need not just an algorithm
to typecheck untyped syntax into typed syntax, but a full proof of the
initiality theorem for a structure built out of untyped syntax.  The
problem is that I want to be sure I know what is denoted by the
untyped syntax I write down.  Maybe you have a typechecking algorithm
that compiles it into typed syntax and thereby gives it a semantic
meaning, but maybe someone else has a different typechecking algorithm
that produces an *a priori* different typed syntax; how do I know that
the "meaning" of what I write down doesn't depend on which
typechecking algorithm I choose?  The most natural way I can see to be
sure of this is to show that untyped syntax assembles into the same
initial structure that typed syntax does.

>
>
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.