From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.101.78.199 with SMTP id w7mr11374258pgq.103.1512966176619; Sun, 10 Dec 2017 20:22:56 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.99.124.83 with SMTP id l19ls1779448pgn.26.gmail; Sun, 10 Dec 2017 20:22:55 -0800 (PST) X-Received: by 10.98.160.77 with SMTP id r74mr2043994pfe.37.1512966175439; Sun, 10 Dec 2017 20:22:55 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1512966175; cv=none; d=google.com; s=arc-20160816; b=UHFS0iygWh2RAMm7ZOcAovcRJNbHVWrKQMA3cK3LKmD+SvLLznvL2z2yEfBuncMy7K 2iPg6x0iJqnYrLQK4qM2+rqE4smcmUbJrR2jgcVFB2tAErS/+Yv+cVkTOVoO8kFJ8vyl u3LXvflX19a68Zxeb8QLI+XyJCJMV80Cls4BwiNKCty+X1t8NVZ+Q6Sbl2w++Aru3Jn8 glZsNEasxZXVdrnjMa78FoZ00YQhjri+Fbr6HhQ+F7Lx7O/2ociyOaUT7vzo5NKWtUYu NH+V3DhTHd9qFhbODRD2nUa2uAlklXQeZBqdM/2byKN/LeCEkQXlvAWnR/036HJLk41D G2Zg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:mime-version:user-agent :date:message-id:subject:from:to:dkim-signature :arc-authentication-results; bh=9nj7hdN3Y3jnd0FNPkSmvKFOvGzLN/HFEhCUij5xlOQ=; b=VCJlsvGqjPW7QbFC0nxPZXIP3e3aWlFwQ6DMIR9VPGTFBCeoOB5KRwnWZgEtRnDqM+ IrzH25hlGIReIh3oxrboKgpKEJ9FaA58xxrfVpG9z/Lhh9vsFFYhV+c+8IQuY5lFsJX9 jAoyutiCX3AsmHC1pjrJMVu5UEkxpeIDNyTvl+HZayp+7cQVljiSzx2SafX7TARFY1e/ mIxVFYjT3pOnGoHs2TqjKA8rxTo8xd05cIc4cJImYEjzBk4kYa5d+n/GfgxNgL1lgogl EQWNVDAB+h7B4E3Gs3AYAmCPL/SvbbcWbkEyBTHrAsrK+k7uNoRciZc2MygrE+jkJ3M/ BpKw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=aVaDyuYu; spf=pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:400d:c0d::233 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-qt0-x233.google.com (mail-qt0-x233.google.com. [2607:f8b0:400d:c0d::233]) by gmr-mx.google.com with ESMTPS id m9si608988plt.2.2017.12.10.20.22.55 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 10 Dec 2017 20:22:55 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:400d:c0d::233 as permitted sender) client-ip=2607:f8b0:400d:c0d::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=aVaDyuYu; spf=pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:400d:c0d::233 as permitted sender) smtp.mailfrom=sojakova...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qt0-x233.google.com with SMTP id k19so35389957qtj.6 for ; Sun, 10 Dec 2017 20:22:55 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=to:from:subject:message-id:date:user-agent:mime-version :content-transfer-encoding:content-language; bh=9nj7hdN3Y3jnd0FNPkSmvKFOvGzLN/HFEhCUij5xlOQ=; b=aVaDyuYuVOMkqt0Wjfavn+70Iz+pCDWnEh6Xg2LNgsbSG9vpHKF3QqJrayg0EZqfc9 5/Fwe76NuSzTjeU9X+yOw8ErY8MYJ8d+tVTxHtBv7aT38Bkz1bsWbcP37MivT/GCJcXF m0RA/30IBzEQ2TpvO8Lh4mkf3AfCJMMcJuHkxdJkcXGXeko1ZORKQFwzVN7zmPUBHMtC s+VPSWS2P6AWqLx0H7CGA3d980zpyze8IOZKt6iBhDERAfsNNozqDApeGYIy3zvDgs7B A9GdoLuwVh5FTwlBEACiSoDeKvvWbs4uojf8V2czy2WZGMOMnfBfXxP4u68BDvavKIHy H84w== X-Gm-Message-State: AJaThX6Y/gyS2k6B0jvwJKc2Wfj+yvlilf5sE9ubzBVDUva2/GLTA7T3 9/L1BzWzJpBkKcYBaIZunQ5s6ron X-Received: by 10.129.155.74 with SMTP id s71mr26846666ywg.231.1512966175031; Sun, 10 Dec 2017 20:22:55 -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 r62sm5042788ywh.86.2017.12.10.20.22.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 10 Dec 2017 20:22:54 -0800 (PST) To: Homotopy Type Theory From: Kristina Sojakova Subject: Impredicative set + function extensionality + proof irrelevance consistent? Message-ID: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> Date: Sun, 10 Dec 2017 23:22:57 -0500 User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.5.0 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Content-Language: en-US Dear all, I asked this question last year on the coq-club mailing list but did not receive a conclusive answer so I am trying here now. Is the theory with a proof-relevant impredicative universe Set, proof-irrelevant impredicative universe Prop, and function extensionality (known to be) consistent? It is known that the proof-irrelevance of Prop makes the Id type behave differently usual and in particular, makes the theory incompatible with univalence, so it is not just a matter of tacking on an interpretation for Prop. Thanks in advance for any insight, Kristina