From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.87.27 with SMTP id l27mr1971926ljb.28.1488221905407; Mon, 27 Feb 2017 10:58:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.22.92 with SMTP id 28ls475304ljw.54.gmail; Mon, 27 Feb 2017 10:58:24 -0800 (PST) X-Received: by 10.46.76.17 with SMTP id z17mr1978969lja.13.1488221903986; Mon, 27 Feb 2017 10:58:23 -0800 (PST) Return-Path: Received: from targaryen.ita.chalmers.se (targaryen.ita.chalmers.se. [129.16.226.133]) by gmr-mx.google.com with ESMTPS id v70si949009wmf.0.2017.02.27.10.58.23 (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Mon, 27 Feb 2017 10:58:23 -0800 (PST) Received-SPF: neutral (google.com: 129.16.226.133 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) client-ip=129.16.226.133; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 129.16.226.133 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) smtp.mailfrom=Thierry...@cse.gu.se Received: from tyrell.ita.chalmers.se (129.16.226.132) by targaryen.ita.chalmers.se (129.16.226.133) with Microsoft SMTP Server (TLS) id 15.1.396.30; Mon, 27 Feb 2017 19:58:22 +0100 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.0396.037; Mon, 27 Feb 2017 19:58:22 +0100 From: Thierry Coquand To: Vladimir Voevodsky CC: "univalent-...@googlegroups.com" , homotopytypetheory Subject: Re: [UniMath] [HoTT] about the HTS Thread-Topic: [UniMath] [HoTT] about the HTS Thread-Index: AQHSjePTXjyUspl4WUiKTqinTtS8xaF6CauAgAMeaICAAADwgIAAEN9U Date: Mon, 27 Feb 2017 18:58:22 +0000 Message-ID: <1806f2f9c6484a438935d6c2ed6d7fc2@cse.gu.se> References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> <12C1D5CB-D95A-4EC1-B5F9-C67F92685529@chalmers.se> <528245BE-80DB-4E94-A887-97D33AD30788@ias.edu>,<9803E33B-06CD-427D-8485-F817390ED527@ias.edu> In-Reply-To: <9803E33B-06CD-427D-8485-F817390ED527@ias.edu> Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [129.16.10.245] Content-Type: multipart/alternative; boundary="_000_1806f2f9c6484a438935d6c2ed6d7fc2cseguse_" MIME-Version: 1.0 --_000_1806f2f9c6484a438935d6c2ed6d7fc2cseguse_ Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Exactly. In my note, I consider three universes (all fibrant) sProp sSet bSet sProp sub-presheaf of sSet sub-presheaf bSet sub-presheaf U They correspond to 3 properties G |- A sprop G |- A sset G |- A bset that can be described semantically in a simple way. For sprop and sset, to have a fibration structure is a property and G |- A sset and fibrant should correspond to the notion of covering space. But sSet does not correspond to a decidable type system, while it should be the case that sProp and bSet corresponds to a decidable type system. At least with bSet we validate axiom K and all developments that have been done using this axiom. ________________________________ From: Vladimir Voevodsky Sent: Monday, February 27, 2017 7:53 PM To: Thierry Coquand Cc: Prof. Vladimir Voevodsky; univalent-...@googlegroups.com; homotopytypet= heory Subject: Re: [UniMath] [HoTT] about the HTS BTW, even if the universe of strict sets is not fibrant we can still have a= judgement that something is a strict set and the rule that a =3D b implies= a is definitionally equal to b if a and b are elements of a strict set. It is such a structure that would make many things very convenient. It is non- clear to, however, why typing would be decidable in such a syste= m. Vladimir. On Feb 27, 2017, at 1:50 PM, Vladimir Voevodsky > wrote: On Feb 25, 2017, at 2:19 PM, Thierry Coquand > wrote: "Bishop set" which corresponds to the fact that any two paths between the same end points are -judgmentall= y- equal. This is not what I mean by a strict set. A strict set is a Bishop set where= any two points connected by a path are judgmentally equal. --_000_1806f2f9c6484a438935d6c2ed6d7fc2cseguse_ Content-Type: text/html; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable


Exactly.


 In my note, I consider three universes (all fibrant)


 sProp 

 sSet

 bSet


 sProp sub-presheaf of sSet sub-presheaf bSet sub-presheaf U


 They correspond to 3 properties


 G |- A sprop

 G |- A sset

 G |- A bset


that can be described semantically in a simple way.


 For sprop and sset, to have a fib= ration structure is a property

and 


 G |- A sset and fibrant


should correspond to the notion of covering space.


 But sSet does not correspond to a decidable type system, while

it should be the case that sProp and bSet corresponds to a decidable

type system.


 At least with bSet we validate axiom K and all developments that h= ave

been done using this axiom.





From: Vladimir Voevodsky &l= t;vl...@ias.edu>
Sent: Monday, February 27, 2017 7:53 PM
To: Thierry Coquand
Cc: Prof. Vladimir Voevodsky; univalent-...@googlegroups.com; homoto= pytypetheory
Subject: Re: [UniMath] [HoTT] about the HTS
 
BTW, even if the universe of strict sets is not fibrant we can still h= ave a judgement that something is a strict set and the rule that a =3D b im= plies a is definitionally equal to b if a and b are elements of a strict se= t.

It is such a structure that would make many things very con= venient. 

It is non- clear to, however, why typing would be decidable= in such a system.

Vladimir.




On Feb 27, 2017, at 1:50 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:


On Feb 25, 2017, at 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote= :

 “Bishop set”= which corresponds
to the fact that any two paths between the same end points are -judgmentall= y- equal.

This is not what I mean by a strict set. A strict set is a = Bishop set where any two points connected by a path are judgmentally equal.=



--_000_1806f2f9c6484a438935d6c2ed6d7fc2cseguse_--