From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.111.75 with SMTP id k72mr16222891pgc.148.1493161718034; Tue, 25 Apr 2017 16:08:38 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.82.106 with SMTP id q42ls6368479otg.12.gmail; Tue, 25 Apr 2017 16:08:37 -0700 (PDT) X-Received: by 10.129.57.85 with SMTP id g82mr15945087ywa.77.1493161717375; Tue, 25 Apr 2017 16:08:37 -0700 (PDT) Return-Path: Received: from mail-yw0-x235.google.com (mail-yw0-x235.google.com. [2607:f8b0:4002:c05::235]) by gmr-mx.google.com with ESMTPS id m63si1883202ywd.5.2017.04.25.16.08.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 25 Apr 2017 16:08:37 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::235 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::235; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::235 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x235.google.com with SMTP id k11so56348137ywb.1 for ; Tue, 25 Apr 2017 16:08:37 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=1aoS6GddBa5G0uKcuNHnCSilxjCU5Bm2fcPmPcxXPlI=; b=uHpWarPluIS83ZcS1Uw9mx9pIvdqaI+tuG7aGVtPAshVMb9J4Z357V9hLpLioSkGDS KYCRSW0B3uWgkvxFY5LGJ3Vp8lkiCWG13ZPdX20L5hv65spBgM0eedzPTfzPPMSpHwgr CF6i0Y0pecRtt6wdZJwLpVlgsfp912fH687N149d89rbQompsjtOnL22NxgL4EOGzRFz lx10YLAPj5cb88QsSW9/uLnQAe9/Vr9ceNlGPOM84nANOjVFXZpKVgBNCN01+O4vWeSb gQ5QvIwFn6sJEVhoCvhfl27q5zfyvSA4tbFeXd05KwitIqrp4b98fGd9LHB5NtMBLdfA 3ARA== X-Gm-Message-State: AN3rC/5c8S11aKFBhCeyf5CrakeDkssZi8Be0n9odomedHk8A4IV9wDY djiHgHYs5raipWnBHNw= X-Received: by 10.129.181.8 with SMTP id t8mr11897618ywh.261.1493161716751; Tue, 25 Apr 2017 16:08:36 -0700 (PDT) Return-Path: Received: from mail-yb0-f169.google.com (mail-yb0-f169.google.com. [209.85.213.169]) by smtp.gmail.com with ESMTPSA id b21sm9243652ywa.48.2017.04.25.16.08.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 25 Apr 2017 16:08:36 -0700 (PDT) Received: by mail-yb0-f169.google.com with SMTP id 81so71986611ybp.0 for ; Tue, 25 Apr 2017 16:08:35 -0700 (PDT) X-Received: by 10.37.10.199 with SMTP id 190mr4963906ybk.142.1493161715604; Tue, 25 Apr 2017 16:08:35 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.207.1 with HTTP; Tue, 25 Apr 2017 16:08:15 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Tue, 25 Apr 2017 16:08:15 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] computing K To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset=UTF-8 Favonia, Dan Licata, and I spent a bit of time trying to answer (1) but didn't get anywhere. I haven't thought much about (2), but I think we were unable to think of any nontrivial types for which we could construct a computing K inside MLTT. On Tue, Apr 25, 2017 at 3:04 PM, Martin Escardo wrote: > 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 >> > > -- > Martin Escardo > http://www.cs.bham.ac.uk/~mhe