From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.46.0.218 with SMTP id e87mr4506759lji.5.1468882874568;
        Mon, 18 Jul 2016 16:01:14 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.31.6 with SMTP id f6ls1845652wmf.11.gmail; Mon, 18 Jul 2016
 16:01:14 -0700 (PDT)
X-Received: by 10.194.95.133 with SMTP id dk5mr604491wjb.4.1468882874075;
        Mon, 18 Jul 2016 16:01:14 -0700 (PDT)
Return-Path: <andrew....@gmail.com>
Received: from mail-lf0-x22f.google.com (mail-lf0-x22f.google.com. [2a00:1450:4010:c07::22f])
        by gmr-mx.google.com with ESMTPS id v14si760588wmf.0.2016.07.18.16.01.14
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 18 Jul 2016 16:01:14 -0700 (PDT)
Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::22f as permitted sender) client-ip=2a00:1450:4010:c07::22f;
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::22f as permitted sender) smtp.mailfrom=andrew....@gmail.com;
       dmarc=pass (p=NONE dis=NONE) header.from=gmail.com
Received: by mail-lf0-x22f.google.com with SMTP id b199so821062lfe.0
        for <HomotopyT...@googlegroups.com>; Mon, 18 Jul 2016 16:01:14 -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=04JWcbIzSxdZvjnXRtZkKBJB39Uo8ixpgecBhE23oVo=;
        b=o075A2mRx+XL7kXuhfg076l8/3JhVxLJwscOeqJUYy3JCQN2+lh+37DfiDubvS3n4T
         FdRmFEnM1LztfQRgpnJTvtJRfYp808JzunucBCHI5Xa4MhCoD7sIKOrNqSAWZc17PDLt
         xA0eYD9oRaEoXO7Vz6Qa3u9XV9CVnyIoU2kNLFcgsHC2hO0cgY/+Z7GJz/8NhF/MKrcL
         s8tcSXucrvwUx0Y3UvQ+n/8tm7Be7niDo+AXmNlUuGo6pON1Kqt2XDHag3BE9IMNuoy3
         YxLmvCPv4PaoUZOEt1ATl7g2mGQM7Qn6IQIDHeIp5HcBVvgxSi4APNxtZN4y3daiA1De
         cTeA==
X-Gm-Message-State: ALyK8tKic0Z6zWfvZExvhN9EynAtaKqTCCRBj68FofgJUlkzM3g6omBmqjHs9iZhMUrTAyq4CK1EGQeBRcdowA==
X-Received: by 10.25.151.132 with SMTP id z126mr14011321lfd.18.1468882873873;
 Mon, 18 Jul 2016 16:01:13 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.25.83.143 with HTTP; Mon, 18 Jul 2016 16:01:12 -0700 (PDT)
In-Reply-To: <CAOvivQw15pOvi9wzWFpB2WcwmgxB=uw-826xNmxUck57VagEQA@mail.gmail.com>
References: <b8aa1ee7-80a9-497b-916b-8b31d6eb76b3@googlegroups.com>
 <CAOvivQyZzdyhFFPfqkH4W+Z--78t0LEVWtthLhCpDxUkJNUrMQ@mail.gmail.com>
 <CABcT7WC2-rQ6uC+JJ1=FJSBYxWqDwWvQQtVP_-GvzEzft9C76g@mail.gmail.com>
 <CAOvivQy44FvN_bVD+nby8t0BnnTYf38dR5=s31_Yv_VsDOzLCA@mail.gmail.com>
 <CABcT7WAJDCOdxCj6YKz3vQd0J4ciS6K=Nk6+dxxnNF72pG5s=A@mail.gmail.com> <CAOvivQw15pOvi9wzWFpB2WcwmgxB=uw-826xNmxUck57VagEQA@mail.gmail.com>
From: Andrew Polonsky <andrew....@gmail.com>
Date: Tue, 19 Jul 2016 01:01:12 +0200
Message-ID: <CABcT7WCxdHSuWdHc+5DwO98ovHx_-9bszE=kOJuuDPg5ZfyZxQ@mail.gmail.com>
Subject: Re: [HoTT] Different notions of equality; terminology
To: Michael Shulman <shu...@sandiego.edu>
Cc: Homotopy Type Theory <HomotopyT...@googlegroups.com>
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.
>
> "Predicate/formula/thing-you-can-prove-or-inhabit" is a long-winded
> way of saying "type".

However, that distinction was present before types.  It is indeed
illogical to call "typal" something which was there before types were
invented.

>> 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.
>
> Only if you are willing to redefine the word "definition".

I am quite happy with it as is.

Andrew