From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:ac2:5f73:: with SMTP id c19mr11616335lfc.135.1589218051647;
        Mon, 11 May 2020 10:27:31 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:a05:6512:202e:: with SMTP id s14ls94013lfs.0.gmail; Mon, 11
 May 2020 10:27:30 -0700 (PDT)
X-Received: by 2002:ac2:55a6:: with SMTP id y6mr11716390lfg.14.1589218050192;
        Mon, 11 May 2020 10:27:30 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1589218050; cv=none;
        d=google.com; s=arc-20160816;
        b=yAGdwogbeSU5tvM17qA7d1GlDZVjW4saE708FCK2KF6iYMKiexO2KdhElhnp1KNkaE
         SineinpFMjoNQB1QPmUPS5XeK4CqSzF7LqQKjM3WV7c962qAhMRl1F7DtfNq2nk3+7zq
         6sYYq3eoSWZ25aAsb5Ojlv5AUNSccbwwWwR7JlhHgW4k6LOzTYWMdlEJKcxuPdoWn+DK
         dX1qzorzqcZ1ogdozH5JzbTgeSUnSWzBvDYq1wbD+z+MdbgJfUCt7ijuIWG2KfutGTPd
         XI9m6FDDkeydmzxJJDwY1WlrcKHFLl68yVBgbDMSUPLKt8ZXy59cTgkE7U3NpKmC4q8H
         JYPA==
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=o7r8xHIsbnoj6GUbZswdSba7l4XKsPkG90ByVu7lVE8=;
        b=HLPt8Xxf9rvVkwD2UQv8imgPeSWhJRvek6DDvzDoUT7VRnIzAVTD44f4rGX+Asy0K4
         1vf1pISeckLjUZRa3gp1WKvCMhhsmgAkpzzhTDTOPIqvk5FNQTwhRMXejNmKmvKeJzjF
         TMKOZ2NpbzIdRl4r36j5nXulprMEsU9QuLH0o4Au8dywN8DHNcNjP64vLXRztKuoysqP
         Yo00N2a96Y71vzAewTL1wUZRwbbaPYRA1SCsjqQYa+uYT47CFxAq8RFJDJ/jy9PlOB+1
         cJP+wF+rWZ0WvKlEl2U+i3E2xW4RVwhLZ3KT9GBS8/MyhJPr8Rm3EW8KD6zB/xoCGt8q
         RuhQ==
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.156.233 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from mail-relay232.hrz.tu-darmstadt.de (mail-relay233.hrz.tu-darmstadt.de. [130.83.156.233])
        by gmr-mx.google.com with ESMTPS id q9si589111lfo.4.2020.05.11.10.27.30
        for <homotopyt...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 11 May 2020 10:27:30 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 as permitted sender) client-ip=130.83.156.233;
Authentication-Results: gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 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-relay232.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 49LSYX5yK5z43qT;
	Mon, 11 May 2020 19:27:28 +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 04BHSEAS015181;
	Mon, 11 May 2020 19:28:14 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 2E9F9C0055; Mon, 11 May 2020 19:27:28 +0200 (CEST)
Date: Mon, 11 May 2020 19:27:28 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Michael Shulman <shu...@sandiego.edu>
Cc: Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Identity versus equality
Message-ID: <20200511172728.GB16935@mathematik.tu-darmstadt.de>
References: <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>
 <20200511073332.GA30513@mathematik.tu-darmstadt.de>
 <8C57894C7413F04A98DDF5629FEC90B1652F5861@Pli.gst.uqam.ca>
 <0388695a1dfc717f9c5e458937dff760.squirrel@webmail.mathematik.tu-darmstadt.de>
 <CAOvivQxPWO-BqgG8EqOBPXrQUOtyiBK4yMaDq_pC+s4gOwpdoA@mail.gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <CAOvivQxPWO-BqgG8EqOBPXrQUOtyiBK4yMaDq_pC+s4gOwpdoA@mail.gmail.com>
User-Agent: Mutt/1.5.23 (2014-03-12)

> FWIW there is no trouble at all with "internal categories" in HoTT;

what I meant is that they are "evil" in the sense that they allow one
to speak about equality of objects
but if you do it in the simplicial sets model of HoTT then they are not quite
the same as categories internal to sSet
they are rather the unstraightenings of simplicially enriched cats
whose homobjects are all contractible

the contractible objects in sSet are much richer than the subobjects of 1

one should not forget that the logic of sSet when viewed at
homotopically is boolean whereas the traditional logic of sSet is not
at all

but I do understand that ordinary finite limit cats do live in sSet
via nerve

Thomas