From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.26.82 with SMTP id a79mr4796864pfa.8.1488248251214; Mon, 27 Feb 2017 18:17:31 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.241.9 with SMTP id c9ls2557390iti.5.canary-gmail; Mon, 27 Feb 2017 18:17:30 -0800 (PST) X-Received: by 10.99.126.69 with SMTP id o5mr6957483pgn.65.1488248250468; Mon, 27 Feb 2017 18:17:30 -0800 (PST) Return-Path: Received: from pps4.ias.edu (pps4.ias.edu. [192.16.204.92]) by gmr-mx.google.com with ESMTPS id d67si24851ywb.3.2017.02.27.18.17.30 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 27 Feb 2017 18:17:30 -0800 (PST) Received-SPF: pass (google.com: domain of vlad...@ias.edu designates 192.16.204.92 as permitted sender) client-ip=192.16.204.92; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of vlad...@ias.edu designates 192.16.204.92 as permitted sender) smtp.mailfrom=vlad...@ias.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=ias.edu Received: from pps.reinject (pps4.ias.edu [127.0.0.1]) by pps4.ias.edu (8.16.0.17/8.16.0.17) with ESMTPS id v1S2HPtA004329 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 27 Feb 2017 21:17:25 -0500 Received: from pps4.ias.edu (pps4.ias.edu [127.0.0.1]) by pps.reinject (8.16.0.16/8.16.0.16) with SMTP id v1S2HP2U004323; Mon, 27 Feb 2017 21:17:25 -0500 X-Proofpoint-Sentinel: stfjN6uyiYVX1DLnJCOFlx5ZI10yD1b91gTm7WR0MIVynnNTYWx0ZWRfX3IQ l73auM0AfZHD+7zzAjqViPLiQrqKm1LZpC7AWX/qzDBeZ7acguIjVE/19gy9CccY04eEmhR/ilTQ 4ZTk/cArpnt3vWAszw== Received: from imap.math.ias.edu (f5-bip.net.ias.edu [172.16.13.241]) by pps4.ias.edu with ESMTP id v1S2HPX4004322 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 27 Feb 2017 21:17:25 -0500 Received: from pool-96-248-86-80.cmdnnj.fios.verizon.net ([96.248.86.80] helo=vladimirs-mbp-2.home) by imap.math.ias.edu with esmtpsa (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.80.1) (envelope-from ) id 1ciXLx-0006n1-Jv; Mon, 27 Feb 2017 21:17:25 -0500 From: Vladimir Voevodsky Message-Id: <814709BF-E17F-4E1B-9676-C01B1673D6B5@ias.edu> Content-Type: multipart/alternative; boundary="Apple-Mail=_403FB953-01A1-49C4-A479-54040878E2F3" Mime-Version: 1.0 (Mac OS X Mail 10.2 \(3259\)) Subject: Re: [UniMath] [HoTT] about the HTS Date: Mon, 27 Feb 2017 21:17:25 -0500 In-Reply-To: <1806f2f9c6484a438935d6c2ed6d7fc2@cse.gu.se> Cc: "Prof. Vladimir Voevodsky" , "univalent-...@googlegroups.com" , homotopytypetheory To: Thierry Coquand 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> <1806f2f9c6484a438935d6c2ed6d7fc2@cse.gu.se> X-Mailer: Apple Mail (2.3259) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-02-28_01:,, signatures=0 X-Proofpoint-Spam-Reason: safe X-IAS-PPS-SPAM: NO X-Proofpoint-Spam-Details: rule=ias_safe policy=ias score=0 spamscore=0 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=donotscan adjust=0 reason=safe scancount=1 engine=8.0.1-1612050000 definitions=main-1702280017 X-IAS-PPS-PHISH: NO --Apple-Mail=_403FB953-01A1-49C4-A479-54040878E2F3 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 We also validate axiom K with the hSet, as far as I understand. BTW why do you call elements of bSet Bishop sets? > On Feb 27, 2017, at 1:58 PM, Thierry Coquand wrote= : >=20 >=20 > Exactly. >=20 > In my note, I consider three universes (all fibrant) >=20 > sProp=20 > sSet > bSet >=20 > sProp sub-presheaf of sSet sub-presheaf bSet sub-presheaf U >=20 > They correspond to 3 properties >=20 > G |- A sprop > G |- A sset > G |- A bset >=20 > that can be described semantically in a simple way. >=20 > For sprop and sset, to have a fibration structure is a property > and=20 >=20 > G |- A sset and fibrant >=20 > should correspond to the notion of covering space. >=20 > 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. >=20 > At least with bSet we validate axiom K and all developments that have > been done using this axiom. >=20 >=20 >=20 >=20 > From: Vladimir Voevodsky > > Sent: Monday, February 27, 2017 7:53 PM > To: Thierry Coquand > Cc: Prof. Vladimir Voevodsky; univalent-...@googlegroups.com ; homotopytypetheory > Subject: Re: [UniMath] [HoTT] about the HTS > =20 > 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 impli= es a is definitionally equal to b if a and b are elements of a strict set. >=20 > It is such a structure that would make many things very convenient.=20 >=20 > It is non- clear to, however, why typing would be decidable in such a sys= tem. >=20 > Vladimir. >=20 >=20 >=20 >=20 >> On Feb 27, 2017, at 1:50 PM, Vladimir Voevodsky > wrote: >>=20 >>=20 >>> On Feb 25, 2017, at 2:19 PM, Thierry Coquand > wrote: >>>=20 >>> =E2=80=9CBishop set=E2=80=9D which corresponds >>> to the fact that any two paths between the same end points are -judgmen= tally- equal. >>=20 >> This is not what I mean by a strict set. A strict set is a Bishop set wh= ere any two points connected by a path are judgmentally equal. >>=20 >>=20 >=20 > --=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 . --Apple-Mail=_403FB953-01A1-49C4-A479-54040878E2F3 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 We also validate a= xiom K with the hSet, as far as I understand.

BTW why do you call elements of bSet Bishop sets?


On Feb 27, 2017, at 1= :58 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:


Exactly.

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

 sProp 
 sSet
 bSet

 sProp sub-presheaf of sSe= t sub-presheaf bSet sub-presheaf U

 They correspond to 3 properties<= /div>

 G |- A sprop
 G |- A sset
 G |- A bset

that can be described semantic= ally in a simple way.

 F= or 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<= /div>
it shou= ld 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 u= sing this axiom.




From: Vladimir Voevodsky <v= lad...@ias.edu>
Sent: Monday, February 27, 2017 7:53 PM
To: <= /span>Thierry Coquand
Cc: Prof. Vladimir Voevodsky; univalent-...@googlegroups.com; homotopytypetheory<= br class=3D"">Subject: Re: [UniMath] [HoTT] about the HTS
&n= bsp;
BTW, even if the universe of strict sets is= not fibrant we can still have a judgement that something is a strict set a= nd 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.&= nbsp;

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

Vladimir.
<= div class=3D"">



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

<= br class=3D"">
On Feb 25, 2017, at 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:
<= br class=3D"Apple-interchange-newline">
 =E2=80=9C= Bishop set=E2=80=9D which corresponds
to the fact that any two paths between the same end points are -judgment= ally- equal.

T= his 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.



-- 
You received this message because you are subscrib= ed to the Google Groups "Homotopy Type Theory" group.
To unsubscr= ibe 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.

--Apple-Mail=_403FB953-01A1-49C4-A479-54040878E2F3--