From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.131.194 with SMTP id f185mr768716wmd.18.1493126266515; Tue, 25 Apr 2017 06:17:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.88.82 with SMTP id x18ls1079569ljd.9.gmail; Tue, 25 Apr 2017 06:17:44 -0700 (PDT) X-Received: by 10.46.87.26 with SMTP id l26mr4076489ljb.12.1493126264873; Tue, 25 Apr 2017 06:17:44 -0700 (PDT) Return-Path: Received: from lnx503.hrz.tu-darmstadt.de (mail-relay15.hrz.tu-darmstadt.de. [130.83.156.239]) by gmr-mx.google.com with ESMTPS id f194si765138wmg.0.2017.04.25.06.17.44 for (version=TLS1 cipher=AES128-SHA bits=128/128); Tue, 25 Apr 2017 06:17:44 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id v3PDHhhr014789; Tue, 25 Apr 2017 15:17:43 +0200 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id v3PDHhES026684; Tue, 25 Apr 2017 15:17:43 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 797271A0C6D; Tue, 25 Apr 2017 15:17:43 +0200 (CEST) Date: Tue, 25 Apr 2017 15:17:43 +0200 From: Thomas Streicher To: Michael Shulman Cc: "HomotopyT...@googlegroups.com" Subject: Re: [HoTT] computing K Message-ID: <20170425131743.GB30195@mathematik.tu-darmstadt.de> References: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2017.4.25.130616 X-PMX-RELAY: outgoing In lccc's (actually finite limits cats) there is no problem to have K. But K allows one to prove UIP which is in contradiction with UA. So we can't have K in all model cat's modelling intensioal TT. Thomas > 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 >