From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:600c:21d6:: with SMTP id x22mr9974393wmj.95.1588846175525; Thu, 07 May 2020 03:09:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:7d92:: with SMTP id y140ls7171197wmc.2.gmail; Thu, 07 May 2020 03:09:33 -0700 (PDT) X-Received: by 2002:a7b:cb53:: with SMTP id v19mr9290095wmj.166.1588846173102; Thu, 07 May 2020 03:09:33 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588846173; cv=none; d=google.com; s=arc-20160816; b=Q9Gm59W1XNi33BdaGqPETX/Mc1X2bswRdSMy8ZD2FR+J58Tg12kr5SL7rA4rox7O6E cJARHI+sn3LmB9GC3UmWwtkqjyC29+IMvGxk4Y5t1XV4cvg37D3c+uOH20/yEPwmmNB2 PS+56g8uKSZ9mE9Zl2K8WOX6L6I6tdrLQ1K3kHX5O3IhK/5BKB/hClYh5Futnlu6ZUGU mmmCmqxLbxBexdVss0p/GElsHgHbQa3mDtQqT+eefKrQw2ng504Yy8wwFZXNTR1YjWCm yhJ++UkQkHrFweXfWjn3RPSoNNBZtNBdz9tUCeCtK6R9zze6FUiwuefY/t1zmGTKD+Dm iRsQ== 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=ChelB1jHUzRdQlKkMZRBnawSXhVtCZlj5GoSV37qWdc=; b=FooCcmrePO3g00+GXQPMgfdz+94H2L3sIKdCmb3RkU9JnfwaxVSNHhPpaSdIq7czo/ M1yb0H3cnc1Rb+znR0QVe1w6rLIRsz2X99SXGDr4lf9UKYKhbwZLBvmVry7seYbA/C+Y I0GLzFV75KOFPnrO7YeMrWbnaXhCQ5lNVeW/MIUfeBSKzcw7gqnoYioqnNFwJam3vPK0 9qUFBhNH3q91fD+qB9JYrwV/U87390N9VtbUZ7bQ48q6+Z6yJ58rLOU/ZBezxKrCu1aF 5YBCpncy1oJ3GhKQqX51w6mYd40eagrmZ2MQBTfcgM+SPPvDfFTGmvFSQjjJ8Hkxae53 N9Dg== 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 m4si315365wrn.5.2020.05.07.03.09.33 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Thu, 07 May 2020 03:09:33 -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 49Hq232WJNz43q8; Thu, 7 May 2020 12:09:31 +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 047AA8BX005700; Thu, 7 May 2020 12:10:08 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 3A06FC0061; Thu, 7 May 2020 12:09:30 +0200 (CEST) Date: Thu, 7 May 2020 12:09:30 +0200 From: Thomas Streicher To: Thorsten Altenkirch Cc: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Subject: Re: [HoTT] Identity versus equality Message-ID: <20200507100930.GA9390@mathematik.tu-darmstadt.de> References: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> <05375057-883F-4487-8919-2579F5771AFC@cmu.edu> <952EF822-FD92-404C-A279-89502238BCDC@nottingham.ac.uk> <8C57894C7413F04A98DDF5629FEC90B1652F526C@Pli.gst.uqam.ca> <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> User-Agent: Mutt/1.5.23 (2014-03-12) In my eyes the reason for the confusion (or rather different views) arises from the different situation we have in syntax and in semantics. In syntax the "real thing" is propositional equality and judgemental equality is just an auxiliary notion. In mathematics it's the well known difference between equality requiring proof (e.g. by induction) and checking equality by mere symbolic computation. The latter is just a technical device and not something conceptually basic. The situation is very different in models (be they simplicial, cubical or whatever). There judgemental equality gets interpreted as equality of morphism and propositional equality gets interpreted as being homotopic. Since the outer level of 2-level type theory is extensional there is no judgemental equality (as in extensional TT). This latter view is the view of people working in higher dimensional category theory as e.g. you, Andr'e when you are not posting on the list but write your beautiful texts on quasicats, Lurie or Cisinski (and quite a few others). In these works people are not afraid of refering to equality of objects, e.g. when defining the infinite dimensional analogue of Grothendieck fibrations. And this for very good reasons since there are important parts of category theory where equality of objects does play a role (typically Grothendieck fibrations). Fibered cats also often don't allow one to speak about equality of objects in the base but it is there. This is very clearly expressed so in the last paragraph of B'enabou's JSL article of fibered cats from 1985. I think this applies equally well to infinity cats mutatis mutandis. This phenomenon is not new. Consider good old topos theory. There are things expressible in the internal logic of a topos and there are things which can't be expressed in it as e.g. well pointedness or every epi splits. The first holds vacuously when (misleadingly) expressed in the internal language of a topos and the second amounts to so called internal AC (which amounts to epis being preserved by arbitrary exponentiation). This doesn't mean at all that internal language is a bad thing. It just means that that it has its limitations... Analogously, so in infinity category theory. Let us assume for a moment that HoTT were the internal language of infinity toposes (which I consider as problematic). There are many things which can be expressed in the internal language but not everything as e.g. being a Grothendieck fibration or being a mono... I mean these are facts which one has to accept. One might find them deplorable or a good thing but one has to accept them... One of the reasons why I do respect Voevodsky a lot is that although he developed HoTT (or better the "univalent view") he also suggested 2-level type theory when he saw its limitations. I hope you apologize but I can't supress the following analogy coming to my mind. After revolution in Russia and the civil war when economy lay down the Bolsheviks reintroduced a bit of market economy under the name NEP (at least that's the acronym in German) to help up the economy. (To finish the story NEP was abandoned by Stalin which lead to well known catastrophies like the forced collectivization...) Sorry for that but one has to be careful when changing things and think twice before throwing away old things...some of them might be still useful and even indispensible! Thomas