From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 23 Mar 2017 04:22:43 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Cc: Thierry...@cse.gu.se, vlad...@ias.edu, univalent-...@googlegroups.com Message-Id: <4f4bcfe8-5d25-42f4-9bf2-ebf5748d629a@googlegroups.com> In-Reply-To: <7EFC9320-4852-469F-9609-16C27D969316@ias.edu> References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> <96ed5e86-5564-4d98-a759-5a3301968501@googlegroups.com> <7EFC9320-4852-469F-9609-16C27D969316@ias.edu> Subject: Re: [HoTT] about the HTS MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_226_372047895.1490268163823" ------=_Part_226_372047895.1490268163823 Content-Type: multipart/alternative; boundary="----=_Part_227_1121601362.1490268163823" ------=_Part_227_1121601362.1490268163823 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Thanks. I agree that with the sSet option, with an equality reflection rule, it=20 would be infeasible to check judgments without extra stuff from outside the= =20 type theory proper. But what's wrong with that? We add extra stuff anyway,= =20 like type classes, proof scripts, and implicit arguments. To me, it seems= =20 that the practical concern of checking the truth of judgments does not need= =20 to be solved by the design of the core type theory. Indeed, it seems like= =20 better separation of concerns *not* to solve it there. Anyway, my understanding of bSet, from what Thierry Coquand said, is that= =20 it'd be a more OTT-like version of sSet, which is more ETT-like. So instead= =20 of paths between bSets being reflectable to judgmental equalities, they=20 would be "strict propositions" (sProp), whose elements are not only all=20 (typally) equal, but they also have no computational content. So any=20 "transport" across a strict equality reduces away, as long as it doesn't=20 change the type. (It doesn't have to be (judgmentally equal to)=20 reflexivity.) I figure the idea is that bSet should be able to do everything sSet can,=20 just with extra computationally-irrelevant transports thrown in to appease= =20 a decidable type checker. I don't actually see how either of these universes would help define=20 semi-simplicial types. I didn't realize that was the goal here. I thought= =20 we were just trying to make set-level math more convenient. ----------- Though I haven't given it a serious thinking-about, I figured that stuff=20 with cohesion would be a good way to make semi-simplicial types definable,= =20 without adding non-fibrant types.=20 (https://homotopytypetheory.org/2015/09/25/realcohesion/) It sounded like= =20 cohesion gives you a set-level view of non-hsets, so I figured you should= =20 be able to use strict equality in the construction of non-hsets that way. I suppose strict sets and cohesion can be combined. A set-level view of=20 things should yield only strict sets, not arbitrary hsets. (I guess that=20 requires a whole hierarchy of strict set universes. But unlike HTS, they're= =20 all "included" in the univalent universes, not the other way around.) On Wednesday, March 22, 2017 at 5:01:16 PM UTC-4, v v wrote: > > 1. As Thierry pointed out previously, the problem with sSet is that if we= =20 > postulate that nat:sSet, then for any (small) type T, the function type T= =20 > -> nat is in sSet, e.g. nat -> nat is in sSet. > > Since it is possible to construct two elements of nat -> nat the equality= =20 > between which is an undecidable proposition, it implies that the=20 > definitional equality in any sufficiently advanced type system with sSet= =20 > and nat:sSet is undecidable. > > That means that witnesses, in some language, of definitional equality nee= d=20 > to be carried around and therefore the design of a proof assistant where= =20 > the proof term is the proof is not possible in this system. > > 2. It is not so clear what would happen with only bSet and nat:bSet.=20 > > Vladimir. > > > > > > On Mar 22, 2017, at 5:49 PM, Thierry Coquand > wrote: > > > If my note was correct, it describes in the cubical set model two=20 > univalent universes > (subpresheaf of the first universe) that satisfy > > (1) if A : sSet and p : Path A a b then a =3D b : A and p = is=20 > the constant path a > (equality reflection rule) > > (2) if A : bSet and p and q of type Path A a b then p =3D q : Path A= a b > (judgemental form of UIP) > > Maybe (1) or (2) could be used instead of HTS (and we would remain in an= =20 > univalent > theory, where all types are fibrant) > > For testing this, one question is: can we define semi-simplicial types= =20 > in (1)? in (2)? > > Best regards, > Thierry > > > > On 20 Mar 2017, at 16:12, Matt Oliveri >= =20 > wrote: > > So the answer was yes, right? Problem solved? > > On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:=20 >> >> Just a thought=E2=80=A6 Can we devise a version of the HTS where exact e= quality=20 >> types are not available for the universes such that, even with the exact= =20 >> equality, HTS would remain a univalent theory.=20 >> >> Maybe only some types should be equipped with the exact equality and thi= s=20 >> should be a special quality of types.=20 >> >> Vladimir.=20 >> >> PS If there are higher inductive types then the exact equality should no= t=20 >> be available for them either. >> > > --=20 > You received this message because you are subscribed to the Google Groups= =20 > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= =20 > email to HomotopyTypeThe...@googlegroups.com . > For more options, visit https://groups.google.com/d/optout. > > > > --=20 > You received this message because you are subscribed to the Google Groups= =20 > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= =20 > email to HomotopyTypeThe...@googlegroups.com . > For more options, visit https://groups.google.com/d/optout. > > ------=_Part_227_1121601362.1490268163823 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Thanks.

