From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.71.82 with SMTP id u79mr156053lja.3.1490651834502; Mon, 27 Mar 2017 14:57:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.131.70 with SMTP id f67ls1622165wmd.20.canary-gmail; Mon, 27 Mar 2017 14:57:13 -0700 (PDT) X-Received: by 10.28.169.83 with SMTP id s80mr150107wme.1.1490651833692; Mon, 27 Mar 2017 14:57:13 -0700 (PDT) Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id p144si69718wme.2.2017.03.27.14.57.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 27 Mar 2017 14:57:13 -0700 (PDT) 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 1cscdV-0007jQ-O0 for HomotopyT...@googlegroups.com; Mon, 27 Mar 2017 22:57:13 +0100 Received: from 128.172.125.91.dyn.plus.net ([91.125.172.128] helo=[192.168.1.75]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1cscdV-0002c4-E6 for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Mon, 27 Mar 2017 22:57:13 +0100 To: "HomotopyT...@googlegroups.com" From: Martin Escardo Subject: Conjecture Message-ID: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> Date: Mon, 27 Mar 2017 22:57:12 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 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) This is a question I would like to see eventually answered. I posed it a few years ago in a conference (and privately among some of you), but I would like to have it here in this list for the record. Definition. A modulus of constancy for a function f:X->Y is a function (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli of constancy, but if Y is a set then it can have at most one.) We know that if Y is a set and f comes with a modulus of constancy, then f factors through |-|: X -> ||Y||, meaning that we can exhibit an f':||X||->Y with f'|x| = f(x). Conjecture. If for all types X and Y and all functions f:X->Y equipped with a modulus of constancy we can exhibit f':||X||->Y with f'|x| = f(x), then all types are sets. For this conjecture, I assume function extensionality and propositional extensionality, but not (general) univalence. But feel free to play with the assumptions. Martin