From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.22.155 with SMTP id 27mr5731778lfw.3.1468876404481; Mon, 18 Jul 2016 14:13:24 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.26.76 with SMTP id a73ls1367627wma.15.gmail; Mon, 18 Jul 2016 14:13:23 -0700 (PDT) X-Received: by 10.194.222.162 with SMTP id qn2mr566383wjc.6.1468876403771; Mon, 18 Jul 2016 14:13:23 -0700 (PDT) Return-Path: Received: from mail-lf0-x229.google.com (mail-lf0-x229.google.com. [2a00:1450:4010:c07::229]) by gmr-mx.google.com with ESMTPS id o85si842665wme.0.2016.07.18.14.13.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Jul 2016 14:13:23 -0700 (PDT) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::229 as permitted sender) client-ip=2a00:1450:4010:c07::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::229 as permitted sender) smtp.mailfrom=andrew....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x229.google.com with SMTP id b199so140684209lfe.0 for ; Mon, 18 Jul 2016 14:13:23 -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=sWqTqqfJVd4OeJPGTaBv7GvBYxja2+hwpyJFELwY/g8=; b=wqn9HjJjzMeTrAlMzuX8aK4d3A7skjaJmrmQVG7VooViI/gsg41biGY0dw7P2v1/Vn 0jmYXB3K7Uhd/2vwArz82E/xzR5OCTZHWt7dHWtSQzVkdYEmw9eHYAPDl4+hI6RQQMpH e00AH2Mg8JyIVf7MAi0MonEDGrr8ovfYyau6T7OiBBvxX2IunsZL+/9pJ2MVfyFB4X4D tbaxIvca1I2s+p5HAoSlbJZ0NiovtjIEIP70z+ApLn8xzHwjHXv2im6jweV87k9A7W2z IQp9jVrPN8W2+umqx6c6RP5TWtSmyh6NBEL2N3pqmWhBM3nTMWuTxsAemJYFtLWElP8X CpDw== X-Gm-Message-State: ALyK8tJnRlR+LFgGzWeElpo2NgXQ/yJgDUpBxfqijieTzF3zI9wlCFmFqFqQ++B8Va3ohxRwKejOpYe7xsiazQ== X-Received: by 10.46.9.141 with SMTP id 135mr6493398ljj.5.1468876403550; Mon, 18 Jul 2016 14:13:23 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.83.143 with HTTP; Mon, 18 Jul 2016 14:13:22 -0700 (PDT) In-Reply-To: References: From: Andrew Polonsky Date: Mon, 18 Jul 2016 23:13:22 +0200 Message-ID: Subject: Re: [HoTT] Different notions of equality; terminology To: Vladimir Voevodsky Cc: Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 On Mon, Jul 18, 2016 at 11:05 PM, Vladimir Voevodsky wrote: > Finally, Voevodsky currently distinguishes between "substitutive" and > "transportational" equalities. But in his system, both concepts are of the > "logical" kind. The effect is therefore to promote "strict" equality to the > logical level; so one can reason about it in the object logic, while > retaining other properties like the conversion rule. > > > I am not sure what you mean by this. In fact, I emphasized that the only > substitutional equality in MLTTs is the definitional equality that can not > be postulated or proved, only checked. I mean that your system with two equalities promotes strict equality of MLTT from definitional to the logical level. It remains "substitutional" but can be asserted in context. It would be nice to have a few simple demonstrations of the uses of this, without getting into simplicial types. Andrew