From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.5.136 with SMTP id 130mr253832ljf.6.1490914193238; Thu, 30 Mar 2017 15:49:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.5.133 with SMTP id 127ls429780ljf.39.gmail; Thu, 30 Mar 2017 15:49:52 -0700 (PDT) X-Received: by 10.25.145.17 with SMTP id t17mr251009lfd.25.1490914192212; Thu, 30 Mar 2017 15:49:52 -0700 (PDT) Return-Path: Received: from mail-wr0-x236.google.com (mail-wr0-x236.google.com. [2a00:1450:400c:c0c::236]) by gmr-mx.google.com with ESMTPS id 82si33294wmg.3.2017.03.30.15.49.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 30 Mar 2017 15:49:52 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c0c::236 as permitted sender) client-ip=2a00:1450:400c:c0c::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c0c::236 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x236.google.com with SMTP id l43so82332578wre.1 for ; Thu, 30 Mar 2017 15:49:52 -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; bh=qWOdAPWOkEjdQJThQ8+Sl0HBdpQ5+xscpbpjzZe0xqg=; b=Lu2SNCQL5/F+NcakjhyDbIuFBMtbVPl9bJmAXeNbFgxEjyRL6DPiN8y3QtDoh33P5G aJZsNrqKGEqLwBTEa55wS9SR6U7XMpCm34c6Ji5w9ChwA7Ys5wYpAZYR+4oqVoPfZgYU lled14L0z2XO/SRJa8asfMBOl+EPvyIc+w+JV06xdAUHxrd26cY1yjCFNBWWSuvnmG5V +uhwN79V8jwk4FgwVKfBSxqWuNA7Z0FAG5TDBu38rbVfD1iW97J2sFiBvOd+kpvgewDk jnyLCB8HYrRQ3jEGLtgCcalgH7fKuBlHRwuL5RxaxDRNY7vrjbah1UO2emOVp5sgnef0 Twpg== X-Gm-Message-State: AFeK/H257SEzJh9nu3CVlPT5x2W7foreTEbJfxixCBoV0GGSP1iRXjZnAHArwv0M+gcYQA== X-Received: by 10.28.100.67 with SMTP id y64mr400340wmb.133.1490914191527; Thu, 30 Mar 2017 15:49:51 -0700 (PDT) Return-Path: Received: from [192.168.0.23] (cpc86229-nott20-2-0-cust356.12-2.cable.virginm.net. [82.7.65.101]) by smtp.gmail.com with ESMTPSA id 204sm572603wmw.0.2017.03.30.15.49.50 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 30 Mar 2017 15:49:50 -0700 (PDT) Subject: Re: [HoTT] Conjecture To: Martin Escardo , "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> From: Nicolai Kraus Message-ID: Date: Thu, 30 Mar 2017 23:49:49 +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: <98e87128-34a8-63a6-a055-8402498ef8b2@googlemail.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Interesting construction by Cory and you! And I think I can help you with the factorisation that you asked for, as follows: On 29/03/17 23:05, 'Martin Escardo' via Homotopy Type Theory wrote: > Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct > its least upper bound. > > Its extent of definition is the proposition ||Sigma_i, P_i||, and the > question is how we define > > f:||Sigma_i, P_i||->X. > > We know how to define > > f':(Sigma_i, P_i)->X > > [...] > > What if X is not a set? (I assume that it is i : Nat in the above.) We can construct the proof of constancy for f' by only going "steps of length 1", i.e. we do it only using the equality proofs of the form f'(i,_) = f'(i+1,_). This constancy proof is coherent up to whichever level you want. By arXiv:1411.2682 Thm 10.5, this means that you can replace the condition "X is a set" by "X is 1-truncated" or "X is 17-truncated" or any finite number you want (this uses funext, but nothing else). With a different strategy, we can do better and drop all assumptions on X. Given this family (P_i, -, f_i), we can define the HIT R with constructors r : (i : Nat) -> P_i -> R s : (i : Nat) -> (p : P_i) -> (r i p) = (r (i+1) (t i p) (where t i : P_i -> P_{i+1} comes from the proof that the family is directed). Now, we can show that R is a proposition. (One way is this: To show R -> isContr(R), we can assume that we are given (r i p : R), and we can prove that this is a centre of contraction.) R is equivalent to ||Sigma_i, P_i||, and it's easy to construct R -> X. Best, Nicolai