From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.223.168.23 with SMTP id l23mr145642wrc.17.1493242402459; Wed, 26 Apr 2017 14:33:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.188.132 with SMTP id m126ls504647wmf.12.gmail; Wed, 26 Apr 2017 14:33:21 -0700 (PDT) X-Received: by 10.28.186.66 with SMTP id k63mr17101wmf.9.1493242401420; Wed, 26 Apr 2017 14:33:21 -0700 (PDT) Return-Path: Received: from mail-lf0-x231.google.com (mail-lf0-x231.google.com. [2a00:1450:4010:c07::231]) by gmr-mx.google.com with ESMTPS id f136si16849wme.1.2017.04.26.14.33.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 26 Apr 2017 14:33:21 -0700 (PDT) Received-SPF: pass (google.com: domain of fpvd...@gmail.com designates 2a00:1450:4010:c07::231 as permitted sender) client-ip=2a00:1450:4010:c07::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of fpvd...@gmail.com designates 2a00:1450:4010:c07::231 as permitted sender) smtp.mailfrom=fpvd...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x231.google.com with SMTP id 75so7417668lfs.2 for ; Wed, 26 Apr 2017 14:33:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=coRb0xpULZgsjLoyTYDoHJOjxhHP5f8Qefyvgp4n55U=; b=Mw0Bxgv1+30Z/0uWjFgYYdcpRNsSLZ/Jg/GSJo4Yfivrx/nuwHAAQMsJYloiYekxDB 8iSDiR4iT02LRjv0qHrUnRPHsUIXDrmVQahQ49i7zm0NZFKWSgOuPQmoq9jXRxoVzKUT 9UJkkgg4qRhoAmgErix0ePUqumNthmw32tARH0X/jRHzbFyMlLNIWr3MZL9bnsBx2qL7 v/BC8zWAkfix1vPjcQfapoQnbmozAYj0MiQqfEPlLakB2I8N55VJ8BqQvjkBetvJYb8X 2EofB2XSBgbkBfNFhDR5l19dzzuLE5W8k5HgjIY51bhhJRPjkWXmRF78ACV+oNuUjjBz Hqdg== X-Gm-Message-State: AN3rC/4s3kc8Ak++YN0s5jwnleH8KXabvAczHxEt33mo0LdJ2odDH4mJ syFoo6KBJZO8ZummbCIhh5G7OBElUw== X-Received: by 10.25.155.145 with SMTP id d139mr717616lfe.174.1493242400891; Wed, 26 Apr 2017 14:33:20 -0700 (PDT) MIME-Version: 1.0 Received: by 10.46.88.17 with HTTP; Wed, 26 Apr 2017 14:33:00 -0700 (PDT) In-Reply-To: References: From: Floris van Doorn Date: Wed, 26 Apr 2017 17:33:00 -0400 Message-ID: Subject: Re: [HoTT] computing K To: "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary=001a11402298de692b054e18967e --001a11402298de692b054e18967e Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Disregard previous email. I misread Mike's proposed computing K (I thought it was refl on all loops). On 26 April 2017 at 16:40, Floris van Doorn wrote: > I think (1) is indeed wishful thinking. > > I can disprove it assuming the following metatheoretical property. I thin= k > this property holds for book-HoTT, but I'm not sure. > > If X is a HIT and p : A -> X is a path constructor of X, and if p a =E2= =89=A1 p a' > for terms a a' : A then a =E2=89=A1 a'. (Here =E2=89=A1 is judgmental equ= ality.) > > I believe that similar properties are true for MLTT if p is a constructor > of an inductive type. > > Now let I be the interval with points 0, 1 : I and consider the following > HIT: > HIT X :=3D > | * : X > | p : I -> * =3D * > | q : p(0) =3D refl > Note that X is the reduced suspension of the interval, which is > contractible, hence in particular a set. But assuming the above > metatheoretical property, X cannot have an axiom K with the definitional > properties Mike described. That would mean that p(0) =E2=89=A1 p(1) and h= ence 0 =E2=89=A1 > 1. But it is impossible that the two points of the interval are > judgmentally equal (because you can make a function which sends them to > equal, but not judgmentally equal terms, for example (=CE=A3(X : Type), X= =3D > empty) and (=CE=A3(X : Type), X =3D unit)). > > Best, > Floris > > On 25 April 2017 at 19:08, Michael Shulman wrote: > >> 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 =3D=3D x) -> p =3D=3D refl >> > >> > is given, internally in a univalent type theory. >> > >> > Is it possible to cook-up a K' of the same type, internally in univale= nt >> > type theory, with the definitional behaviour you require? >> > >> > We are looking for an endofunction of the type ((x : A) (p : x =3D=3D = x) -> >> p =3D=3D >> > refl) that performs some sort of definitional improvement. >> > >> > We know of an instance of such a phenomenon: if a factor f':||X||->A o= f >> 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 typ= e >> A' >> > equivalent to A (maybe A'=3D Sigma(x:A) (x=3Dx)) 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 =3D=3D x) -> p =3D=3D refl >> >> K A x refl =3D refl >> >> >> >> then the equation "K A x refl =3D 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 constructe= d >> >> 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) (whic= h >> >> type theoretically is A -> Sigma(x:A) (x=3Dx)) 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 >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >> > > --001a11402298de692b054e18967e Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Disregard previous email. I misread Mike's proposed co= mputing K (I thought it was refl on all loops).

