From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:ac8:604c:: with SMTP id k12-v6mr73375qtm.7.1525934137181;
        Wed, 09 May 2018 23:35:37 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:aed:2825:: with SMTP id r34-v6ls2698086qtd.14.gmail; Wed, 09
 May 2018 23:35:36 -0700 (PDT)
X-Received: by 2002:ac8:12c3:: with SMTP id b3-v6mr77200qtj.56.1525934136420;
        Wed, 09 May 2018 23:35:36 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1525934136; cv=none;
        d=google.com; s=arc-20160816;
        b=Zr0wCvvPvkny1wI/kV21szsVFg5+dHFTocUQL0RmagxqZs3L5fZG5A3VvoaOMvoi5n
         zq3F/pTm4Q5kEjhOpoEUjuPwZjSeKk8jtyZ47UQ2rn5M9M78KyTadFqvs2SwfAd2d7I5
         G8c9WDZmBui81rHjYe1gXNCxCR1CSJ9F269HMpoXKkoWwbH+Nb75a29h4zMG+XEFHegZ
         p/u8C/l7t3e1cYDkqXSKVrlpwJ9crDzz8BeTgd+QnJIbzvNPJgIlUgGFnEL03Ws7igO7
         r6l5sS9EXBjqYj60mVB9Sq7ZkR2QffQLFJHtxDZ28OBM0U92R9PrAVXvJF070Sg2tHL0
         exdQ==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816;
        h=to:subject:message-id:date:from:references:in-reply-to:mime-version
         :dkim-signature:arc-authentication-results;
        bh=Ws9LVAW07yABYoLyI66p31c3MFRdiXLv0hosWvqVLQE=;
        b=bzRH5+t0WJ1ed6QwnnfAQZSrowgVZTto0OhuqkRs8nxtTUp4bZt+uKoNP9++/wo/+W
         HZJxl8OGLICUCBgf65T6H+0N2cHRUsTU68lXB+nnglMP8GxaXNXyoArA5SiiG3IJKYtJ
         1tEMLRf7U58wTwzN6AP65Of1WE+t7feLk67NA1uvGqSul1M//THvqcHxgj4JrtbXAthJ
         QBnOHCZxN9iBRWlbjly5hm70WcNufmnVnh546Eu1Btz3bqe/kPjW0qLxS7TI2m7a18Sz
         WXvkeRnqhwFvW7j6HCh3RdISBba/2Vtn7jJTDmpFztfoRxAJxiKDfnYMwWTzTZEpCu1c
         rp0g==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=uqYtfzuc;
       spf=neutral (google.com: 2607:f8b0:4001:c06::230 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-io0-x230.google.com (mail-io0-x230.google.com. [2607:f8b0:4001:c06::230])
        by gmr-mx.google.com with ESMTPS id y6-v6si8514qtn.1.2018.05.09.23.35.36
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Wed, 09 May 2018 23:35:36 -0700 (PDT)
Received-SPF: neutral (google.com: 2607:f8b0:4001:c06::230 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4001:c06::230;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=uqYtfzuc;
       spf=neutral (google.com: 2607:f8b0:4001:c06::230 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com
Received: by mail-io0-x230.google.com with SMTP id t23-v6so1778957ioc.10
        for <HomotopyT...@googlegroups.com>; Wed, 09 May 2018 23:35:36 -0700 (PDT)
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;
        bh=Ws9LVAW07yABYoLyI66p31c3MFRdiXLv0hosWvqVLQE=;
        b=uqYtfzucQNgLge8rOpXwUbRy0iv5nB4CXulcRioxXxlSAwhkXhEbrMUw74pfUDOlvf
         CCrP2SeH6LDU4IP5fJ1JIzDGwhU82CrjtgSDdIHp9mMj++/2zuxUrcWk96ldaYCIbAgG
         9z5LH+/Dojcd8Wru374KPaCKeHUTwaFezG2FzS7ZBN8dRpR/M4Ty/IRzLeUznRg/+91i
         heb+RzvYCi/eV6NQrdjuTIDF42DBtVTmyg9+P6wED965XeyR75LgZWV8R7L/wEXdpjJy
         SxnVIbL+sn7apjCJNCXSb7rdLbLXKAgJqUXJPKQv1D2rF9vDVedPTvR9TI/e2q3Qzaz5
         3Wcg==
X-Gm-Message-State: ALKqPweiWIasYh8MxSgUL5Chw5b3Hi1jFhpMDChLv6j+CMxB2rmsVBtc
	GQ/krtxnab1jvgqiBnHSDqfk2VwpWTBJqU+NZvH+wg==
X-Received: by 2002:a6b:1c06:: with SMTP id c6-v6mr157227ioc.247.1525934135699;
 Wed, 09 May 2018 23:35:35 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.192.174.39 with HTTP; Wed, 9 May 2018 23:35:35 -0700 (PDT)
X-Originating-IP: [2001:1470:fff0:830:18c8:5214:a951:3f32]
In-Reply-To: <3b661da9-52d2-43b0-b346-902e610a3057@googlegroups.com>
References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com>
 <CAOoPQuSUu+j7jcjAg7fioYFkj78+8MRtDfwVHHrqHfry2gPEoQ@mail.gmail.com>
 <32baa760-53ed-4fa4-b69c-9537be5b63aa@googlegroups.com> <CAOoPQuTOTFMEL5a+chTXEv5Ct7YvZaK5m55Emrg-djxZ0MgHtA@mail.gmail.com>
 <385f5d47-0656-4a4d-b24c-c2abeab629e7@googlegroups.com> <CAOvivQzovmetiZJUF+z0scQtVr42oLE2ygwJtRNTC0eM=R0sTA@mail.gmail.com>
 <CAOvivQwE+o3nmbdw5i1y5dGM=x-ET28FFyKwqd2m-z5LfifUoA@mail.gmail.com> <3b661da9-52d2-43b0-b346-902e610a3057@googlegroups.com>
From: Andrej Bauer <andrej...@andrej.com>
Date: Thu, 10 May 2018 08:35:35 +0200
Message-ID: <CAB0nkh3vYApu3WmETVwePAdNbJOKEvGomqtVaDsgjYWt7BwLaw@mail.gmail.com>
Subject: Re: [HoTT] Bishop's work on type theory
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset="UTF-8"

Hi,

I have had these documents in my office for a while, but forgot about
them and never found the time to look at them. Such an opportunity
missed.

In any case, it looks like I have an earlier vesion, because some of
the manuscripts are written in hand in they do look like an incomplete
version of the ones that Martin published. If anyone wants to do
archeological mathematics, I could scan them in, althogh I hesitate to
make them publically available.

With kind regards,

Andrej