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

[Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>]

[-- Attachment #1: Type: text/plain, Size: 6466 bytes --]


I just had a chance to catch up and watch the video which
prompted this disucussion last night.  I'm a huge fan of the idea
of trying to understand and make precise the notion of "higher
category with families" and what that might say about the syntax
of type theory.  So my question is probably mostly directed at
Thorsten, but I am curious to hear other people's responses as
well.

I guess my question is pretty simple: why should we insist,
as Thorsten seems to, that the "intrinsic" syntax of type
theory form a set?

I am a bit late and it seems that Mike has already given a nice answer. In a computational reasonable version of type theory we should be able to compute normal forms and be able to show that the terms (with a non-trivial equality) are equivalent and hence the terms form a set. This also entails important properties for an implementation which is one of the reasons that we are interested in a computationally adequate type theory. If we define a version of higher type theory which we can't normalize then maybe there is something missing. But actually I think that a naïve version of higher type theory (using (infinity,1)-version of the usual definition) should be fine and we should eb able to transfer the usual normalisation by evaluation construction to this setting.

Now, there are interesting type theories that are not computationally adequate. Extensional type theory (ETT) was already mentioned. In a higher setting the equality reflection principle of ETT should actually become that propositional equality and judgemental equality are equivalent. The type theory (o.e. the initial algebra) that also features univalence and maybe HITs will not be a set. I think it should be possible to relate such a semantic (extensional) theory to a computational (intensional) one via a conservativity theorem along the lines of Martin Hofmann's conservativity theorem that showed that ETT is conservative over ITT with functional extensionality and uniqueness of equality proofs.

I can, I think, anticipate the first response: well, we want to
have a type-checking algorithm.  And, in light of the conversion
rule, this typically means that we will have to reduce type
expressions to a normal form and check if they are equal.  Hence,
if we don't have decidability of the syntax, we cannot have
decidability of typechecking.  Am I right that this is the principle
motivation for having decidable syntax?

But, then, this seems to be a statement about *extrinsic* syntax.

You can relate explicit syntax (I.e. term trees) to intrinsic syntax and type checking is the problem to decide wether a given tree is the underlying representation of a derivation. This is actually similar to the problem of parsing where we can print a tree and the problem is given a string to find a tree that prints as the term.

  If,
as Thorsten advocates, we somehow manage to produce a highly
structured, internal description of the syntax of type theory,
then typechecking for this syntax is, by definition, unnecessary!  After all,
the whole point is that in such a setup, only the well-typed terms
even make sense (i.e., are typeable in the meta-language).

So from an internal perspective, I cannot think of any reason to
insist on decidability.  And consequently, insisting that an
internal higher category with families be univalent does not seem
in any way strange to me.

But maybe there is some other objection that I'm not seeing?

Eric

On Fri, Jun 1, 2018 at 7:07 PM Martín Hötzel Escardó <escardo...@gmail.com<mailto:escardo...@gmail.com>> wrote:


On Thursday, 31 May 2018 20:02:51 UTC+1, Alexander Kurz wrote:

> On 31 May 2018, at 12:05, Michael Shulman <shu...@sandiego.edu> wrote:
>
> 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.

I am interested in this question of translating the untyped stuff we write on the page into type theory.

To give a concrete example of what I am thinking of as untyped, but nevertheless conceptual and structural mathematics, I would point at Tom Leinster’s elegant description of the solution to the problem of Buffon’s needle, see the first paragraphs of the section “What is category theory?” at https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html

I call this argument type free because I see no obvious or canonical way to make the types precise enough in order to implement the proof in, say, Agda. Even if this can be done, it is still important that mathematicians can discuss this argument first without having to make the types precise. So there will always be mathematics outside of type theory.

 I don't understand why you call this argument untyped. Do you feel that a formalization in set theory, which is untyped, would be easier than a formalization in type theory? How is untypedness helping with this argument?

Martin


--
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<mailto: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<mailto: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.





[-- Attachment #2: Type: text/html, Size: 9718 bytes --]