From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.221.149 with SMTP id w21mr1471232lfi.25.1474478313498; Wed, 21 Sep 2016 10:18:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.33.195 with SMTP id h64ls1333898lji.24.gmail; Wed, 21 Sep 2016 10:18:32 -0700 (PDT) X-Received: by 10.25.43.76 with SMTP id r73mr3857111lfr.9.1474478312611; Wed, 21 Sep 2016 10:18:32 -0700 (PDT) Return-Path: Received: from mail-wm0-x22a.google.com (mail-wm0-x22a.google.com. [2a00:1450:400c:c09::22a]) by gmr-mx.google.com with ESMTPS id c13si2260316wme.3.2016.09.21.10.18.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 21 Sep 2016 10:18:32 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::22a as permitted sender) client-ip=2a00:1450:400c:c09::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::22a as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x22a.google.com with SMTP id w84so205003230wmg.1 for ; Wed, 21 Sep 2016 10:18:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=WR2gqsKByXmBndBItB5j26qfnqcSwGjeESiYFrwtdpo=; b=O8UtV2gdKwBzv4IE6Qobt8CnSkGvqo8WuzKJVbG2cYRD1a3E/GABrT+YdAvbQhfGz5 bnBkRR0ySyDLNmPFCx+VxqakP7HEufU9+OTqje/lDPd+Eb4ny3jz8xVI5Sibjb641OXa bTjQDbqd6IrLPt5i8M5cl6zATa4/LoEr43HaKHW1zWDIEJYfd0cvYLJOZ8wJ7tOxGyp9 GBrS6hXKT8Eq3gu155R4mrkkXC71oQiIJFuTfvjl3/HT0wEeEN+qhywV+Y6TQ/t7qsvn 4IIVcm5NbA66qN9v+l07eSSvHN8sEw1/NKZdBwC/laZpAkRGkLDuO49TsSi3Iha90E8F KHtg== X-Gm-Message-State: AE9vXwMg8KclW/k/maT63olE1nVuwd9DyjX+YBMSla7UOt/KgO2fNQRw682MGP1Pk117cw896o9d5kJtuxCUHw== X-Received: by 10.28.154.142 with SMTP id c136mr4554472wme.102.1474478312330; Wed, 21 Sep 2016 10:18:32 -0700 (PDT) MIME-Version: 1.0 Received: by 10.80.146.174 with HTTP; Wed, 21 Sep 2016 10:18:31 -0700 (PDT) In-Reply-To: References: From: Nicolai Kraus Date: Wed, 21 Sep 2016 18:18:31 +0100 Message-ID: Subject: Re: [HoTT] Semantic Success Condition for the definability of Semi-Simplicial Types To: Dimitris Tsementzis Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a114b23c009347f053d07bce3 --001a114b23c009347f053d07bce3 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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 the 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 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 theory 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 criteria (it would give you something with the expected structure, but it's not clear 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 type 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 thesis, 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 < > dtse...@princeton.edu> 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 types= 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 know 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 --001a114b23c009347f053d07bce3 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On W= ed, Sep 21, 2016 at 1:48 PM, Dimitris Tsementzis <dtse...@princeton.ed= u> wrote:
=

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 sh= ould be (up to equivalence). If you want, you can take some programming lan= guage and write a program P : Nat -> String such that P(n) is a syntacti= cal 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 theory= such that, for every numeral n, f(n) and P(n) are equivalent.=C2=A0
However, this would only cover the first poi= nt of Andrej's success criteria (it would give you something with the e= xpected structure, but it's not clear whether it will be useful).
<= br>An alternative way of phrasing what I said above would be: take the Alte= nkirch-Capriotti-K paper "Extending Homotopy Type Theory with Strict E= quality" which presents an HTS-style two-level system with a fibrant t= ype Nat of natural numbers and a non-fibrant type Nat_s of strict natural n= umbers. We have a family S : Nat_s -> U of semi-simplicial types. The ch= allenge here would be to define a family S' : Nat -> U which extend= s S. By the conservativity construction of Paolo Capriotti's forthcomin= g PhD thesis, this can then be translated back to types in "book HoTT&= quot;.
I think this could make it easi= er to see whether we can actually do something useful with such a construct= ion of semi-simplicial types.

Andrej, I am not sure about this:

On Wed, Sep 21, 2016 = at 2:40 PM, Andrej Bauer <andrej...@andrej.com> wrote:

O= n Wed, Sep 21, 2016 at 2:48 PM, Dimitris Tsementzis <<= a target=3D"_blank" href=3D"mailto:dtse...@princeton.edu">dtse...@princeton= .edu> wrote:
What I am asking for ideally is a formula P(x) of set theory that expresses=20 =E2=80=9Cx is a successful definition of semi-simplicial types in T=E2=80= =99=E2=80=99.

I think having such a formula co= unts as success.

If P(x) was a formula in type theory, then maybe, yes. I don't= really know 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
<= /div>

--001a114b23c009347f053d07bce3--