On 26 April 2017 at 16:40, Floris v= an Doorn <fpvd...@gmail.com> wrote:
I = think (1) is indeed wishful thinking.

I can disprove it assuming th= e following metatheoretical property. I think this property holds for book-= HoTT, but I'm not sure.

If X is a HIT and p : A -> X is= a path constructor of X, and if p a =E2=89=A1 p a' for terms a a' = : A then a =E2=89=A1 a'. (Here =E2=89=A1 is judgmental equality.)
I believe that similar properties are true for MLTT if p is a const= ructor of an inductive type.

Now let I be the interval with points = 0, 1 : I and consider the following HIT:
HIT X :=3D
| * := X
| p : I -> * =3D *
| q : p(0) =3D refl
Not= e that X is the reduced suspension of the interval, which is contractible, = hence in particular a set. But assuming the above metatheoretical property,= X cannot have an axiom K with the definitional properties Mike described. = That would mean that p(0) =E2=89=A1 p(1) and hence 0 =E2=89=A1 1. But it is= impossible that the two points of the interval are judgmentally equal (bec= ause you can make a function which sends them to equal, but not judgmentall= y equal terms, for example (=CE=A3(X : Type), X =3D empty) and (=CE=A3(X : = Type), X =3D unit)).

Best,
Floris

On 25 April 2017 at 19:08, Michael Shulman &= lt;shu...@sandiego= .edu> wrote:
Favonia, Dan L= icata, and I spent a bit of time trying to answer (1)
but didn't get anywhere.=C2=A0 I haven't thought much about (2), bu= t 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 <m.es...@cs.bham.ac.uk> wrote: > Interesting. So, then, here are some questions:
>
> (1) Suppose, for given type A, a hypothetical
>
> K: (x : A) (p : x =3D=3D x) -> p =3D=3D refl
>
> is given, internally in a univalent type theory.
>
> Is it possible to cook-up a K' of the same type, internally in uni= valent
> type theory,=C2=A0 with the definitional behaviour you require?
>
> We are looking for an endofunction of the type ((x : A) (p : x =3D=3D = x) -> p =3D=3D
> 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#155= 08
> and also in a paper by Nicolai, Thorsten, Thierry and myself.
>
> (2) Failing that, can we, given the same hypothetical K, cook-up a typ= e A'
> equivalent to A (maybe A'=3D Sigma(x:A) (x=3Dx)) with K' as ab= ove?
>
> (That is, maybe A itself won't provably have (1), but still will h= ave 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 ref= l.
>> 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 definition= ally.=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
>> allow unrestricted pattern-matching when the types are automatical= ly
>> provable to be hsets, since a general hset apparently need not adm= it 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.=C2=A0 Suppose we are in a model category whose cofib= rations
>> are exactly the monomorphisms, like simplicial sets or any Cisinsk= i
>> 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 equiva= lence.
>> But it is also a split monomorphism, hence a cofibration; and thus= an
>> acyclic cofibration.=C2=A0 Therefore, we can define functions by i= nduction
>> 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

--
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.


--001a11402298de692b054e18967e--