From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.20.41 with SMTP id h38mr2723057oth.76.1474465258292; Wed, 21 Sep 2016 06:40:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.18.201 with SMTP id g67ls1880345otg.26.gmail; Wed, 21 Sep 2016 06:40:57 -0700 (PDT) X-Received: by 10.157.63.161 with SMTP id r30mr2553135otc.24.1474465257764; Wed, 21 Sep 2016 06:40:57 -0700 (PDT) Return-Path: Received: from mail-qk0-x229.google.com (mail-qk0-x229.google.com. [2607:f8b0:400d:c09::229]) by gmr-mx.google.com with ESMTPS id d206si2497847ywh.3.2016.09.21.06.40.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 21 Sep 2016 06:40:57 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c09::229 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:400d:c09::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:400d:c09::229 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-qk0-x229.google.com with SMTP id t7so45395975qkh.2 for ; Wed, 21 Sep 2016 06:40:57 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=sGUKKRJvupugvmEj3jaIPvSk9xQZfDaJUPC4ZBww7nM=; b=KfnuREILQd0KPOqEPc4Q7pklMz4Rf6qLXJutXzP/Zk9jeGQ3TVxOTHf04e+HRph9dH WlPK4P05ppvRCEtdTxw7FtvdmBGekttOxc+ljXp1TZRX1a/6vr9dh7l+Q6qxWjVd2TES ABJTfMm4rri2TyRcfP07Oq5ROtc1f9YhkoH0FHLkCozD+tnDadB7P/i/iT/p14hmUwUZ kr7AsnKENZxm8vnD/q5U5fYaseuXfMGHAsFVfSLUmuceJ1cbwRw01L51PzTZ2y4B0jGR s9BlI7owX+ed7q5nmFyoSzp/j0HEUAcuHeVxKnfX3EuqEp7gC4bXf/NvvGxSOMbv7fW9 XTmw== X-Gm-Message-State: AE9vXwOGyLEvSngCmBsfTnIuU20krIbp4/nfzhrsF3vSPQl/JcaCsKq4stqYPDk6gMu8pC0RLzwR+p70ah2dGg== X-Received: by 10.55.214.220 with SMTP id p89mr39065439qkl.162.1474465257236; Wed, 21 Sep 2016 06:40:57 -0700 (PDT) MIME-Version: 1.0 Received: by 10.55.53.70 with HTTP; Wed, 21 Sep 2016 06:40:56 -0700 (PDT) In-Reply-To: References: From: Andrej Bauer Date: Wed, 21 Sep 2016 15:40:56 +0200 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=001a1147a348e474de053d04b1bd --001a1147a348e474de053d04b1bd Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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 types = in T=E2=80=99=E2=80=99. I think having such a formula counts as success. A good definition of semi-simplicial types should satisfying the following criteria: 1. The semi-simplicial types have the expected structure, and 2. It is possible to actually do something useful with them, inside type theory. For instance, how do we know that the usual HIT definition of the circle is the right one? I was not really convinced until Mike calculated its fundamental group to be Z. This goes under "the object has the expected structure". The external criterion of success is that for some (many) semantic model the internal definition correspond to an established notion of semi-simplicial objects. With kind regards, Andrej --001a1147a348e474de053d04b1bd Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

= On Wed, Sep 21, 2016 at 2:48 PM, Dimitris Tsementzis <= dtse...@princeto= n.edu> wrote:
What I am ask= ing for ideally is a formula P(x) of set theory that expresses =E2=80=9Cx i= s a successful definition of semi-simplicial types in T=E2=80=99=E2=80=99.<= /blockquote>

I think having such a formula counts as success.

A good def= inition of semi-simplicial types should satisfying the following criteria:<= /div>

1. The= semi-simplicial types have the expected structure, and
2. It is possible to actually do something useful with them, i= nside type theory.

For instance, how do we know that the usual HIT definition of = the circle is the right one? I was not really convinced until Mike calculat= ed its fundamental group to be Z. This goes under "the object has the = expected structure".

The external criterion of success is that for some (man= y) semantic model the internal definition correspond to an established noti= on of semi-simplicial objects.

With kind regards,

Andrej
--001a1147a348e474de053d04b1bd--