From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Mon, 16 Oct 2017 03:42:05 -0700 (PDT)
From: Andrew Polonsky <andrew....@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <855393ab-3b24-4de4-81aa-a7b9e3c102dc@googlegroups.com>
In-Reply-To: <F9E4D5E5-D0AB-48C7-AE2D-22F1CE88D9C5@exmail.nottingham.ac.uk>
References: <F9E4D5E5-D0AB-48C7-AE2D-22F1CE88D9C5@exmail.nottingham.ac.uk>
Subject: Re: [HoTT] A small observation on cumulativity and the failure of
 initiality
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_17803_1862107618.1508150525097"

------=_Part_17803_1862107618.1508150525097
Content-Type: multipart/alternative; 
	boundary="----=_Part_17804_2021257749.1508150525097"

------=_Part_17804_2021257749.1508150525097
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit


>
> 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

------=_Part_17804_2021257749.1508150525097
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><blockquote class=3D"gmail_quote" style=3D"margin: 0;margi=
n-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div bgcolor=
=3D"white" lang=3D"EN-GB" link=3D"blue" vlink=3D"purple"><div><div><p class=
=3D"MsoNormal">Equalities in the set theoretic translation of Type Theory a=
re accidents of implementation choices. Making them the guideline for the d=
esign of Type
 Theory seems to to put the cart in front of the horse.<br></p></div></div>=
</div></blockquote><div><br></div><div>No.</div><div><br></div><div>The fac=
t that equalities corresponding to beta reduction, etc. are validated is no=
t &quot;an accident of implementation choices&quot;.</div><div><br></div><d=
iv>It is a consequences of the fact that standard type constructors (functi=
on space, products, ...) are interpreted by their native meaning in the met=
a-level.</div><div><br></div><div>For example, if the metatheory is again t=
ype theory, and interpretation is done by recursion over the universes of o=
bject types, reifying all type constructors by themselves (like in an induc=
tive-recursive universe), then all conversions in the object language will =
again be valid in the metatheory, and coherence issues won&#39;t arise.</di=
v><div><br></div><div>I suspect that (sufficiently split) categorical model=
s could also be presented this way, but it might be less natural because eq=
uality of types would then have to refer to (actual) equality of objects.</=
div><div><br></div><div>Cheers,</div><div>Andrew</div></div>
------=_Part_17804_2021257749.1508150525097--

------=_Part_17803_1862107618.1508150525097--