From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.46.85 with SMTP id s21mr7954283qta.49.1474494996363; Wed, 21 Sep 2016 14:56:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.65.36 with SMTP id x36ls1979ita.15.canary; Wed, 21 Sep 2016 14:56:35 -0700 (PDT) X-Received: by 10.107.134.134 with SMTP id q6mr19235648ioi.21.1474494995290; Wed, 21 Sep 2016 14:56:35 -0700 (PDT) Return-Path: Received: from Princeton.EDU (ppa02.Princeton.EDU. [128.112.128.216]) by gmr-mx.google.com with ESMTPS id p193si2710134ywe.6.2016.09.21.14.56.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 21 Sep 2016 14:56:35 -0700 (PDT) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.216 as permitted sender) client-ip=128.112.128.216; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.216 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp202l.Princeton.EDU (csgsmtp202l.Princeton.EDU [140.180.223.155]) by ppa02.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id u8LLuYwF001431 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Wed, 21 Sep 2016 17:56:34 -0400 Received: from 192.168.1.4 (pool-96-239-81-135.nycmny.east.verizon.net [96.239.81.135]) (authenticated authid=dtsement bits=0) by csgsmtp202l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id u8LLuXQn027449 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Wed, 21 Sep 2016 17:56:34 -0400 Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] Semantic Success Condition for the definability of Semi-Simplicial Types From: Dimitris Tsementzis In-Reply-To: Date: Wed, 21 Sep 2016 17:56:33 -0400 Content-Transfer-Encoding: quoted-printable Message-Id: <1F4005E2-600A-446A-8A22-B7AF95F834F0@princeton.edu> References: To: Michael Shulman , Homotopy Type Theory X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-09-21_12:,, signatures=0 X-Proofpoint-Spam-Details: rule=quarantine_notspam policy=quarantine score=0 spamscore=0 suspectscore=8 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1609020000 definitions=main-1609210397 Ah thanks! This is exactly what I was looking for. (In fact, a strong gener= ally accepted necessary condition is really what I should=E2=80=99ve asked = for.) Dimitris > On Sep 21, 2016, at 17:43, Michael Shulman wrote: >=20 > In any oo-topos C we can talk about a classifying object for > semisimplicial objects. This would be an object T together with, for > any object X, an equivalence (natural in X) between the > hom-oo-groupoid Hom_C(X,T) and the oo-groupoid of (small) > semisimplicial objects in the slice oo-category C/X. So one semantic > criterion for correctness would be that "the type of semisimplicial > types" interprets in any oo-topos (or, specifically in the oo-topos of > oo-groupoids, as presented by simplicial sets) to such a classifying > object. Other stronger conditions could also be given -- in > particular, this one says nothing about Reedy fibrancy -- but this > seems to me to be certainly a necessary condition for correctness. >=20 > On Wed, Sep 21, 2016 at 1:45 PM, Dimitris Tsementzis > wrote: >> Thanks a lot, Andrej and Nicolai. I=E2=80=99m merging your responses tog= ether. >>=20 >> The external criterion of success is that for some (many) semantic model= the >> internal definition correspond to an established notion of semi-simplici= al >> objects. >>=20 >>=20 >> Right, exactly. My question then is: in the case of the simplicial model= is >> there a generally accepted way of expressing that the "internal definiti= on >> corresponds to the established notion" without referring to some propert= y >> the internal definition satisfies (e.g. Nicolai=E2=80=99s way of making = it precise >> below)? >>=20 >> the goal would be to write a function f : Nat -> U' (where U' is e.g. th= e >> second universe) in type theory such that, for every numeral n, f(n) and >> P(n) are equivalent. >>=20 >>=20 >> In those terms, what I am asking for is this: If you interpret such an f >> into the simplicial model, then what would be something that we can say >> about the interpreted f (call it =E2=80=9CF") that would count as a succ= essful >> definition? Obviously, one answer would be that F is the interpretation = of a >> term f that satisfies the property you outlined. This would be a formula= in >> set theory too because we can take the syntax to have been encoded in se= t >> theory. >>=20 >> But I was wondering whether there is something that does not refer to a >> property that F would satisfy simply because it is the interpretation of >> something in the syntax. For example, something in terms of (external) R= eedy >> diagrams in semi-simplicial sets? >>=20 >> (There is nothing constraining me to the simplicial model, but I would >> imagine stating a semantic success condition for the simplicial model wo= uld >> be the easier first step.) >>=20 >> . I don't really know what exactly "a formula P in set theory=E2=80=9D m= eans. >>=20 >>=20 >> The simplicial model is constructed in set theory (in particular in ZFC+= 2 >> inaccessibles). A possible solution f: Nat -> U=E2=80=99 (to use Nicolai= =E2=80=99s notation) >> in the syntax will then be interpreted as something in set theory (in >> particular, a section F in some category). In that setting we can talk a= bout >> F using formulas of set theory. So I was wondering whether such a formul= a >> =CF=86(x) has been stated, for which we can say that >>=20 >> exists x =CF=86(x) encodes that =E2=80=9Cthere is a definition of semi-s= implicial types >> in T=E2=80=9D >>=20 >> As I said above, we could simply take =CF=86(x)=3D=E2=80=9Cx is the int= erpretation of a >> function f: N -> U=E2=80=99 in T that satisfies Nicolai=E2=80=99s condit= ion=E2=80=9D. But I=E2=80=99m asking >> whether there is a =CF=86 that is (more) semantic in character. >>=20 >> Best, >>=20 >> Dimitris >>=20 >> On Sep 21, 2016, at 13:18, Nicolai Kraus wrote: >>=20 >> On Wed, Sep 21, 2016 at 1:48 PM, Dimitris Tsementzis >> wrote: >>>=20 >>> Is there an agreed-upon semantic success condition for the definition o= f >>> semi-simplicial types? >>=20 >>=20 >> I'm not sure whether the following is helpful because I won't refer to t= he >> simplicial sets model. >> Given a fixed numeral n, we know what the type of semi-simplicial types = up >> to level n should be (up to equivalence). If you want, you can take some >> programming language and write a program P : Nat -> String such that P(n= ) is >> a syntactical representation of semi-simplicial types up to n (two years= ago >> or so, I wrote a Haskell script which generated Agda code). Then, you ca= n >> take this P to make the challenge precise: the goal would be to write a >> function f : Nat -> U' (where U' is e.g. the second universe) in type th= eory >> such that, for every numeral n, f(n) and P(n) are equivalent. >> However, this would only cover the first point of Andrej's success crite= ria >> (it would give you something with the expected structure, but it's not c= lear >> whether it will be useful). >>=20 >> An alternative way of phrasing what I said above would be: take the >> Altenkirch-Capriotti-K paper "Extending Homotopy Type Theory with Strict >> Equality" which presents an HTS-style two-level system with a fibrant ty= pe >> Nat of natural numbers and a non-fibrant type Nat_s of strict natural >> numbers. We have a family S : Nat_s -> U of semi-simplicial types. The >> challenge here would be to define a family S' : Nat -> U which extends S= . By >> the conservativity construction of Paolo Capriotti's forthcoming PhD the= sis, >> this can then be translated back to types in "book HoTT". >> I think this could make it easier to see whether we can actually do >> something useful with such a construction of semi-simplicial types. >>=20 >> Andrej, I am not sure about this: >>=20 >> On Wed, Sep 21, 2016 at 2:40 PM, Andrej Bauer >> wrote: >>>=20 >>>=20 >>> On Wed, Sep 21, 2016 at 2:48 PM, Dimitris Tsementzis >>> wrote: >>>>=20 >>>> What I am asking for ideally is a formula P(x) of set theory that >>>> expresses =E2=80=9Cx is a successful definition of semi-simplicial typ= es in T=E2=80=99=E2=80=99. >>>=20 >>>=20 >>> I think having such a formula counts as success. >>=20 >>=20 >> If P(x) was a formula in type theory, then maybe, yes. I don't really kn= ow >> what exactly "a formula P in set theory" means, but I don't think such a >> formula would solve the problem, given that we can say externally what >> semi-simplicial types ought to be. >>=20 >> Best, >> Nicolai >>=20 >>=20 >> -- >> 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.