From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:a2e:b8c9:: with SMTP id s9mr9740834ljp.100.1589182416541;
        Mon, 11 May 2020 00:33:36 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:ac2:5de8:: with SMTP id z8ls1656126lfq.4.gmail; Mon, 11 May
 2020 00:33:34 -0700 (PDT)
X-Received: by 2002:a19:f70f:: with SMTP id z15mr9889103lfe.53.1589182414896;
        Mon, 11 May 2020 00:33:34 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1589182414; cv=none;
        d=google.com; s=arc-20160816;
        b=DWZ3jZWMsj9LqLwHGM3vfauSLRIwtPxfxnCteUTpY2ROpRrJ5zIt30ExdmIlttg+mG
         aI7Dl2nVX8JFHDDMVEJYFrNRNn/ZrIIcnJgGHsUDZhY7YDF/THMh21dVkrAvYBi+sk/m
         huYYZsUHbvkptQlUc1kY9ssNvxmQcLJ/tCRxXrfhcxfHIdom19BXkEqHv2SpL7Lz4Ys1
         pI4dByuXYHRdlk0QpebtR8ZAKvmbNzm2MJgQQHL/wZHET8JlzjlpWchl9dXrLTyQYRNt
         fYTk7ZVHNayej3+zSnGQxItKx2EirY7cQKevQJKWQdM3b6yd6iv/0jjB0cjpo2Or5w6s
         gpBg==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816;
        h=user-agent:in-reply-to:content-disposition:mime-version:references
         :message-id:subject:cc:to:from:date;
        bh=0XnDzkBPEWkB2lLlSJNF8juvjAzIrEhW8Ehctt++vI4=;
        b=FqH0oZO+qcAV4i4vSqn7LxPKwrWz3d/eipE8p+JwFvMBy9n/wez+MVEPi5f7FxmIRw
         LTqLzxFqWHG2b4vid7HkPHPiXvCP9RTO+zkumISVMKAVmDHINV2Q0Bq4ngaV7e1fgr/T
         vRsPIbQBvMGH7WpgXhSDMmTKSYEPVoxZ3c0ZMqt+eaGiEY1/X3tFzTA9fk/gx+QHuFOm
         fUDn6M19DgzhljWUOj6BoCzfeJbvcFa9UUjWB2qsUg3WBdPNSeAST4JI16qh4H9MT1Cm
         IxtGpklqY9d3Ic9oBYJ/DgsMCs8JBbulgRnHKDVZTOhAxsuxUCMVuxnhjDTguqZRJe60
         2bqQ==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.252.150 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from mail-relay150.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de. [130.83.252.150])
        by gmr-mx.google.com with ESMTPS id c16si485625ljk.5.2020.05.11.00.33.34
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 11 May 2020 00:33:34 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.252.150 as permitted sender) client-ip=130.83.252.150;
Authentication-Results: gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.252.150 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21])
	(using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits))
	(Client CN "mail.mathematik.tu-darmstadt.de", Issuer "DFN-Verein Global Issuing CA" (verified OK))
	by mail-relay150.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 49LCNF3GZtz43rL;
	Mon, 11 May 2020 09:33:33 +0200 (CEST)
Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209])
	by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id 04B7YHVX005089;
	Mon, 11 May 2020 09:34:17 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 4B655C0055; Mon, 11 May 2020 09:33:32 +0200 (CEST)
Date: Mon, 11 May 2020 09:33:32 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= <joyal...@uqam.ca>
Cc: Ulrik Buchholtz <ulrikbu...@gmail.com>,
        Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Identity versus equality
Message-ID: <20200511073332.GA30513@mathematik.tu-darmstadt.de>
References: <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca>
 <CAFL+ZM-X6tkX+666LTkfPqG1ALeytO=5-7A1XUn8f5q8AdgNqA@mail.gmail.com>
 <20200508064039.GC21473@mathematik.tu-darmstadt.de>
 <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca>
 <20200509082829.GA8417@mathematik.tu-darmstadt.de>
 <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca>
 <20200509184313.GB28841@mathematik.tu-darmstadt.de>
 <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca>
 <e47e6263-d0eb-4882-ab07-e31483095bd4@googlegroups.com>
 <8C57894C7413F04A98DDF5629FEC90B1652F5753@Pli.gst.uqam.ca>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F5753@Pli.gst.uqam.ca>
User-Agent: Mutt/1.5.23 (2014-03-12)

Dear Andr"e,

the exo/endo distinction is different from external/internal. It is like
L in set theory ZF which does not allow one to prove consisteny of ZF.
(An aside: why do internal cats play such an important role in traditional
 topos theory and are evil in Hott?)

Thomas