From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.67.132 with SMTP id q126mr335279wma.22.1474494234651; Wed, 21 Sep 2016 14:43:54 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.198.67 with SMTP id w64ls2651799wmf.21.canary; Wed, 21 Sep 2016 14:43:53 -0700 (PDT) X-Received: by 10.28.55.205 with SMTP id e196mr343182wma.0.1474494233864; Wed, 21 Sep 2016 14:43:53 -0700 (PDT) Return-Path: Received: from mail-lf0-x241.google.com (mail-lf0-x241.google.com. [2a00:1450:4010:c07::241]) by gmr-mx.google.com with ESMTPS id e21si2770175wmc.2.2016.09.21.14.43.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 21 Sep 2016 14:43:53 -0700 (PDT) Received-SPF: neutral (google.com: 2a00:1450:4010:c07::241 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2a00:1450:4010:c07::241; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2a00:1450:4010:c07::241 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-lf0-x241.google.com with SMTP id l131so3084852lfl.0 for ; Wed, 21 Sep 2016 14:43:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=yDptG7SunWoAKpsJnQh/55kn9G5mLnquhLQVNZ0y8SM=; b=Xvb6kVhY4PRQlUiiRg8Rd0PnZFzQAv6bb9fWK0cH3uo5YfVD1hT8MsPvcF0Yx7sqG+ ImiZCCjvCyoL4elozoN0AFCMUJsv0iqps3p459ENqtwHZySv7AHBX7rJBCZ6ruLTamlX H7au2Lz+StDPGNHw2jCxx4wZapmso2hdJedP7RzU24/Qb/m8XP778rZjgnejHsO2H+nd wNvE/xt2XAOhPIR3XjAesjJ/lvf/sQEchxABoBOfOqr0kB6/Wt9QS8KTdncvE4fnN32B Dt2WiNIu6kaxToXmNEIPhG2iaOrP4SVIpVrMrT7IuInJWPTZKkFZBGT0bfQ13dhu6eG+ Avhg== X-Gm-Message-State: AE9vXwOEZsA7Jy76jUUAKM+9jxVEk4M2xtQ0JqvIKoMRNMaOnsJ3evdKGhK+oVSfzRob6m41 X-Received: by 10.25.24.91 with SMTP id o88mr16560703lfi.81.1474494232817; Wed, 21 Sep 2016 14:43:52 -0700 (PDT) Return-Path: Received: from mail-lf0-f54.google.com (mail-lf0-f54.google.com. [209.85.215.54]) by smtp.gmail.com with ESMTPSA id o84sm916457lfi.34.2016.09.21.14.43.51 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 21 Sep 2016 14:43:52 -0700 (PDT) Received: by mail-lf0-f54.google.com with SMTP id g62so52633759lfe.3 for ; Wed, 21 Sep 2016 14:43:51 -0700 (PDT) X-Received: by 10.25.153.76 with SMTP id b73mr9223512lfe.17.1474494231446; Wed, 21 Sep 2016 14:43:51 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Wed, 21 Sep 2016 14:43:30 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Wed, 21 Sep 2016 14:43:30 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Semantic Success Condition for the definability of Semi-Simplicial Types To: Dimitris Tsementzis Cc: Nicolai Kraus , Homotopy Type Theory , Andrej Bauer Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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. 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 toge= ther. > > The external criterion of success is that for some (many) semantic model = the > internal definition correspond to an established notion of semi-simplicia= l > objects. > > > Right, exactly. My question then is: in the case of the simplicial model = is > there a generally accepted way of expressing that the "internal definitio= n > corresponds to the established notion" without referring to some property > the internal definition satisfies (e.g. Nicolai=E2=80=99s way of making i= t precise > below)? > > the goal would be to write a function f : Nat -> U' (where U' is e.g. the > second universe) in type theory such that, for every numeral n, f(n) and > P(n) are equivalent. > > > 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 succe= ssful > definition? Obviously, one answer would be that F is the interpretation o= f 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 set > theory. > > 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) Re= edy > diagrams in semi-simplicial sets? > > (There is nothing constraining me to the simplicial model, but I would > imagine stating a semantic success condition for the simplicial model wou= ld > be the easier first step.) > > . I don't really know what exactly "a formula P in set theory=E2=80=9D me= ans. > > > 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 ab= out > F using formulas of set theory. So I was wondering whether such a formula > =CF=86(x) has been stated, for which we can say that > > exists x =CF=86(x) encodes that =E2=80=9Cthere is a definition of semi-si= mplicial types > in T=E2=80=9D > > As I said above, we could simply take =CF=86(x)=3D=E2=80=9Cx is the inte= rpretation of a > function f: N -> U=E2=80=99 in T that satisfies Nicolai=E2=80=99s conditi= on=E2=80=9D. But I=E2=80=99m asking > whether there is a =CF=86 that is (more) semantic in character. > > Best, > > Dimitris > > On Sep 21, 2016, at 13:18, Nicolai Kraus wrote: > > On Wed, Sep 21, 2016 at 1:48 PM, Dimitris Tsementzis > wrote: >> >> Is there an agreed-upon semantic success condition for the definition of >> semi-simplicial types? > > > I'm not sure whether the following is helpful because I won't refer to th= e > simplicial sets model. > Given a fixed numeral n, we know what the type of semi-simplicial types u= p > 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 can > 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 the= ory > 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 criter= ia > (it would give you something with the expected structure, but it's not cl= ear > whether it will be useful). > > 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 typ= e > 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 thes= is, > 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. > > Andrej, I am not sure about this: > > On Wed, Sep 21, 2016 at 2:40 PM, Andrej Bauer > wrote: >> >> >> On Wed, Sep 21, 2016 at 2:48 PM, Dimitris Tsementzis >> wrote: >>> >>> 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 type= s in T=E2=80=99=E2=80=99. >> >> >> I think having such a formula counts as success. > > > If P(x) was a formula in type theory, then maybe, yes. I don't really kno= w > 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. > > Best, > Nicolai > > > -- > 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.