From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.194.153.199 with SMTP id vi7mr1074819wjb.1.1465034180935;
        Sat, 04 Jun 2016 02:56:20 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.142.85 with SMTP id q82ls67529wmd.48.gmail; Sat, 04 Jun
 2016 02:56:20 -0700 (PDT)
X-Received: by 10.28.176.68 with SMTP id z65mr428658wme.7.1465034180141;
        Sat, 04 Jun 2016 02:56:20 -0700 (PDT)
Return-Path: <mphm...@gmail.com>
Received: from mail-wm0-x232.google.com (mail-wm0-x232.google.com. [2a00:1450:400c:c09::232])
        by gmr-mx.google.com with ESMTPS id s140si470230wme.1.2016.06.04.02.56.20
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Sat, 04 Jun 2016 02:56:20 -0700 (PDT)
Received-SPF: pass (google.com: domain of mphm...@gmail.com designates 2a00:1450:400c:c09::232 as permitted sender) client-ip=2a00:1450:400c:c09::232;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@gmail.com;
       spf=pass (google.com: domain of mphm...@gmail.com designates 2a00:1450:400c:c09::232 as permitted sender) smtp.mailfrom=mphm...@gmail.com
Received: by mail-wm0-x232.google.com with SMTP id n184so27201737wmn.1
        for <HomotopyT...@googlegroups.com>; Sat, 04 Jun 2016 02:56:20 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=mime-version:sender:in-reply-to:references:from:date:message-id
         :subject:to:cc;
        bh=AuScCUSVpMLcAvnYkqmu8RUNlP0tD+GOvzLC+cllwlU=;
        b=L94VkBvq+Z0+//hGMzdj9DaAzh+FMewsqI7SKGKzkkUfV2NplJXEvWY9T3SecvK5Zh
         oVIjrQjvFMFgOzXTVr8Y7+uFmUXtHWvu72ykiED/Xay5Rp3MI9oo6uOGiyMNtB8mWNaH
         W1K6rI9oO8lnSBrbtLzAg3ryb3Ba4AnEL9HRdNXTCA7sqKgnlCL1UogX/4NzM7Yi30ej
         Vv2AoQ+IYLRwsXY5DH2ynuwBcWnPWyarudnK9En/BNpI6dVQBJtS3HLR2Kn30zaN0dPt
         yTQzg6mOqRCKwnFvKD1btTJQATedcFayl0FU57mhcOf1/dSRAM2qUudS6aeRFFPRnHA7
         onSA==
X-Gm-Message-State: ALyK8tKsfLOETlWI4alRLCuWUq3b+83FEkGHQluO3Y/MAZ0NZ1LErKc0OCC1lw8Z2DlfaAW4mGu4o9uI6BvepQ==
X-Received: by 10.194.5.7 with SMTP id o7mr7106229wjo.145.1465034179961; Sat,
 04 Jun 2016 02:56:19 -0700 (PDT)
MIME-Version: 1.0
Sender: mphm...@gmail.com
Received: by 10.194.112.33 with HTTP; Sat, 4 Jun 2016 02:56:00 -0700 (PDT)
In-Reply-To: <B073EA60-F3F4-47F4-85FF-7750B5753BB9@ias.edu>
References: <5750A527.4060705@cs.bham.ac.uk> <deb61dfc-f1f3-48fc-b208-b94caca612d4@googlegroups.com>
 <C03FD0E7-5F21-45FA-B0A9-11DDDDE385A3@ias.edu> <CABcT7WAEpiV3ShjJ8Zeokw+d8Zngzf9ZMiWP_CQAycfLR8LO8g@mail.gmail.com>
 <A9CC94F9-0983-4087-9DF6-DC18A8891FB7@ias.edu> <CAHPPr6zxGA=i2HBuhyCjs1ZmetT2funLRHpsCh346Mtnk0XTyw@mail.gmail.com>
 <B073EA60-F3F4-47F4-85FF-7750B5753BB9@ias.edu>
From: =?UTF-8?Q?andr=C3=A9_hirschowitz?= <a...@unice.fr>
Date: Sat, 4 Jun 2016 11:56:00 +0200
Message-ID: <CAHPPr6xp6bmXKopdz45nsJUybB62Dx9RwaFU0HQTthT-X_U8RQ@mail.gmail.com>
Subject: Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?
To: Vladimir Voevodsky <vlad...@ias.edu>
Cc: Andrew Polonsky <andrew....@gmail.com>, Martin Escardo <m.es...@cs.bham.ac.uk>, 
	Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: multipart/alternative; boundary=047d7b5d8d45e16b6c053470d914

--047d7b5d8d45e16b6c053470d914
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

Thanks!

2016-06-04 10:38 GMT+02:00 Vladimir Voevodsky <vlad...@ias.edu>:

> It is very easy to formalize, for example in UniMath, the concept of a
> quasi-category.
>

I now understand that you even accept such a "flattened" notion of
(oo, 1)-category. Great! So, since at least one (simple, standard)
definition is already there, what exactly is missing in your view for them
"all start to turn their heads in [y]our direction"?

andr=C3=A9

--047d7b5d8d45e16b6c053470d914
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div class=3D"gmail_extra">Thanks!<br><br></div><div class=
=3D"gmail_extra"><div class=3D"gmail_quote">2016-06-04 10:38 GMT+02:00 Vlad=
imir Voevodsky <span dir=3D"ltr">&lt;<a href=3D"mailto:vlad...@ias.edu" tar=
get=3D"_blank">vlad...@ias.edu</a>&gt;</span>:<br><blockquote class=3D"gmai=
l_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,20=
4,204);padding-left:1ex"><div>It is very easy to formalize, for example in =
UniMath, the concept of a quasi-category.=C2=A0</div></blockquote><div><br>=
</div><div>I now understand that you even accept such a &quot;flattened&quo=
t; notion of <br>(oo, 1)-category. Great! So, since at least one (simple, s=
tandard) definition is already there, what exactly is missing in your view =
for them &quot;all start to turn their heads in [y]our direction&quot;?<br>=
<br></div><div>andr=C3=A9<br></div><div><div><br></div> </div></div><br><br=
></div></div>

--047d7b5d8d45e16b6c053470d914--