From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.144.5 with SMTP id s5mr69926wmd.18.1500487457957; Wed, 19 Jul 2017 11:04:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.30.69 with SMTP id e66ls1195838wme.27.gmail; Wed, 19 Jul 2017 11:04:16 -0700 (PDT) X-Received: by 10.28.165.88 with SMTP id o85mr72583wme.32.1500487456866; Wed, 19 Jul 2017 11:04:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500487456; cv=none; d=google.com; s=arc-20160816; b=m9vNJU897yxNkWuOd2oxh6aQKtk78Z/pdCmxLjLhbbNOfSJ9w/DALHdlxHVWX+ntOS 9mJPTOJZ0hAXIK1MQOycgxdz5HXk08iB4brCWaY3W6pN+/c3xCVcfxpauMGQ+bGh3Rtl x2J3bUCQMsxFhioTGrLBx13AK9CYGoGKJjlfo2BwwomFsXwSqNBvpWe0F4dtsKEmI1lu 55xxUFE4WPyxGX2XmW+EZL6wgwZvi/SsbxwC9rYmqX/c5bRBKarVDIVLV6HXlcZYMyOO Q8JEHg+Orb3uQXQPVUlNFFS/8eqYKAnS1d3L9FfH6eKs93fORsY9RWNESbgmjZB6uQkH 7T4Q== 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=ApqGYT2dAOb1kQtKxYdsypSeTiaTyxKElvRVkxKodi0=; b=Bjij9SqTVpnPKOHnwqDBqtCrCE8jYbTmi1LydGAda0MR5v2hgDztKvQdJUcu7acJ5N IdupyuvxvUWBEvcyIOzBPtaF+8hgmq5w6BYLDchjcZ8z0+fKTVwi0a2Xz49EgwrwGOPl yrpL935aWEJ44W+Hpg4Bb+vRp20DJIcJGrOmAHVF2969nkzP3qdUBHUv899344Z90KKs e/WpuMJFgzgW13hMgQd0Zytf5Sqppjq4NLUmn2xBEpO3yA2myEzOinv5UBJcX+bD/Jpo XTYvr7dji+APaEZsRsWwrz8vynT7srHmIlaUsMxcxW28ZhfSlv3LEJhCsCyigTuFgY2w bfyA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.b=vhSNvWGS; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::236 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wm0-x236.google.com (mail-wm0-x236.google.com. [2a00:1450:400c:c09::236]) by gmr-mx.google.com with ESMTPS id m138si107529wma.7.2017.07.19.11.04.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 19 Jul 2017 11:04:16 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::236 as permitted sender) client-ip=2a00:1450:400c:c09::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.b=vhSNvWGS; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::236 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x236.google.com with SMTP id w126so5678698wme.0 for ; Wed, 19 Jul 2017 11:04:16 -0700 (PDT) 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=ApqGYT2dAOb1kQtKxYdsypSeTiaTyxKElvRVkxKodi0=; b=vhSNvWGSBbwXsDJaoPBAbSmMNq6E2Z67ehhCXqp2+87F/4XDrjlAspsKMxMfDfd4gS Ta8br14lAqOTNhVFxPaWsUB7bDvzmSelDowOVoR6giCU0x0IhGRVzjL047q7dzVLebrQ a6moHUVjXo9YCPJz0zM1q/TTnqrlh9e8+D7IGPSZGLk/y4Jostg+OJ4RRfpUGRko50PP wa9kikS0SpMaxY6b7HXZY8Fio/cOndtY64VegcOPMivTRKEL9Two0ATmoug4EKvSTpKe fVXIhmYJ59SF3Wp3AzMgg754amUZvPuaabEnN1XTv5wfvnJPc1brLkAc24Gi6snfDD/a lGtg== X-Gm-Message-State: AIVw112UOXYv7HJ9VLOB35XsSsK6+2wfvBHgY2+FKWfNsXEJ/QLGzg/r OY7PBDyEsggkcF45OUE= X-Received: by 10.28.111.218 with SMTP id c87mr559294wmi.36.1500487456141; Wed, 19 Jul 2017 11:04:16 -0700 (PDT) Return-Path: Received: from [192.168.0.3] (cpc86229-nott20-2-0-cust356.12-2.cable.virginm.net. [82.7.65.101]) by smtp.gmail.com with ESMTPSA id 125sm476810wmp.37.2017.07.19.11.04.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 19 Jul 2017 11:04:14 -0700 (PDT) Subject: Re: [HoTT] Weaker forms of univalence To: HomotopyTypeTheory@googlegroups.com References: From: Nicolai Kraus Message-ID: Date: Wed, 19 Jul 2017 19:04:13 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Content-Language: en-US On 19/07/17 18:19, Michael Shulman wrote: > I am not sure about (1). It might be an open question even in the > case when A and B are propositions. If we restrict ourselves to the case that A and B are propositions, then (1) (A ≃ B) -> (A = B) is as strong as (2) / (3), since (1) then says that equality is implied by a reflexive propositional relation and thus a proposition. Of course this needs funext. (Afaik (1) is often called "propositional extensionality", but we could also just call it "univalence for propositions.) We have once discussed on this list whether (1) is consistent with UIP (i.e. it would be different from (2)), but we did not find an answer. Nicolai