I agree that with the sSet option, with an = equality reflection rule, it would be infeasible to check judgments without= extra stuff from outside the type theory proper. But what's wrong with= that? We add extra stuff anyway, like type classes, proof scripts, and imp= licit arguments. To me, it seems that the practical concern of checking the= truth of judgments does not need to be solved by the design of the core ty= pe theory. Indeed, it seems like better separation of concerns *not* to sol= ve it there.

Anyway, my understanding of bSet, from what Thierry Coq= uand said, is that it'd be a more OTT-like version of sSet, which is mo= re ETT-like. So instead of paths between bSets being reflectable to judgmen= tal equalities, they would be "strict propositions" (sProp), whos= e elements are not only all (typally) equal, but they also have no computat= ional content. So any "transport" across a strict equality reduce= s away, as long as it doesn't change the type. (It doesn't have to = be (judgmentally equal to) reflexivity.)

I figure the idea is that b= Set should be able to do everything sSet can, just with extra computational= ly-irrelevant transports thrown in to appease a decidable type checker.
=
I don't actually see how either of these universes would help defin= e semi-simplicial types. I didn't realize that was the goal here. I tho= ught we were just trying to make set-level math more convenient.

---= --------

Though I haven't given it a serious thinking-about, I f= igured that stuff with cohesion would be a good way to make semi-simplicial= types definable, without adding non-fibrant types. (https://homotopytypeth= eory.org/2015/09/25/realcohesion/) It sounded like cohesion gives you a set= -level view of non-hsets, so I figured you should be able to use strict equ= ality in the construction of non-hsets that way.

I suppose strict se= ts and cohesion can be combined. A set-level view of things should yield on= ly strict sets, not arbitrary hsets. (I guess that requires a whole hierarc= hy of strict set universes. But unlike HTS, they're all "included&= quot; in the univalent universes, not the other way around.)

On Wedn= esday, March 22, 2017 at 5:01:16 PM UTC-4, v v wrote:
1. As Thierry po= inted out previously, the problem with sSet is that if we postulate that na= t:sSet, then for any (small) type T, the function type T -> nat is in sS= et, e.g. nat -> nat is in sSet.

Since it is possible = to construct two elements of nat -> nat the equality between which is an= undecidable proposition, it implies that the definitional equality in any = sufficiently advanced type system with sSet and nat:sSet is undecidable.

That means that witnesses, in some language, of defi= nitional equality need to be carried around and therefore the design of a p= roof assistant where the proof term is the proof is not possible in this sy= stem.

2. It is not so clear what would happen with= only bSet and nat:bSet.=C2=A0

Vladimir.





On Mar 22, 2017, at 5:49 PM, Thierry Coquand <= Thier= ...@cse.gu.se> wrote:


If my note was correct, it describes in the cubical set model two univ= alent universes
(subpresheaf of the first universe) =C2=A0that satisfy

=C2=A0(1) =C2=A0 if =C2=A0 A : sSet =C2=A0 =C2=A0and =C2=A0 p : Path A= a b =C2=A0 then =C2=A0 a =3D b : A =C2=A0and p is the constant path a
(equality reflection rule)

=C2=A0(2) =C2=A0 if A : bSet and p and q of type Path A a b =C2=A0 the= n p =3D q : Path A a b
(judgemental form of UIP)

=C2=A0Maybe (1) or (2) could be used instead of HTS (and we would rema= in in an univalent
theory, where all types are fibrant)

=C2=A0For testing this, one question is: =C2=A0can we define semi-simp= licial types in (1)? in (2)?

=C2=A0Best regards,
=C2=A0Thierry



On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com> wrote:<= /div>
So the answer was yes, right? Problem solved?

On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:
Just a thought=E2=80=A6 Can we devise a version of the HTS where exact equa= lity types are not available for the universes such that, even with the exa= ct equality, HTS would remain a univalent theory.

Maybe only some types should be equipped with the exact equality and this s= hould be a special quality of types.

Vladimir.

PS If there are higher inductive types then the exact equality should not b= e available for them either.

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


--
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+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/= d/optout.
------=_Part_227_1121601362.1490268163823-- ------=_Part_226_372047895.1490268163823--