From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a19:c515:: with SMTP id w21mr11240522lfe.186.1588593984594; Mon, 04 May 2020 05:06:24 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:3208:: with SMTP id y8ls2413294ljy.6.gmail; Mon, 04 May 2020 05:06:23 -0700 (PDT) X-Received: by 2002:a2e:9f13:: with SMTP id u19mr10305498ljk.42.1588593983220; Mon, 04 May 2020 05:06:23 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588593983; cv=none; d=google.com; s=arc-20160816; b=e6oX0e15eA+DX12qBc/Gq9uakXQs0/xJ+yjg8H723rEQedEFXWtD/V5o3fWpzDaRw8 9ATKHN9zIAuOmlOCHXmr74ZUbAmiozJ85kBYrJgx9STtIaQUaGW6p7yKtQiOHPr+LLhe uYKHZ0DxCsRe01mRCuIxkvuqxuX8HFVEUT3zgq44BuX70xDUZLE8HY2i+kqwUeP6f80y sk7vuJfIyAPImMLnnxhud8gBmff6yZb/EwTbHOeLBedayBgYnTSEwYxbCafMGyhKknhi MLD4K/l+AcuU1q70zAtIxOPUJZocA3bWaC6WAow+P1C4U9ZcvoI91Q0TGm15fgN+sJKG Vy0A== 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=KcPC2Wk07KF1VT+r4a/meGPNnmkyMChx1jfdwGY4hp0=; b=sOtPYrFVwLoTezxTmsSt3VXBRncDYIkr1lv8SLzMBrOi/9sKc3b8xSpDHQYQoYf0Fy ODzXgv2MD3bhLInszBsKNsTK3MGEOWeqQ3ai7sbamlO7b4ele0bK43nBiP6DPXP1sgdi 8k2H464LfYeOwhbsNOQyOwTfLAZ95GItJ0XPDvxM3AeXFh8/i/5Pk3Y1LIk5c9QCRZmn 9UWFfuyw5YgTyng+wnQdaltSX2YMMdgDsR/zbimKcYKNGFz7WXyQ1jdVYo18W8Eg0Eal tsPB6ggkqh/qXskPop/U4s+uXFzqEU4HxcKQhGSb+dW+V9inwq0kCdgQZ1IfYobfslTh Gm1g== 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: 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 d19si753113lji.3.2020.05.04.05.06.23 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 05:06:23 -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 49G1mF2Jx9z43p2; Mon, 4 May 2020 14:06:21 +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 044C6rk7009740; Mon, 4 May 2020 14:06:53 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id AB9FDC0061; Mon, 4 May 2020 14:06:20 +0200 (CEST) Date: Mon, 4 May 2020 14:06:20 +0200 From: Thomas Streicher To: Thorsten Altenkirch Cc: "homotopyt...@googlegroups.com" Subject: Re: [HoTT] "Identifications" ? Message-ID: <20200504120620.GA14623@mathematik.tu-darmstadt.de> References: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) Hi Thorsten, > This is really different in the respective topos models as eg simplicial > sets or already the topos of reflexive graphs as exemplified by N. Kraus's > puzzling counterexample. > > What puzzling counterexample is this? I learnt it from Nicolai when he gave a little talk at CSL 2017 when given a prize for his thesis. The counterexample or rather my appreciation of it I have made a little note on which I have put for convenience at https://www.mathematik.tu-darmstadt.de/~streicher/kraus.pdf The point is that interpreting HoTT in sSet is very different from the traditional interpretation of logic in sSet. The same happens already the topos of reflexive graphs. Propositions are connected reflexive graphs and thee are very man nonisomorphic such guys but HoTT identifies them all. But this has nothing to do with HoTT per se. For example you can interpret HOL in assemblies in two very different ways once `a la topos (proof irrelevant) and once `a la model of TT (proof relevant). In mathematics equality is a very relative notion. But one may perform quotients to reconcile them... Thomas