From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.72.71 with SMTP id v68mr1968291lfa.9.1491186014981; Sun, 02 Apr 2017 19:20:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.69.85 with SMTP id s82ls781260lja.45.gmail; Sun, 02 Apr 2017 19:20:14 -0700 (PDT) X-Received: by 10.25.216.154 with SMTP id r26mr1861217lfi.7.1491186013997; Sun, 02 Apr 2017 19:20:13 -0700 (PDT) Return-Path: Received: from mail-wr0-x231.google.com (mail-wr0-x231.google.com. [2a00:1450:400c:c0c::231]) by gmr-mx.google.com with ESMTPS id 82si940290wmg.3.2017.04.02.19.20.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 02 Apr 2017 19:20:13 -0700 (PDT) Received-SPF: pass (google.com: domain of fav...@gmail.com designates 2a00:1450:400c:c0c::231 as permitted sender) client-ip=2a00:1450:400c:c0c::231; 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::231 as permitted sender) smtp.mailfrom=fav...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x231.google.com with SMTP id w11so147636410wrc.3 for ; Sun, 02 Apr 2017 19:20:13 -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; bh=q3iznaRWhgWPhbmvbAQuGKjOD9/ETHV/bjMuG0yJbfY=; b=Ib8C9Qw7ybnlsLD66Te1MyjEuFoZNuBUOLwAy1dBy2m6lwaScb8IJjn9YrnYVVN3EH WiriPzH4UsajPk29Y9pKA8Iu3ocoqyjr5D1xpAvMIrNmKWuR3CDsJXmXYPSzL3c0/POj Btia6Q8O+X9ShZVCw67/nqpQC/S2Dcf/xdABi/PyPO9bhfB35bDBivKxT25pOAnXnPUr 86gwTmj/8GxUoimP1hr3QOrlVVcuh1KSSrcMgqgtYylF28+GzyEaIlLQdAmv21tZ9/50 ocBId6ltqZ8NtvQSbcjiA3pYbUfpunAqJwsovywBd3/tEzsc0y8HPLKIhGZm1R8t7jJS BVUg== X-Gm-Message-State: AFeK/H25m8b7Z0ZAIZXTDC1wgdC9JfbiR2nIdtXzissbdsIyVcrmMUss3OnSVLSELJ4gQmzByf1ENv2+1jebRg== X-Received: by 10.223.171.179 with SMTP id s48mr11266944wrc.167.1491186013799; Sun, 02 Apr 2017 19:20:13 -0700 (PDT) MIME-Version: 1.0 References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <3016af27-384d-4b95-9a04-5c803e08608e@googlegroups.com> In-Reply-To: <3016af27-384d-4b95-9a04-5c803e08608e@googlegroups.com> From: Favonia Date: Mon, 03 Apr 2017 02:20:02 +0000 Message-ID: Subject: Re: [HoTT] Re: Conjecture To: "Daniel R. Grayson" , Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a113c5b20a58b85054c39ccba --001a113c5b20a58b85054c39ccba Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Yes, this has been known from Nicolai's work on truncation (e.g. "The General Universal Property"). I just learned that this has been mechanized in Agda by Nils as well. http://www.cse.chalmers.se/~nad/listings/equality/H-level.Truncation.html#1= 8216 By the way, the condition (=E2=88=8F x, c x x =3D idpath (f x)) is provable fr= om transitivity. -Favonia On Sun, Apr 2, 2017 at 8:35 PM Daniel R. Grayson < danielrich...@gmail.com> wrote: Here's a fact related to the current discussion, which I have formalized today. I would appreciate knowing whether it's already known. It gives a criterion for factoring through the propositional truncation when the target is of h-level 3. Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3} (f : X -> Y) (c : =E2=88=8F x x', f x =3D f x') : (=E2=88=8F x, c x x =3D idpath (f x)) -> (=E2=88=8F x x' x'', c x x'' =3D c x x' @ c x' x'') -> =E2=88=A5 X =E2=88=A5 -> Y. You may find it in WellOrderedSets.v on one of my branches. --=20 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. --001a113c5b20a58b85054c39ccba Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Yes, this has been kn= own from Nicolai's work on truncation (e.g. "The General Universal= Property"). I just learned that this has been mechanized in Agda by N= ils as well. http://= www.cse.chalmers.se/~nad/listings/equality/H-level.Truncation.html#18216=C2=A0By the way, the condition (=E2=88=8F x, c x x =3D idpath (f x)) is p= rovable from transitivity. -Favonia

On Sun, Apr= 2, 2017 at 8:35 PM Daniel R. Grayson <danielrich...@gmail.com= > wrote:
Here's a fact related to th= e current discussion, which I have formalized today.=C2=A0 I would apprecia= te knowing
whether it's already known.=C2=A0 It= gives a criterion for factoring through the propositional truncation
=
when the target is of h-level 3.

=C2=A0 Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3}
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(f : X -> Y) (c= : =E2=88=8F x x', f x =3D f x') :
=C2=A0 =C2= =A0 (=E2=88=8F x, c x x =3D idpath (f x)) ->
=C2=A0 = =C2=A0 (=E2=88=8F x x' x'', c x x'' =3D c x x' @ c = x' x'') ->
=C2=A0 =C2=A0 =E2=88=A5 X = =E2=88=A5 -> Y.

You may find it in=C2=A0WellOrderedSets.v=C2=A0on one of my branche= s.


--
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.
--001a113c5b20a58b85054c39ccba--