From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.17.12 with SMTP id c12mr375163qtj.5.1513002752953; Mon, 11 Dec 2017 06:32:32 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.237.35.75 with SMTP id i11ls3914814qtc.7.gmail; Mon, 11 Dec 2017 06:32:32 -0800 (PST) X-Received: by 10.200.55.29 with SMTP id o29mr371894qtb.38.1513002751998; Mon, 11 Dec 2017 06:32:31 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513002751; cv=none; d=google.com; s=arc-20160816; b=Xk8voBvut7b/E+SzkG9Um8ZGhmPgzxV5fugvImWTOwNUJ+IrWICPfWhM/j1jpIrR// efsxwvBNjQIn1/SxcSMtk7JA/2nmLJiQqQX+uUKGP1c/rjRSBTkKxgsPTCGVvEaw35nn fBn+bhd+TQDBlCU9rY0DS55znHYliZ2n6+GwvIzinmYvuRra7VrN3RU22NcAyB4f+vY4 4o9fYUzQiY7piX+1uUNbWphF1AW4fiRN186z2xtMZ9Gh4ps8VeY4Ej4Tbvs5WuEAlu5j +w8RBC7IEWD0ntNxY7pZZWKRukga7q2QdsV+chM/lySwXTHOcFBl1SzkD86c45S9deld sJuw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :dkim-signature:arc-authentication-results; bh=fd6jJcpe6BYBhP838HIPpeOiRL+RS8d4H6Aqhs99QPA=; b=OK0kfXfpD0XmtGOKlFN7f0hxW75C9riZ+70A8+fYCOFolKhvXWj6CGZxIwb9f3Ul6w zE33N2enUV1Wlh+jJHzlBe6ybTlWJS8NrZFGfVaF09GcRVXrtsgHyZHjhwGgq625TodP W2E68lWLRudz3vmkQVOaNg8IRbocshWsE1BfLfgEGA0GNafQ/6pH09J9V195LBHjr1z6 RC7Gcku75DypACss9t+9koZwrr3sQexvW3ae6jk44OniYnOfPncLlgrbDUKVBJEuPvak wEsZEeYJhO9UKnaghQg8aCTs8sx+UylDUjYy8BrUSJwf/RBW4SwSBB//N9LR8LuNth/r tj+g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=oQzu4/73; spf=pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:4002:c09::235 as permitted sender) smtp.mailfrom=sojakova...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yb0-x235.google.com (mail-yb0-x235.google.com. [2607:f8b0:4002:c09::235]) by gmr-mx.google.com with ESMTPS id b139si764546qkc.2.2017.12.11.06.32.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Dec 2017 06:32:31 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:4002:c09::235 as permitted sender) client-ip=2607:f8b0:4002:c09::235; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=oQzu4/73; spf=pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:4002:c09::235 as permitted sender) smtp.mailfrom=sojakova...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-yb0-x235.google.com with SMTP id h28so861874ybj.5 for ; Mon, 11 Dec 2017 06:32:31 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding:content-language; bh=fd6jJcpe6BYBhP838HIPpeOiRL+RS8d4H6Aqhs99QPA=; b=oQzu4/73ieklFHYZ4BeYUQdCMxwm06WALvgT6j4Ls7fKyjVTvrDKlAjvTtqkwWzy/g i6HfOrOpTL6KyJPpqkRg0NNEwW16bPYpGC8haP227qKySB9DYPIy5slPMqajxhjzRz5o /M95761swDaoCm8rY2r/ZRtKsVb9UNloHTbjViaJmDnb7Rq9QHeB+kC5owhxrZCm0lnQ 4SiwWzn1Titrbcd0ZajAS+YUXUjOg/A54DpoTCePWAhJ9qIcyuOEpsWOw5Npu1Zoez5k fpRgWbnstSiBQUiuXbUPG9WrYOXPXJLcyxcju8W2XPn/Ho+CjvXPaXDvJAhAK+Gm5cpv eMDA== X-Gm-Message-State: AKGB3mIOBsEt+kJ/R9S2bDjwYQXTjzm1lGDbevv5BOMn55LcRkzRRWBL lTv2NmDtHR79GdWvrkUi+0TsBrip X-Received: by 10.129.33.87 with SMTP id h84mr451992ywh.30.1513002751586; Mon, 11 Dec 2017 06:32:31 -0800 (PST) Return-Path: Received: from [10.111.19.233] (h50.129.138.40.static.ip.windstream.net. [40.138.129.50]) by smtp.gmail.com with ESMTPSA id g37sm6366138ywk.95.2017.12.11.06.32.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Dec 2017 06:32:31 -0800 (PST) Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? To: HomotopyTypeTheory@googlegroups.com References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <1512992534.265543.1200966552.20A0FEC1@webmail.messagingengine.com> <1512996187.281015.1201017552.7F33C02E@webmail.messagingengine.com> <20171211142816.GA24950@mathematik.tu-darmstadt.de> From: Kristina Sojakova Message-ID: Date: Mon, 11 Dec 2017 09:32:35 -0500 User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.5.0 MIME-Version: 1.0 In-Reply-To: <20171211142816.GA24950@mathematik.tu-darmstadt.de> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Content-Language: en-US Hi Thomas, Thank you for the answer! You wrote: "Id takes values in Prop and is isomorphic to Leibniz equality." That would be what coq calls "eq". But what is the interpretation of the proof-relevant identity type "Id", which takes values in Type? For my theory I want both. Kristina > > See work from the 80s by Martin Hyland, myself and a few others. > > Thomas >