From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.80.201.7 with SMTP id o7mr1068810edh.3.1513108362630; Tue, 12 Dec 2017 11:52:42 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.80.159.161 with SMTP id c30ls177081edf.1.gmail; Tue, 12 Dec 2017 11:52:41 -0800 (PST) X-Received: by 10.80.244.178 with SMTP id s47mr1069144edm.6.1513108361496; Tue, 12 Dec 2017 11:52:41 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513108361; cv=none; d=google.com; s=arc-20160816; b=aioZg+b5qm4rRaKmjHzNvYJf2kIKBUrYedHiMoMK/ynaIZvvMgYZu9gY5K69hVHLFS 5DYMbH9u5+iY5el9me6RCMHmaWtobOXLRgyPQhEr35sfk/p6vt2M3X4Aj5Z1ruTcivmZ 7uEPY1sVozirQQ2fl19DZPKIhaOZvPCV9kTYOC1X+MgHlmyVSZaWjkhRkrTCM+hWKZas n3SSIPeuGQk4S8RJbcMdA8UO9cDIdyopQuxfidsKzR0qQzZzv4liqXPskzJ2IDZ7OH2I 1lMrg/dplpzk86u3N5Xe0MPYA1Z91jspHzHZK7TmnUhX1baGA6YI2HjDsh6EpfprEViH LQGA== 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:cc:to:subject :arc-authentication-results; bh=GxamjIWqGzteso7QwJFEiXj300F6s6NLoMdvmDioXUU=; b=kqCN+FiRcW6lDswe8uqnC77vX5I2x+AWRa0Q17YDaaTUgi41KktksRO1DHcAeuWEnK +cJD5He8ACzsV42ZHE0vOl8XNBJQVNVc/wkKgE9jOhV5JrMveQ50Qxe1Kil89euDiX1h 9cFP0JTl6XlKouv+Int1iaALtScdf/cr9PAfzLMBdveO3/nTfxssbxr4iWJLYMX8p4kO /I8JC19XY60kw4jqAZ6KpxUZU434BEw77OrC89tPv1TTgCBngRpJXiJin2wQULr0+81C 3YiMYyodC0jq7kenxjhW4uC34K/ZjeSiGHMcNbAgdxZxosZxAOqEDof4litECSR7WVot bDvA== 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.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id a23si33368edd.1.2017.12.12.11.52.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 12 Dec 2017 11:52:41 -0800 (PST) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 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 sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1eOqbZ-0003Ao-Md; Tue, 12 Dec 2017 19:52:41 +0000 Received: from 108.115.39.217.dyn.plus.net ([217.39.115.108] helo=[192.168.1.103]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1eOqbY-0002Ss-Fy using interface auth-smtp.bham.ac.uk; Tue, 12 Dec 2017 19:52:40 +0000 Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? To: Thomas Streicher , Jon Sterling Cc: HomotopyT...@googlegroups.com References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk> <20171212120233.GA32661@mathematik.tu-darmstadt.de> <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> <1513084622.1768586.1202387232.03F5CC27@webmail.messagingengine.com> <20171212192921.GA11564@mathematik.tu-darmstadt.de> From: Martin Escardo Message-ID: <6b10fcd2-a4bf-7269-5e08-afa1b0b177f9@googlemail.com> Date: Tue, 12 Dec 2017 19:52:42 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.5.0 MIME-Version: 1.0 In-Reply-To: <20171212192921.GA11564@mathematik.tu-darmstadt.de> Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-GB Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) On 12/12/17 19:29, Thomas Streicher wrote: > Univalence is something which will not hold in most toposes and if it > does one has to interpret Id in a way that it is not a proposition. How do you even formulate univalence for an arbitrary topos? Martin