From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.200.54.138 with SMTP id a10mr20739925qtc.47.1520584246728;
        Fri, 09 Mar 2018 00:30:46 -0800 (PST)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.55.77.8 with SMTP id a8ls3640778qkb.3.gmail; Fri, 09 Mar 2018
 00:30:46 -0800 (PST)
X-Received: by 10.55.158.81 with SMTP id h78mr20198389qke.24.1520584246241;
        Fri, 09 Mar 2018 00:30:46 -0800 (PST)
Received: by 10.55.167.150 with SMTP id q144msqke;
        Thu, 8 Mar 2018 02:04:43 -0800 (PST)
X-Received: by 10.25.150.71 with SMTP id y68mr1824707lfd.42.1520503482663;
        Thu, 08 Mar 2018 02:04:42 -0800 (PST)
ARC-Seal: i=1; a=rsa-sha256; t=1520503482; cv=none;
        d=google.com; s=arc-20160816;
        b=gnEa190DGeazA5xzazZdTyDU9WXcVPbnekhWY1MSVBrTFs18cNpa7vUWJW9MwsL5VR
         agARRFPaYj1uTJbUhRzDNl0Yc726bUlTNL4mpRBtxgeh62UwE/DJr3lRcgY2D8DWfMk2
         7I5PBD7l7O6dDeseknH8p98pyEUlbimTFgx/y+BnzMDv6o2pYJgNWgMu5VQ354HnSCCO
         g9q8PAvFP9nzlLrvRtwV5uDAGM0AKDbJnTkaEVmFv3rBu3Pr5YQ8e3r16pNPxQzGTDDX
         kffgr3FZOfmkaLzDJ+Tnw6Ony3MXgz05z/LDAqYLuLxwulDsdQ82L6/ukw1Zbq1kHP/f
         CNCw==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816;
        h=content-transfer-encoding:content-language:in-reply-to:mime-version
         :user-agent:date:message-id:from:references:to:subject
         :arc-authentication-results;
        bh=zwUrkN3CEHdmiKvEeChMDRlnTvOkhBGlQCmQRWbmgCs=;
        b=m0gOZ2IM4hX+vC/pK3vU7BHDGJxJ5k1sNnEtvrGfukSWONi7ZWl7GVi4z8ilb5fC3/
         g4rERDcK1pHsLtElXRRncewY7gMcx+C9JJSeve1p+lkh/o5uUdlAsHxpsZYiARTaD1mt
         QAyx8u1ZIo5EajTfZwGlPaxir14sJcbX70gP1PBdJvVrAtjTrdFd/azV1gtaXjWYwk89
         HIsQzcsNyEbfJZ83gGkUBAFBk9RsOTX+losASj/EgF6vdSZf++it3/DshZILLuycT12f
         KY4GHQU/vpDQvSa97pvKl7IDyyYQ+YXOWr79ljJ0NjttJ6lPNUVyqbvSlndQQEr6DLw4
         +Cdw==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com;
       dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com
Return-Path: <escardo...@googlemail.com>
Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137])
        by gmr-mx.google.com with ESMTPS id s12si786068lje.3.2018.03.08.02.04.42
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Thu, 08 Mar 2018 02:04:42 -0800 (PST)
Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137;
Authentication-Results: gmr-mx.google.com;
       spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com;
       dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com
Received: from [147.188.128.54] (helo=mailer3)
	by sun60.bham.ac.uk with esmtp (Exim 4.89)
	(envelope-from <escardo...@googlemail.com>)
	id 1etsPi-0007m0-Mi; Thu, 08 Mar 2018 10:04:42 +0000
Received: from dynamic200-210.cs.bham.ac.uk ([147.188.200.210])
	by bham.ac.uk (envelope-from
	<escardo...@googlemail.com>)
	with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128)
	(Exim 4.84)
	id 1etsPi-0001u3-Cu 
	using interface auth-smtp.bham.ac.uk; Thu, 08 Mar 2018 10:04:42 +0000
Subject: Re: [HoTT] Re: Univalence from scratch
To: Andrej Bauer <andrej...@andrej.com>,
 Homotopy Type Theory <HomotopyT...@googlegroups.com>
References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com>
 <f758a1c3-9dc8-457f-b039-ab5f124e642d@googlegroups.com>
 <CAB0nkh2fjMZEOz7ix68qEMTXtJpxO7hd0u31JPdtyZJq=3eBrA@mail.gmail.com>
From: Martin Escardo <escardo...@googlemail.com>
Message-ID: <0b85afaf-3c5d-9e3d-6691-d11192516c0c@googlemail.com>
Date: Thu, 8 Mar 2018 10:04:33 +0000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101
 Thunderbird/52.6.0
MIME-Version: 1.0
In-Reply-To: <CAB0nkh2fjMZEOz7ix68qEMTXtJpxO7hd0u31JPdtyZJq=3eBrA@mail.gmail.com>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
X-BHAM-SendViaRouter: yes
X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom)

On 08/03/18 09:25, Andrej Bauer wrote:
> Martin-Löf'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
> 

Thanks Matt and Andrej.

Best,
Martin