From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.66.83.136 with SMTP id q8mr31771379pay.38.1468932843221; Tue, 19 Jul 2016 05:54:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.14.35 with SMTP id c32ls10460468otc.46.gmail; Tue, 19 Jul 2016 05:54:02 -0700 (PDT) X-Received: by 10.157.16.10 with SMTP id h10mr25623515ote.3.1468932842630; Tue, 19 Jul 2016 05:54:02 -0700 (PDT) Return-Path: Received: from mail-it0-x236.google.com (mail-it0-x236.google.com. [2607:f8b0:4001:c0b::236]) by gmr-mx.google.com with ESMTPS id o70si970074ith.1.2016.07.19.05.54.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Jul 2016 05:54:02 -0700 (PDT) Received-SPF: pass (google.com: domain of virit...@gmail.com designates 2607:f8b0:4001:c0b::236 as permitted sender) client-ip=2607:f8b0:4001:c0b::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of virit...@gmail.com designates 2607:f8b0:4001:c0b::236 as permitted sender) smtp.mailfrom=virit...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-it0-x236.google.com with SMTP id f6so18573483ith.0 for ; Tue, 19 Jul 2016 05:54:02 -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; bh=fD56OOVabMK3zozKfjP9U/IdclhiGs4PAbuF9L0LaPs=; b=PLevRiLdEHv+nfSFpKe9Opi0pLpqtwuKihVb7BT+gBlqbWhU6o4y4JrTVxC+HrpwOM 0Y9H2MaaidbNsSp/5EXujadCVTJPIZmnX3vIVNY9ltcpmy4Myz0AF0a13/F7zt90MVDk YRaotDCKfpWEx8Ml2em5L5MYcMM79HehhPbQdTW38Yw2mCWKZxEx/NCz+he65P/mmcWd 9FPX2RcqtpQzc/UN0HRwLy7f0sukFtMueKwpFD30nDKk13WA3bqo1fTmr73vkT08GoDz tqfcT0y/gSjQU2AnKecUWQuULNFL/tjWyaNWgrpaVkwCtNQRxcRbGlbeVPIJys9LJzfF g/Ww== X-Gm-Message-State: ALyK8tJd/mC82V/QMJFTutwYTDjDQBMr/GuB06VhSrJeP3qMVj4on3W1HllFb1sB2Qzx49N8EPp0NWU7ik3/ow== X-Received: by 10.36.192.8 with SMTP id u8mr53535294itf.77.1468932842095; Tue, 19 Jul 2016 05:54:02 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.139.85 with HTTP; Tue, 19 Jul 2016 05:53:41 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Tue, 19 Jul 2016 09:53:41 -0300 Message-ID: Subject: Re: [HoTT] Different notions of equality; terminology To: Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 My apologies to everyone (except Andrew), who saw his replies to my messages without the originals. The problem was an email issue on my end. Below I summarize the content of my messages; this will be my last email on the subject. ~~ I have been advocating the term "typal equality" for what used to be called "propositional". It is less awkward than "type-level" or "type-theoretic", and conveys exactly what is meant, namely that the statement of equality *is a type*. I prefer it to "logical equality" because traditionally, "logic" has often referred only to the type theory of mere propositions, so "logical equality" has something of the same problem as "propositional equality". For the reasons given by Andrew, in most cases it suffices to simply say "equality". It only occasionally happens that we need to disambiguate what kind of equality we are talking about, and in that case I think it better to use a word that conveys *exactly* what the distinction is, rather than any historical or opinionable gloss on that distinction. (If this is "logical" equality, is the other one "illogical"?) Typal equality is indeed related to other kinds of equality that existed before type theory, but inside of type theory, what distinguishes it is precisely that it is a type (and inside of type theory, "predicate/formula/thing-you-can-prove-or-inhabit" is just a long-winded way of saying "type"). For the same reasons, I prefer "judgmental equality" because it conveys exactly what is meant in that case, namely that the statement of equality *is a judgment*. Maybe it doesn't have to be formulated as a judgment, but as far as I know in all cases it can our could be so, without changing the type theory materially. This possible slight inaccuracy seems to me to be preferable to the more serious problem with "definitional equality", namely that such a statement of equality is certainly not always 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. Associativity of addition of natural numbers is not true "by definition" unless you are willing to redefine the word "definition".