From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.46.7.10 with SMTP id 10mr761796ljh.1.1490976251816;
        Fri, 31 Mar 2017 09:04:11 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.46.8.73 with SMTP id g9ls554896ljd.33.gmail; Fri, 31 Mar 2017
 09:04:10 -0700 (PDT)
X-Received: by 10.25.153.74 with SMTP id b71mr801279lfe.23.1490976250688;
        Fri, 31 Mar 2017 09:04:10 -0700 (PDT)
Return-Path: <escardo...@googlemail.com>
Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150])
        by gmr-mx.google.com with ESMTPS id e72si267936wma.0.2017.03.31.09.04.10
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Fri, 31 Mar 2017 09:04:10 -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.127] (helo=bham.ac.uk)
	by sun61.bham.ac.uk with esmtp (Exim 4.84)
	(envelope-from <escardo...@googlemail.com>)
	id 1ctz22-0002Lp-O3
	for HomotopyT...@googlegroups.com; Fri, 31 Mar 2017 17:04:10 +0100
Received: from mx1.cs.bham.ac.uk ([147.188.192.53])
	by bham.ac.uk (envelope-from
	<escardo...@googlemail.com>)
	with esmtp (Exim 4.84)
	id 1ctz22-00035t-EE
	for HomotopyT...@googlegroups.com 
	using interface smart1.bham.ac.uk; Fri, 31 Mar 2017 17:04:10 +0100
Received: from dynamic200-118.cs.bham.ac.uk ([147.188.200.118])
	by mx1.cs.bham.ac.uk with esmtp (Exim 4.51)
	id 1ctz22-0003ys-Bt
	for HomotopyT...@googlegroups.com; Fri, 31 Mar 2017 17:04:10 +0100
Subject: Re: [HoTT] Conjecture
To: "HomotopyT...@googlegroups.com"
 <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>
 <dfcfdadd-2324-38c0-916b-f0fa3a10d292@gmail.com>
From: Martin Escardo <escardo...@googlemail.com>
Message-ID: <6767f0e2-a1e3-9d27-602c-8b81d8579893@googlemail.com>
Date: Fri, 31 Mar 2017 17:09:43 +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: <dfcfdadd-2324-38c0-916b-f0fa3a10d292@gmail.com>
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 7bit
X-BHAM-SendViaRouter: yes



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.

Best,
Martin