From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.189.203 with SMTP id n194mr4310004vkf.26.1493113603054; Tue, 25 Apr 2017 02:46:43 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.19.72 with SMTP id q8ls14202977otq.23.gmail; Tue, 25 Apr 2017 02:46:42 -0700 (PDT) X-Received: by 10.157.53.78 with SMTP id l14mr10236101ote.28.1493113602527; Tue, 25 Apr 2017 02:46:42 -0700 (PDT) Return-Path: Received: from mail-yw0-x230.google.com (mail-yw0-x230.google.com. [2607:f8b0:4002:c05::230]) by gmr-mx.google.com with ESMTPS id t84si2577785ywa.1.2017.04.25.02.46.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 25 Apr 2017 02:46:42 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x230.google.com with SMTP id k11so46474486ywb.1 for ; Tue, 25 Apr 2017 02:46:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:from:date:message-id:subject:to; bh=8WAZ8UJ8Ie1orBqbq3I5uSZSp5UGTkOsrBRnIbdm2ys=; b=PbUmqtN1RCd0dOyeeYmoGT6uVhDvuQUpZMX58XlnveMjzimJhc8MDbcZYRPmG8VtwC RywxTjRpqWTfVmHwLJ9n9NSPZMYGSPbzVbA7Z9opTN5r014c+858eea7Upcfq2wBa/Ye Wshp06irgBvDJCYI6ODLN0nMFOx4rku9xHU6aaNECXx7+XQMogBGX56+IInAlPpz7s8k I8Z9p7kqaLybqM6FKFHt96x7U53euSeMLqEky17utTVSHf60fWXSQSMkoZTM29XzcI9p XxgOPwCCkiZJpcN/mTevHDyv2YcIrcHdIxjl4KARsdaDbJMUGGPucNuQ2cO5wi/ta3Qh JLCg== X-Gm-Message-State: AN3rC/5LOVJrK1jkPWFZGSXIIIGymi8A1pbnPm4CmtbrApZLd6vDAEbj sbYut/poijNGQSeYRh0= X-Received: by 10.129.44.138 with SMTP id s132mr7899044yws.221.1493113602125; Tue, 25 Apr 2017 02:46:42 -0700 (PDT) Return-Path: Received: from mail-yw0-f169.google.com (mail-yw0-f169.google.com. [209.85.161.169]) by smtp.gmail.com with ESMTPSA id b204sm8336015ywh.36.2017.04.25.02.46.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 25 Apr 2017 02:46:41 -0700 (PDT) Received: by mail-yw0-f169.google.com with SMTP id k11so46479991ywb.1 for ; Tue, 25 Apr 2017 02:46:41 -0700 (PDT) X-Received: by 10.129.79.210 with SMTP id d201mr7941934ywb.132.1493113601502; Tue, 25 Apr 2017 02:46:41 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.207.1 with HTTP; Tue, 25 Apr 2017 02:46:21 -0700 (PDT) From: Michael Shulman Date: Tue, 25 Apr 2017 02:46:21 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: computing K To: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset=UTF-8 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