Re: [HoTT] A small observation on cumulativity and the failure of initiality

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

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

Just to clarify: by set theory we mean ZFC, not the set-level fragment of HoTT.

I am not sure what is in general the “native meaning” of type constructors. Ok, it is pretty clear for function types but not in general.

Choosing a clever encoding you could make products strictly monoidal, that is Ax(BxC) = (AxB)xC. Is this now the true equality or not?

Looking at inductive types you can have representations where F(mu F) = mu F or you choose that this is just an isomorphism. Either of them can be justified by set theoretic encodings which is no help in deciding which ones should hold.

Thorsten

From: <homotopyt...@googlegroups.com> on behalf of Andrew Polonsky <andrew....@gmail.com>
Date: Monday, 16 October 2017 at 11:42
To: Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality

Equalities in the set theoretic translation of Type Theory are accidents of implementation choices. Making them the guideline for the design of Type Theory seems to to put the cart in front of the horse.

No.

The fact that equalities corresponding to beta reduction, etc. are validated is not "an accident of implementation choices".

It is a consequences of the fact that standard type constructors (function space, products, ...) are interpreted by their native meaning in the meta-level.

For example, if the metatheory is again type theory, and interpretation is done by recursion over the universes of object types, reifying all type constructors by themselves (like in an inductive-recursive universe), then all conversions in the object language will again be valid in the metatheory, and coherence issues won't arise.

I suspect that (sufficiently split) categorical models could also be presented this way, but it might be less natural because equality of types would then have to refer to (actual) equality of objects.

Cheers,
Andrew
--
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 send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.


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