From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.157.19.119 with SMTP id q52mr29971534otq.33.1468875784730;
        Mon, 18 Jul 2016 14:03:04 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.157.46.200 with SMTP id w66ls8296987ota.15.gmail; Mon, 18 Jul
 2016 14:03:04 -0700 (PDT)
X-Received: by 10.13.235.147 with SMTP id u141mr28383257ywe.27.1468875784137;
        Mon, 18 Jul 2016 14:03:04 -0700 (PDT)
Return-Path: <andrej...@andrej.com>
Received: from mail-qt0-x230.google.com (mail-qt0-x230.google.com. [2607:f8b0:400d:c0d::230])
        by gmr-mx.google.com with ESMTPS id w1si1481886yww.7.2016.07.18.14.03.03
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 18 Jul 2016 14:03:03 -0700 (PDT)
Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::230 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:400d:c0d::230;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com;
       spf=neutral (google.com: 2607:f8b0:400d:c0d::230 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com
Received: by mail-qt0-x230.google.com with SMTP id u25so98702054qtb.1
        for <HomotopyT...@googlegroups.com>; Mon, 18 Jul 2016 14:03:03 -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=bskbeqEC0VLw02Zv9jl7LRESQkfixMyMLZEreovNXtw=;
        b=BwrPmxfTPPylIUHSoJXKGeIxV3pT4Qxye5f3sjuDomWiuZjTEgl9ScbliBFGwf7Urz
         q1K1joN1k54qsc85rzOiwtIX3jzyUa2aWXonzMlg7EumarRYfH9dJa8pLndreltQ3QAj
         RbE/Jv5Xd6dhhN+0yqgInUElkNDjO4CbmdhQd6oJuxAB5kDg/4zKwW8RnWHCUAzyREJj
         weQ37YlYQiy9S8IVo3PJUukJGqi5XMEI5w3woPWQy8ZsT37cwH2Ly5eYIME3GvXYiYZU
         +ajGTpILbv9L6H52yUAVnlFMXB9hPfgb+dJDsogioJIuU4oCfZlBg1sxrjGfEMIcs5zM
         ilBA==
X-Gm-Message-State: ALyK8tJp5pjgjVnjSjCLVtDXtrgFy0GZlaIQTl3NUJbHfFWYGP0GrZ/556xf8VJmRrBvjP1UdCRspYlt/jusKg==
X-Received: by 10.200.50.20 with SMTP id x20mr54387506qta.71.1468875783732;
 Mon, 18 Jul 2016 14:03:03 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.55.31.38 with HTTP; Mon, 18 Jul 2016 14:03:03 -0700 (PDT)
In-Reply-To: <b8aa1ee7-80a9-497b-916b-8b31d6eb76b3@googlegroups.com>
References: <b8aa1ee7-80a9-497b-916b-8b31d6eb76b3@googlegroups.com>
From: Andrej Bauer <andrej...@andrej.com>
Date: Mon, 18 Jul 2016 23:03:03 +0200
Message-ID: <CAB0nkh01NMCY3Ri89OMLdzPuC_n_7F12QogYmh46dUfvdTPKuw@mail.gmail.com>
Subject: Re: [HoTT] Different notions of equality; terminology
To: Andrew Polonsky <andrew....@gmail.com>
Cc: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset=UTF-8

On Mon, Jul 18, 2016 at 10:45 PM, Andrew Polonsky
<andrew....@gmail.com> wrote:
> 1. DEFINITIONAL EQUALITY.

Judgmental equality seems a better phrase, no?