From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.154.71 with SMTP id c68mr802677wme.14.1493129461988; Tue, 25 Apr 2017 07:11:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.0.69 with SMTP id 66ls988394lja.21.gmail; Tue, 25 Apr 2017 07:11:00 -0700 (PDT) X-Received: by 10.25.0.194 with SMTP id 185mr2708790lfa.14.1493129460352; Tue, 25 Apr 2017 07:11:00 -0700 (PDT) Return-Path: Received: from mail-wr0-x232.google.com (mail-wr0-x232.google.com. [2a00:1450:400c:c0c::232]) by gmr-mx.google.com with ESMTPS id f136si1384737wme.1.2017.04.25.07.11.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 25 Apr 2017 07:11:00 -0700 (PDT) Received-SPF: pass (google.com: domain of fav...@gmail.com designates 2a00:1450:400c:c0c::232 as permitted sender) client-ip=2a00:1450:400c:c0c::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of fav...@gmail.com designates 2a00:1450:400c:c0c::232 as permitted sender) smtp.mailfrom=fav...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x232.google.com with SMTP id l50so35773402wrc.3 for ; Tue, 25 Apr 2017 07:11:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=2CgOiQ36gMlY+hkry0CEGUfqN0Su39o1hcXzqurdXeI=; b=D4dTYpGoggcDVZ06vyC3APxQCXtVKt7MoIZD3RTgC+tL91JttfdO/EaTHY6JYC+VDL Z4wWPfUono4/aWJHwH/OwX1jSZrXwoMK0jf7G4ZpBOp80hkLbQqL6GNfg0ZDV3KCsIUo HFpzEt6Z8XqJdO3BbEUhqi2CUhFt9xPSdxjfTbrevmaRKrOeb4FrZWzkpwzwLF86dlPM SFExodnjkEmxg2l8F1iFf5M7cVdg6Pfi+hFzJl03vhFa/1/Y83KPLZQ13TdaK5+lWju4 LLhyacanFOUr6d81ij9ELQ60Zz56IpR7G8PkkiQfuQyJwsN8eEkoVwzzXvhrrsRlh7GA bFpg== X-Gm-Message-State: AN3rC/7NSvi6tm9N9gLsoKXo1MtnLBGVksNmlQgRiywneumWwHpcyypc ITc0rZ/KsM3aD4jVHY9yP132xKn6vg57 X-Received: by 10.223.132.39 with SMTP id 36mr9312420wrf.182.1493129460079; Tue, 25 Apr 2017 07:11:00 -0700 (PDT) MIME-Version: 1.0 References: <20170425131743.GB30195@mathematik.tu-darmstadt.de> In-Reply-To: <20170425131743.GB30195@mathematik.tu-darmstadt.de> From: Favonia Date: Tue, 25 Apr 2017 14:10:48 +0000 Message-ID: Subject: Re: [HoTT] computing K To: Thomas Streicher , Michael Shulman Cc: "HomotopyT...@googlegroups.com" , Jesper Cockx Content-Type: multipart/alternative; boundary=94eb2c0defc61261f8054dfe4b87 --94eb2c0defc61261f8054dfe4b87 Content-Type: text/plain; charset=UTF-8 I believe Mike is talking about a restricted version of K which only applies to types satisfying UIP, not all types. The question is whether a "weak" K which might not compute can be "strictified" to another K which does, at least in good models. By the way, my question about the restricted K was due to Jesper's attempt to have Agda automatically detect types that admit K (now temporarily disabled). -Favonia On Tue, Apr 25, 2017 at 9:17 AM Thomas Streicher < stre...@mathematik.tu-darmstadt.de> wrote: > 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 > > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --94eb2c0defc61261f8054dfe4b87 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I believe Mike is talking about a restricted version of K = which only applies to types satisfying UIP, not all types. The question is = whether a "weak" K which might not compute can be "strictifi= ed" to another K which does, at least in good models. By the way, my q= uestion about the restricted K was due to Jesper's attempt to have Agda= automatically detect types that admit K (now temporarily disabled). -Favon= ia

On Tue, Apr 25, 2017 at 9:17 AM Thomas Streicher <stre...@mathemat= ik.tu-darmstadt.de> wrote:
I= n 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 =3D=3D x) -> p =3D=3D refl
> K A x refl =3D refl
>
> then the equation "K A x refl =3D refl" holds definitionally= .=C2=A0 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<= br> > 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 c= onstructed
> for any hset.=C2=A0 Suppose we are in a model category whose cofibrati= ons
> are exactly the monomorphisms, like simplicial sets or any Cisinski > model category.=C2=A0 If A is an hset, then the map A -> Delta^*(PA= ) (which
> type theoretically is A -> Sigma(x:A) (x=3Dx)) is a weak equivalenc= e.
> But it is also a split monomorphism, hence a cofibration; and thus an<= br> > acyclic cofibration.=C2=A0 Therefore, we can define functions by induc= tion
> on loops in A that have definitionally computing behavior on refl,
> which is exactly what unrestricted pattern-matching allows.
>
> Mike
>

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--94eb2c0defc61261f8054dfe4b87--