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

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

It sounds like Thorsten and are both starting to repeat ourselves, so
we should probably spare the patience of everyone else on the list
pretty soon.  I'll just make my own hopefully-final point by saying
that if "properties of the typed algebraic syntax" can imply that the
untyped stuff we write on the page has a *unique* typed denotation,
independent of a particular typechecking algorithm, as mentioned in my
last email, then I'll (probably) be satisfied.  (But at present I
don't see how it can do that without also essentially implying the
initiality theorem for untyped syntax.)

Thanks everyone for a very interesting discussion!

On Thu, May 31, 2018 at 3:06 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> It appears somehow inconsequential to say on the one hand that a typed approach to Mathematics is preferable but then when we talk about type theory itself it is preferable to consider untyped objects first. Doesn't solving the initiality problem just means that you have establish a view on the untyped objects which doesn't depend on them? If we apply the idea of structural Mathematics to type theory itself, isn't it clear that we should take the algebraic view as the fundamental definition? And indeed, using the idea of HITs combined with inductive-inductive it turns out that we can just give an inductive definition of the initial object in this algebraic view. This is nice because indeed HITs were not invented for this particular purpose!
>
> And yes we have to relate this abstract initial object to the stuff we write or type in or create by clicking somewhere (indeed linear syntax may be a thing of the past anyway). We can do this by just establishing properties of the typed algebraic syntax, e.g. decidability and type inference in a way similar as we can understand parsing as the partial inverse of printing trees.
>
> Thorsten
>
>
> On 30/05/2018, 20:07, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:
>
>     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.
>
>     --
>     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.
>
>
>
>
>
> 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.