From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.253.198 with SMTP id n189mr7701951ywf.114.1474462109143; Wed, 21 Sep 2016 05:48:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.46.207 with SMTP id w73ls3978350ota.8.gmail; Wed, 21 Sep 2016 05:48:28 -0700 (PDT) X-Received: by 10.129.113.196 with SMTP id m187mr7073853ywc.106.1474462108616; Wed, 21 Sep 2016 05:48:28 -0700 (PDT) Return-Path: Received: from Princeton.EDU (ppa02.Princeton.EDU. [128.112.128.216]) by gmr-mx.google.com with ESMTPS id m82si2118087ywm.2.2016.09.21.05.48.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 21 Sep 2016 05:48:28 -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 csgsmtp203l.Princeton.EDU (csgsmtp203l.Princeton.EDU [140.180.223.156]) by ppa02.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id u8LCmSti020751 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Wed, 21 Sep 2016 08:48:28 -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 csgsmtp203l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id u8LCmRsB029876 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT) for ; Wed, 21 Sep 2016 08:48:27 -0400 From: Dimitris Tsementzis Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: Semantic Success Condition for the definability of Semi-Simplicial Types Message-Id: Date: Wed, 21 Sep 2016 08:48:27 -0400 To: Homotopy Type Theory Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-09-21_08:,, signatures=0 X-Proofpoint-Spam-Details: rule=quarantine_notspam policy=quarantine score=0 spamscore=0 suspectscore=2 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1609020000 definitions=main-1609210232 Is there an agreed-upon semantic success condition for the definition of se= mi-simplicial types? In particular, given the type theory T in the Simplicial Model paper, if X = is a type definable in T, then what must the interpretation of X in the sim= plicial model satisfy in order to be regarded a successful definition of se= mi-simplicial types?=20 (What I am asking for ideally is a formula P(x) of set theory that expresse= s =E2=80=9Cx is a successful definition of semi-simplicial types in T=E2=80= =99=E2=80=99.) Thank you, Dimitris