From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:6214:17d0:: with SMTP id cu16mr11758394qvb.177.1589120850813; Sun, 10 May 2020 07:27:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:468d:: with SMTP id g13ls3537975qto.11.gmail; Sun, 10 May 2020 07:27:29 -0700 (PDT) X-Received: by 2002:ac8:4983:: with SMTP id f3mr12036884qtq.343.1589120849738; Sun, 10 May 2020 07:27:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589120849; cv=none; d=google.com; s=arc-20160816; b=On4bmohkFx6zG0tFsoxK3J1H+jqkeQi2l9gjJr6AbtBglKe4HozHniBmYFz8K1tZ8M 4OnyzU5bQtEwQ2p0D4PGcpZyQc5zItbUwTe196aFSFg9jS5ddKlctuWPHpkDkskv6Ofd HG9V01NYmcpI3ysEsgT39S7b/+lMY0WkSKX3qLqX3MYxYU/dDicKD2nC8YTWaYlmmRba 1ZZmrAzws9T1FMLMUvb8AmYXPWMd5eYJhTT1GdOscxmYIl047z04XSd087XBHbD1Je7+ EaIoKpEQS0cLz5qA3bqKNMGtTH0iMIzGgVLyTfJ3+RCkv0auVPC39ueXBjepuYTcm0WW r6hA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=imw01CrvpbOHsA1wUiLELPdbA1CUn/WQFiJPrtxkVQc=; b=GSkJrCJipbIXJSOyU5zaDGsDHx4+K34zMS3/pBg06pZVsu33+R1LoZFOZ+9jeKAI+O qYyhJXlpoxM0qoqLfH4ZqsGbhd4rU/7+BFv8bAe6BDEiqtsombgu4R+o4FmsCwo35Dpu 9xzxo9ag5zMrqQfX1dCbv9a5WZ4FY6l3ZB83J8f88RynRJtABlVido5ERpPUKgmdI8/K 281f/Jt/oIcFVO1uTLsuNpOc8qAuu1zITL0RH1wWp3zFBHNM7hRFSMRi9xpHCWwY4xds EnKBh1bAVIZbVebqUrOHE0SEeCcAgbJJ+12ie3d3Pke0HvI5GcJc7S70mMV2LuVVT73M qRAw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=aaJlYo+E; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::331 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ot1-x331.google.com (mail-ot1-x331.google.com. [2607:f8b0:4864:20::331]) by gmr-mx.google.com with ESMTPS id m128si617689qke.3.2020.05.10.07.27.29 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:27:29 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::331 as permitted sender) client-ip=2607:f8b0:4864:20::331; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=aaJlYo+E; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::331 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-ot1-x331.google.com with SMTP id e20so5444481otk.12 for ; Sun, 10 May 2020 07:27:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=imw01CrvpbOHsA1wUiLELPdbA1CUn/WQFiJPrtxkVQc=; b=aaJlYo+EakpBihApOR/Tgqe0XhT7rOjUJkUue2OAuC20o4PJg/XiDacWxmpwpGV5Uv /u292OXdjMlYu2v+bhRnI4aMQzjJARtGwnZ8RNJbkhwgsepE4Mf2osnVnCjpf0ZPq7Tx EBanH0YYIJm3+buvTVofzOnaE9ZbWhq/hcwHeYcMzxmxuWmrQ8TA+iUt4AFq6/YincAf fP8dGRUJnuehJhaRYRQ16VO2HlIdha68VRZEktGoYqdCas0NkOPmVnf4s2UgU3LIbu80 OoItjS7oPtgyfxHjHPri6yOPCSRTWEeSUVzlpZyB15UJNn7x2zkuaPPaO6Ex5QvHxsql DuZw== X-Gm-Message-State: AGi0PuawXwzFeXAWjkJiYfstyGGkrEQVj3bW4cx7n4mQuNYD9GG2YOe0 NEhB1DrdPkjhj6tMbXfva7S70eH+0blUn8AfAoE= X-Received: by 2002:a9d:7082:: with SMTP id l2mr8973449otj.361.1589120849229; Sun, 10 May 2020 07:27:29 -0700 (PDT) MIME-Version: 1.0 References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <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> In-Reply-To: From: Nicolai Kraus Date: Sun, 10 May 2020 15:27:17 +0100 Message-ID: Subject: Re: [HoTT] Identity versus equality To: Michael Shulman Cc: Ulrik Buchholtz , Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000b93c1705a54c0750" --000000000000b93c1705a54c0750 Content-Type: text/plain; charset="UTF-8" On Sun, May 10, 2020 at 3:01 PM Michael Shulman wrote: > On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz > wrote: > > The 2-level type theories can be viewed as another way of making a type > theory that is faithful to the idea that everything is based on sets. > > While I kind of see how one could say this, I think it's misleading > especially in light of the above dichotomy, becuase 2LTT doesn't imply > any of the *internal* "types are based on sets" axioms for the fibrant > layer. As you know, 2LTT without additional axioms is conservative > over HoTT, while even with stronger axioms it can still be modeled in > many or all higher toposes. > I agree with Mike - sorry Ulrik :-) For me, "everything is based on sets" would mean that every fibrant type can be written as the realization of a (semi-) simplicial type, or something like this. --000000000000b93c1705a54c0750 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Sun, May 10, 2020 at 3:01 PM Michael S= hulman <shu...@sandiego.edu&g= t; wrote:
On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz
<ulrikbu...@gm= ail.com> wrote:
> The 2-level type theories can be viewed as a= nother way of making a type theory that is faithful to the idea that everyt= hing is based on sets.

While I kind of see how one could say this, I think it's misleading
especially in light of the above dichotomy, becuase 2LTT doesn't imply<= br> any of the *internal* "types are based on sets" axioms for the fi= brant
layer.=C2=A0 As you know, 2LTT without additional axioms is conservative over HoTT, while even with stronger axioms it can still be modeled in
many or all higher toposes.

I agree wit= h Mike - sorry Ulrik :-)
For me, "everything is based on set= s" would mean that every fibrant type can be written as the realizatio= n of a (semi-) simplicial type, or something like this.=C2=A0
--000000000000b93c1705a54c0750--