From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.0.208 with SMTP id e77mr592808lji.10.1464963135007; Fri, 03 Jun 2016 07:12:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.21.102 with SMTP id l99ls61947lfi.72.gmail; Fri, 03 Jun 2016 07:12:13 -0700 (PDT) X-Received: by 10.46.5.1 with SMTP id 1mr593229ljf.1.1464963133772; Fri, 03 Jun 2016 07:12:13 -0700 (PDT) Return-Path: Received: from mail-lf0-x22e.google.com (mail-lf0-x22e.google.com. [2a00:1450:4010:c07::22e]) by gmr-mx.google.com with ESMTPS id ur4si187164lbc.0.2016.06.03.07.12.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 03 Jun 2016 07:12:13 -0700 (PDT) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::22e as permitted sender) client-ip=2a00:1450:4010:c07::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::22e as permitted sender) smtp.mailfrom=andrew....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x22e.google.com with SMTP id k98so55290799lfi.1 for ; Fri, 03 Jun 2016 07:12:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=1Eb2Tp+N1rTorbOvin6qKiTEksRJkeA5OTVyENDTrNA=; b=Qd9SHl328rHA67Kej8aR7qIUot7CWvLOCTqSMkUsSLo51HMQRtck9AJiE6xg2vS8HY jcd2f9tr3CZSuVoOL8mztMaMzioW0ofV1pmgvE5frdvRd6SK0eVqkTBvB0xvw+Vos/dW D7N87jp8WOtYg6rOuTzqXR3RYa+dCr5CDaRx733An7Zxd9Gw18FcKOlrRp+mrLPhvHG5 CbocO97Grv/0VU1Oa9GlBDOPGsgxAacmPc7dUnlxgNybvGXo07qifPR6Cm4xrwTX1Mh8 vkWrCh37lzNHg+9DfPyL6jOc9h4TOhXSNi9fdhFtfDFj2GO6HC+WlGVVr3BqklrS9/fN MqRg== X-Gm-Message-State: ALyK8tKPAH6tnNeqk5rCbHJBhBf5QzJzUAjzTEEaPYmeldkwx5nhQ1GRLCIbm261ZPJw/wER31LDEb3qS4aEkQ== X-Received: by 10.25.152.211 with SMTP id a202mr928952lfe.33.1464963133597; Fri, 03 Jun 2016 07:12:13 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.16.40 with HTTP; Fri, 3 Jun 2016 07:12:12 -0700 (PDT) In-Reply-To: References: <5750A527.4060705@cs.bham.ac.uk> From: Andrew Polonsky Date: Fri, 3 Jun 2016 16:12:12 +0200 Message-ID: Subject: Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory? To: Vladimir Voevodsky Cc: Martin Escardo , Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a1140135c2febf20534604fcf --001a1140135c2febf20534604fcf Content-Type: text/plain; charset=UTF-8 Dear Vladimir, We are also isolated from many and many mathematicians who are trying to > find a way to express ideas that in my opinion are most naturally expressed > in the UF in various theories formulated inside the set theory. > In this paragraph, are you referring to what Martin called "synthetic homotopy theory/infinity-toposes" branch of the HoTT community, or to a disparate body of mathematical research with different objectives? Greetings, Andrew --001a1140135c2febf20534604fcf Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Dear Vladimir,

We are also isolated from many and many mathematicians who = are trying to find a way to express ideas that in my opinion are most natur= ally expressed in the UF in various theories formulated inside the set theo= ry.

In this paragraph, are you = referring to what Martin called "synthetic homotopy theory/infinity-to= poses" branch of the HoTT community, or to a disparate body of mathema= tical research with different objectives?

Greeting= s,
Andrew
--001a1140135c2febf20534604fcf--