From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.129.58.9 with SMTP id h9mr9727059ywa.221.1520501124082;
        Thu, 08 Mar 2018 01:25:24 -0800 (PST)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:a25:ad1b:: with SMTP id y27-v6ls322278ybi.9.gmail; Thu, 08
 Mar 2018 01:25:23 -0800 (PST)
X-Received: by 2002:a25:850e:: with SMTP id w14-v6mr12129310ybk.9.1520501123380;
        Thu, 08 Mar 2018 01:25:23 -0800 (PST)
ARC-Seal: i=1; a=rsa-sha256; t=1520501123; cv=none;
        d=google.com; s=arc-20160816;
        b=zsXxP6ZFCPT2rr5zqinSOTK9W4cfFG6ml4OSfn+4+GR9pt73yyJXyTL0eem8PY6i9M
         nxtjFuEIGwfTSiQSZSlqWPwlc+jBxFmtLGLNqks2ezrBbU+IJmcURuWuElVpQXMXHwL/
         Dk0KM7iZ5M805LBTNJq3twFWlTiHLtc03OhUeK5wBkXAmjAG41mlqv5vPq58V1tVrADj
         Ra7rUl/pfAEllY1jvDMx+7LVoObam+QQKmGmutmkJZc+D5Zlm12SCOcJDHMoDeXbiRaD
         5uSlbXWvQS3Ugk7UxIrsHoMmd8cBmFFwjr9tXDzjF+Qbx+fQFVWW6Jm6688JTkrIFTCU
         NgAQ==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816;
        h=content-transfer-encoding:to:subject:message-id:date:from
         :references:in-reply-to:mime-version:dkim-signature
         :arc-authentication-results;
        bh=IIw4dm+XvJNUW3TYdYTUusZXWofDFu+HMnOlOOoRhA4=;
        b=OCxqir/5vQLCEYqvEvz1hsfHeLP3Mmi0TGhz3Jrifxp0HJW0BD27uLgIyYgfzPPuF2
         PXm7XlIRbatqmDyJtKPIVmqzrj84PRyznh3mvM35gywZCWxjdV4ptBVyUYm1JOm5TbUA
         6EQ6aH6h7YCg+rWtrN5mM9PuR0iKfyEqfW7gRhfBhXn/bIs1c/fseCkdm0dv58YGCwm5
         /wIu9dfF2uYQFsHC/WVN/DXrDM7hoo+YK5Lgg/wIMoGajGzmSwgyqEQDRt12qwTxOWJF
         tUUNXfjp8VmO6VBK8zIZhulQ/N4U4srTow5kyN7Fmwgi1sR+joQ+TN4NkRjpW8fbhSQt
         HVjw==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=SbHWSW7B;
       spf=neutral (google.com: 2607:f8b0:4001:c0b::236 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com
Return-Path: <andrej...@andrej.com>
Received: from mail-it0-x236.google.com (mail-it0-x236.google.com. [2607:f8b0:4001:c0b::236])
        by gmr-mx.google.com with ESMTPS id s5-v6si1119793ybk.4.2018.03.08.01.25.23
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Thu, 08 Mar 2018 01:25:23 -0800 (PST)
Received-SPF: neutral (google.com: 2607:f8b0:4001:c0b::236 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4001:c0b::236;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=SbHWSW7B;
       spf=neutral (google.com: 2607:f8b0:4001:c0b::236 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com
Received: by mail-it0-x236.google.com with SMTP id k79so7117723ita.2
        for <HomotopyT...@googlegroups.com>; Thu, 08 Mar 2018 01:25:23 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=andrej-com.20150623.gappssmtp.com; s=20150623;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :content-transfer-encoding;
        bh=IIw4dm+XvJNUW3TYdYTUusZXWofDFu+HMnOlOOoRhA4=;
        b=SbHWSW7BQW7SbnXjFFCB25Gt1VcfCrTZEzDDSiEbY5edihFnNCM30pO9VYzM7OTpRW
         zj9sD61K9c+8tqZBdGeBVDaplZdoI06fuyCdsN2fWTZ0xFeVGeDW+9291E/j1BP8oFGf
         ZZcs99W6SSXj5gCaPNr//MlryEL/5IZUFjmikddT2+AqMukwRBaHsT/mTFal413pAFqa
         UFPk4dzKTwJSHcsxRl6TYjmDvUOr1TgkkuqLUmnAkavilSR/YkHW467CWZRKZ7GoznoJ
         mHaWmwvrska8rjX6ZVKzlsKSVrHNFiodVIJHD3eV2itjXMQONQ1Z+lKVRQHJvOLSL54M
         RnQA==
X-Gm-Message-State: AElRT7GScvOntt6ORoWVIu2Cy3lKUF+zT58wtLiyftsF0uT9VXFFNMNb
	UGA0LutZM8lFwfqvwDsC1jEBTo6iS/IdrZT0RvkK6Q==
X-Received: by 10.36.94.65 with SMTP id h62mr27989642itb.144.1520501122673;
 Thu, 08 Mar 2018 01:25:22 -0800 (PST)
MIME-Version: 1.0
Received: by 10.192.171.138 with HTTP; Thu, 8 Mar 2018 01:25:22 -0800 (PST)
X-Originating-IP: [2001:1470:fff0:830:bc42:b944:e3d3:1767]
In-Reply-To: <f758a1c3-9dc8-457f-b039-ab5f124e642d@googlegroups.com>
References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> <f758a1c3-9dc8-457f-b039-ab5f124e642d@googlegroups.com>
From: Andrej Bauer <andrej...@andrej.com>
Date: Thu, 8 Mar 2018 10:25:22 +0100
Message-ID: <CAB0nkh2fjMZEOz7ix68qEMTXtJpxO7hd0u31JPdtyZJq=3eBrA@mail.gmail.com>
Subject: Re: [HoTT] Re: Univalence from scratch
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Martin-L=C3=B6f's paper "25 years of constructive type theory" might be an
appropriate reference. It's an updated version of earlier work, and
somewhere near the beginning he says explicitly that terms are always
constructed with their types.

With kind regards,

Andrej