From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.173.38 with SMTP id w38mr3912590ioe.10.1493355357573; Thu, 27 Apr 2017 21:55:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.17.19 with SMTP id g19ls5453272ote.17.gmail; Thu, 27 Apr 2017 21:55:57 -0700 (PDT) X-Received: by 10.157.60.247 with SMTP id t52mr3175028otf.110.1493355357182; Thu, 27 Apr 2017 21:55:57 -0700 (PDT) Received: by 10.55.170.198 with SMTP id t189msqke; Tue, 25 Apr 2017 15:05:14 -0700 (PDT) X-Received: by 10.25.56.8 with SMTP id f8mr3913876lfa.13.1493157914209; Tue, 25 Apr 2017 15:05:14 -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 d184si1520382wmc.0.2017.04.25.15.05.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 25 Apr 2017 15:05:14 -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 1d38a9-0005cx-PX for homotopyt...@googlegroups.com; Tue, 25 Apr 2017 23:05:13 +0100 Received: from laubervilliers-656-1-172-228.w193-251.abo.wanadoo.fr ([193.251.57.228] helo=[192.168.1.26]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1d38a9-0006bX-F8 for homotopyt...@googlegroups.com using interface auth-smtp.bham.ac.uk; Tue, 25 Apr 2017 23:05:13 +0100 Subject: Re: [HoTT] computing K To: "HomotopyT...@googlegroups.com" References: From: Martin Escardo Message-ID: Date: Tue, 25 Apr 2017 23:05:12 +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: Content-Type: text/plain; charset=utf-8; format=flowed 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) Interesting. So, then, here are some questions: (1) Suppose, for given type A, a hypothetical K: (x : A) (p : x == x) -> p == refl is given, internally in a univalent type theory. Is it possible to cook-up a K' of the same type, internally in univalent type theory, with the definitional behaviour you require? We are looking for an endofunction of the type ((x : A) (p : x == x) -> p == refl) that performs some sort of definitional improvement. We know of an instance of such a phenomenon: if a factor f':||X||->A of some f:X->A through |-|:X->||X|| is given, then we can find another *definitional* factor f':||X||->A. This is here in agda http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html#15508 and also in a paper by Nicolai, Thorsten, Thierry and myself. (2) Failing that, can we, given the same hypothetical K, cook-up a type A' equivalent to A (maybe A'= Sigma(x:A) (x=x)) with K' as above? (That is, maybe A itself won't provably have (1), but still will have an equivalent manifestation which does.) Or is this wishful thinking? Martin On 25/04/17 10:46, Michael Shulman wrote: > Here is a little observation that may be of interest (thanks to > Favonia for bringing this question to my attention). > > The Axiom K that is provable using unrestricted Agda-style > pattern-matching has an extra property: it computes to refl on refl. > That is, if we define > > K: (A : Type) (x : A) (p : x == x) -> p == refl > K A x refl = refl > > then the equation "K A x refl = refl" holds definitionally. As was > pointed out on the Agda mailing list a while ago, this might be > considered a problem if one wants to extend Agda's --without-K to > allow unrestricted pattern-matching when the types are automatically > provable to be hsets, since a general hset apparently need not admit a > K satisfying this *definitional* behavior. > > However (this is the perhaps-new observation), in good > model-categorical semantics, such a "computing K" *can* be constructed > for any hset. Suppose we are in a model category whose cofibrations > are exactly the monomorphisms, like simplicial sets or any Cisinski > model category. If A is an hset, then the map A -> Delta^*(PA) (which > type theoretically is A -> Sigma(x:A) (x=x)) is a weak equivalence. > But it is also a split monomorphism, hence a cofibration; and thus an > acyclic cofibration. Therefore, we can define functions by induction > on loops in A that have definitionally computing behavior on refl, > which is exactly what unrestricted pattern-matching allows. > > Mike >