From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a37:5d42:: with SMTP id r63mr3245157qkb.317.1588981452553; Fri, 08 May 2020 16:44:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:530e:: with SMTP id t14ls2160891qtn.0.gmail; Fri, 08 May 2020 16:44:11 -0700 (PDT) X-Received: by 2002:ac8:720f:: with SMTP id a15mr5488022qtp.207.1588981451283; Fri, 08 May 2020 16:44:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588981451; cv=none; d=google.com; s=arc-20160816; b=aZBFLzhxwMy9iecA+ZxGs6Ybgya5f4pwzjFu5VHS9uSvuXLgC1C7Wz0PYGOD7g9mDI 07XYpFmr3g4EWqNOt6VuwpnnD1SDGn0sdJCZc0QknD3Hrcvh4rHPFOTrm7wRc/ni+Ztf vrOSvizAH8UbXSqO/gYXYCw1VHASmYEXnMM48r3ZxF9PbUL2IKVnYH1Tu7x6pO8kQNjq uVRhX+R7JW6wevTdlRJt0WOS6Wxmav1rvD46uk2NTQ7gdLu30LfNMqztZWc6CR5xlMHC CyNzyhdHvXSNBm1iGl6rjvOQYFY5NCq9mAVChjZxhqR9Rt9AHBRUZxTNKGVPNZPb+ylh c89Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:in-reply-to:cc:references:message-id:date:subject:mime-version :from:content-transfer-encoding:dkim-signature; bh=CvOZjjSwes2ULxy2AUIaRafwfxamOXQo91Ox3Zvt0Zo=; b=G5pWgnUuKnAfWiz50HpaCXCjm4ucKG9BOcDLmW6W2o/52x6uE1TrtPP5d9/rQBjdJh GbQi5Gv95ijq9vnnNsHeOTkZUhFGs23KJ8eo6nADosCOBsSHeoC8jnV7NUZ5S9WfHD9G idjAMdtlTRmcxeNqWc8fKWqZnBbPJks/JKLxNpJDFokMhjNRmUAQN8tBsBR0pmCtfyQd K/ZjXo+zGYRpxB0fTQpZmNSNWwwXnDI5cE8HWfnt6Od6BjxcdwFfd4v8i2kXbl1gDWDG 4d1sgJbrhp7vMp0zzS7/lrhAL7EfFOMgsKtORHNjxDGw4+dSpxdOcLJRGtfEUIeqmDu+ zVOA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Xl92NUuU; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4864:20::72e as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qk1-x72e.google.com (mail-qk1-x72e.google.com. [2607:f8b0:4864:20::72e]) by gmr-mx.google.com with ESMTPS id w66si300889qka.6.2020.05.08.16.44.11 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 08 May 2020 16:44:11 -0700 (PDT) Received-SPF: pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4864:20::72e as permitted sender) client-ip=2607:f8b0:4864:20::72e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Xl92NUuU; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4864:20::72e as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-qk1-x72e.google.com with SMTP id c64so3639322qkf.12 for ; Fri, 08 May 2020 16:44:11 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=content-transfer-encoding:from:mime-version:subject:date:message-id :references:cc:in-reply-to:to; bh=CvOZjjSwes2ULxy2AUIaRafwfxamOXQo91Ox3Zvt0Zo=; b=Xl92NUuUcz8QXgi8UTmUXEEW6ljm4l20jxVpRlDTVz3Bd9CLHJ1GKjS6GPghoGKxdT 8XBq0vEQ0sxGV5WVxGzKhcVpylbabP1gcvgh2rp8NSIxvKoDdlk2QFgSZ1JrICyZOhKo ups4M/89XToTKTulH0ijQYni1sPvfu7YEXIntxVACbex7WaTqkytFMNWlevHKs/ftaNd xgFjsF2pgGG6KmxOcPS2Foa1uat9e+wrDpTaWa2E/n7mHWfj0uOlGYnV6SWTm+JBsi/Q 7ogfOud0N7C26gx7J1pHyd2qOnGg4O8bB9opj3oPiO9lYFTYjvhZ/yIU9skbSMWUIgC5 adAg== X-Gm-Message-State: AGi0PubmRzroPKTPoIpsTC9kUCP/w8mu8GeomUVOM7ThaIeOPRM2zEQE dscAlcSiI7z6cJLMp50lMoE= X-Received: by 2002:a37:a193:: with SMTP id k141mr5331952qke.147.1588981450941; Fri, 08 May 2020 16:44:10 -0700 (PDT) Return-Path: Received: from [192.168.1.152] (pool-74-111-173-45.pitbpa.fios.verizon.net. [74.111.173.45]) by smtp.gmail.com with ESMTPSA id a27sm2926204qtb.26.2020.05.08.16.44.09 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 08 May 2020 16:44:10 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable From: Steve Awodey Mime-Version: 1.0 (1.0) Subject: Re: [HoTT] Identity versus equality Date: Fri, 8 May 2020 19:44:08 -0400 Message-Id: <1044A78D-8F16-4856-9B50-9B7FB7EF579A@gmail.com> References: <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> Cc: Thomas Streicher , David Roberts , Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> To: =?utf-8?Q?"Joyal,_Andr=C3=A9"?= X-Mailer: iPhone Mail (17D50) Dear Andr=C3=A9, I would prefer to say that t current systems of type theory have failed to = *compute* pi_4(S^3), so as not to diminish the value of Guillaume=E2=80=99s= beautiful proof, which has even been formally checked in different proof a= ssistants.=20 You of course know the difference between proving something in type theory = and computing the value of a term, but some readers may not.=20 Best wishes, Steve=20 Ps: In my opinion, for what it=E2=80=99s worth, making a system that will c= ompute the value of Brunerie=E2=80=99s constant is an engineering problem, = not a mathematical one. Which is not to say it would not be an important ad= vance! > On May 8, 2020, at 17:06, Joyal, Andr=C3=A9 wrote: >=20 > =EF=BB=BFDear Thomas, >=20 > You are right, the equality of objects in a Grothendieck fibration is jud= gemental. >=20 > Propositional equality of type theory has been studied a lot during the l= ast decades. > I feel quite confortable with it, with the homotopy interpretation and th= e univalence principle, etc. > I confess that I am much less at ease with judgmental equality and the sy= ntax of type theory. > Until now, type theory has failed to prove that pi_4(S^3)=3DC_2. > Is it the symptom of a fundamental problem? > Is it because the reduction algoritms are not optimal? > Or because computers are not powerful enough? > What is the abstract theory of terms reduction in type theory? > I apologise for my ignorance. >=20 > Best, > Andr=C3=A9 >=20 > ________________________________________t > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] > Sent: Friday, May 08, 2020 2:40 AM > To: David Roberts > Cc: Joyal, Andr=C3=A9; Thorsten Altenkirch; Michael Shulman; Steve Awodey= ; homotopyt...@googlegroups.com > Subject: Re: [HoTT] Identity versus equality >=20 > Dear Robert, >=20 > in what I said I didn't mean set theory literally. I was rather referring > to all kinds of categorical logic where equality is interpreted as > (fiberwise) diagonal like (traditional) topos theory in particular. > These kinds of gadgets all have the advantage that "Set" is not ruled > out as a model. >=20 > Since the diagonal is hardly ever fibrant HoTT rules out Set as a model. >=20 > But this is not my main problem. My main problem is that there is at leas= t > one area of category theory where one has to speak about equality of > objects and these are Grothendieck fibrations. And these are intrinsic > for doing topos theory over general base toposes. > (That I really like them is, admittedly, also an important reason for me > not being ready to give them up! And for reasons of personal and > cultural "antagonisms" they are not very popular among the majority of > category theorists... Thus, there are many people who would not be too > sad about working in a framework not allowing to speak about them.) > But I want to emphasize that real masters of infinite dimensional > categories do not have the faintest problem speaking about equality > when speaking about infinite dimensional versions of Grothendieck > fibrations!) >=20 > Though (traditional) topos theory can be developed over fairly general > toposes and this, at least philosophically, is an important aspect one > cannot deny that most toposes of interest heavily rely on Set, be they > of the Grothendieck kind or be they of the realizability kind! >=20 > Thomas >=20 > PS Above I put Set into inverted commas because the logician in me > finds it amusing to speak about "the" category of sets which is > nothing but an illusion... Even the nowadays not so little number of > adherents of the "multiverse" view of set theory would share this view! > But even the "universe" view is nothing but an ideology because since > Cohen set theory is mainly a business of constructing different models > via forcing. > Thus, since Set is (sort of) an illusion it is important to do toposes > over arbitrary bases for which purpose one needs Grothendieck fibrations > which do not make sense without equality of objects. >=20 > PPS Some people might get the impression I am a "crypto set > theorist". Nothing could be more wrong. I am anti-ideological and > pluralist and I like "deviating" ideas. But I am interested in > calibrating what one needs for which goals. What I am allergic at is > ideological positions which want to forbid someone doing certain > things because they do not fit to some ideological positions... > And one has to accept that not all combinations are possible. Thus > pluralist is better to inegrist! >=20 > --=20 > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F54CC%40Pli.gst.uqa= m.ca.