From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.27.205 with SMTP id b196mr108135wmb.0.1468881803113; Mon, 18 Jul 2016 15:43:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.215.39 with SMTP id o39ls89324lfg.25.gmail; Mon, 18 Jul 2016 15:43:22 -0700 (PDT) X-Received: by 10.25.22.155 with SMTP id 27mr5770366lfw.3.1468881802229; Mon, 18 Jul 2016 15:43:22 -0700 (PDT) Return-Path: Received: from mail-lf0-x230.google.com (mail-lf0-x230.google.com. [2a00:1450:4010:c07::230]) by gmr-mx.google.com with ESMTPS id r74si757577wme.3.2016.07.18.15.43.22 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Jul 2016 15:43:22 -0700 (PDT) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::230 as permitted sender) client-ip=2a00:1450:4010:c07::230; 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::230 as permitted sender) smtp.mailfrom=andrew....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x230.google.com with SMTP id g62so536865lfe.3 for ; Mon, 18 Jul 2016 15:43:22 -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=ccU4qVOft9OVHwh702/3Txqtp3qAIU+VxnfTyQmOAcM=; b=vizPUJ+PODgQoW5RGnplivFI3M922g72RbVkg3FQx44uC7j//JuRIfjhhoJ63GbQcZ UFSxOQYqf5hbZyvjEuMvdCBnoFHRpFo8je8G5ytgRQCLZ/m1cHqlnoUsjNxFtIHZbQE8 0Wk1xSNfyJd4HV/9A7cAvkNq8PqlR8L3XCiNNCjMDaN2zugND8A8FoQbiB/2UmuRGM1Y ttOrkPyKuvMd/UJv+PRhxQNWxDBNNhhKKUsQMTOdt662SqJoQJWz6G8mLAv3oHSZkUGK tV0znyrenB46ADF/9UTzlOROzet2fe2uJfXzMBVBaB+Db32dKhooZo70om7B8cF397N4 A4Ug== X-Gm-Message-State: ALyK8tI0uqG1Hj+rNiMjZE3zBmx6lj3pP/PxZAduwMGDmnx2VvyPGJsW/MvtmP8y2x8t9HFFNmH0GhH5uMl3cA== X-Received: by 10.46.0.97 with SMTP id 94mr15976992lja.60.1468881802029; Mon, 18 Jul 2016 15:43:22 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.83.143 with HTTP; Mon, 18 Jul 2016 15:43:21 -0700 (PDT) In-Reply-To: References: From: Andrew Polonsky Date: Tue, 19 Jul 2016 00:43:21 +0200 Message-ID: Subject: Re: [HoTT] Different notions of equality; terminology To: Michael Shulman Cc: Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 > case I think it better to use a word that conveys *exactly* what the > distinction is, The distinction is that it is the equality predicate/formula/thing-you-can-prove-or-inhabit. > I suppose judgmental equality doesn't have to be formulated as a > judgment, but as far as I know in all cases it can be so, without > changing the type theory materially. In principle, this should of course always be possible. But in practice, one often describes and implements the systems long before the conjecture above is verified. (If ever.) > It is not always, however, a > definition; for instance, in type theory with a reflection rule from > typal equality to judgmental, there is no sense in which a judgmental > equality obtained by that rule is a "definition" of one side in terms > of the other. In type theory with reflection rule, one can think of all equalities as "definitional", including those that appear in the hypothesis of the reflection rule. Andrew