From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.84.84 with SMTP id y20mr3008602ljd.21.1491421079342; Wed, 05 Apr 2017 12:37:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.99.213 with SMTP id v82ls2617519lfi.45.gmail; Wed, 05 Apr 2017 12:37:58 -0700 (PDT) X-Received: by 10.25.80.88 with SMTP id z24mr3966941lfj.29.1491421078016; Wed, 05 Apr 2017 12:37:58 -0700 (PDT) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id p10si130004wmg.1.2017.04.05.12.37.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 05 Apr 2017 12:37:57 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 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 sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1cvqkf-0005vD-Ov for HomotopyT...@googlegroups.com; Wed, 05 Apr 2017 20:37:57 +0100 Received: from 128.172.125.91.dyn.plus.net ([91.125.172.128] helo=[192.168.1.74]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1cvqkf-0001jQ-Eq for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Wed, 05 Apr 2017 20:37:57 +0100 Subject: Re: [HoTT] Conjecture To: "HomotopyT...@googlegroups.com" References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <2445fdca-d1bb-08c8-6061-e4a7e0faffa7@gmail.com> <98e87128-34a8-63a6-a055-8402498ef8b2@googlemail.com> <6767f0e2-a1e3-9d27-602c-8b81d8579893@googlemail.com> From: Martin Escardo Message-ID: Date: Wed, 5 Apr 2017 20:37:57 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 In-Reply-To: <6767f0e2-a1e3-9d27-602c-8b81d8579893@googlemail.com> 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) On 31/03/17 17:09, 'Martin Escardo' via Homotopy Type Theory wrote: > > > On 30/03/17 23:49, Nicolai Kraus wrote: >> Interesting construction by Cory and you! And I think I can help >> you with the factorisation that you asked for, as follows: > > Thanks for this, Nicolai. > > Cory and I a battling against the clock to get our submission ready for > a conference. I'll continue the discussion after that. I may as well give a link to the paper now that we have finished and submitted it, which is about partial functions in univalent type theory: http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf The conjecture in the initial message of this thread goes well beyond this, and is even unrelated. But I am still very interested in the conjecture independently of any use of it. Martin