From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a62:5f81:: with SMTP id t123mr12847717pfb.79.1589121308499; Sun, 10 May 2020 07:35:08 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90a:c713:: with SMTP id o19ls15097730pjt.1.gmail; Sun, 10 May 2020 07:35:07 -0700 (PDT) X-Received: by 2002:a17:902:cb91:: with SMTP id d17mr11304728ply.129.1589121306978; Sun, 10 May 2020 07:35:06 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589121306; cv=none; d=google.com; s=arc-20160816; b=rgn6olZzwAQ1smIDDJGExU2xaUl56M0wXjQkwGHSSDqDkrf8ZXrzhi2vVhL3PXXttd cFiz6lVZbC8QAgi43k3wMyU0JcP3eT4aQhsGmYI8DycT3sjAX9uhnteDb+MMi8urMFQ8 DLQoEOIwa7v46G0CuMXoCt+fOiASDQJUb9UmBqjIT9raYQgGdsC3bfz5VqebQiOJOhTm PDCRA7zr9Cuy1s1w/Wq6xOMnv0VYefLkYurjGUGipaqJzKe/JEKAtLj3mUV45/rbnVzq WPqAg5u7kaJyr4gRneucMD4YRUWrvq1JGr0E0wXMvW96OQ4X7IDvF9nrfZ5HXkcsMjf0 FG/Q== 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=/IVn2NNj5XErFg+MkyPc9Gp6fTpunD0Ad4505NS+kck=; b=cJxNI3e2H0ouPA6wU1W78pimbdwC96Krq5s2B3hgUT1+/hy0JtSeg6pmlsoWhYr0HN N7hY9KaUZicw2+kLtAWFByCSSOUxfKNhSZm6cR+BLgK1lYeqj94v3xNKREVrOH8/zOuu HMeqcsWA69MWAnRJC2lzVmYb6cmDwBu6AbIDjB3ts7n04Ju4jE743UzB4EEBwrLfNSOI aPtX+jXxT3lBBUXWEQxgpPuRBwXBQr/ORVaHPsGhHg5wjV9Jv1L9NffCKoDT6Ly1gNiC bkTD/1VUd79Cs0uJgdrmWsGUC+DqJZkh4sf137iQfQ8huGltLySqxI20Rlhl4qICGNhR PfDw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ZzPgeFjE; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::331 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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 t141si559029pfc.5.2020.05.10.07.35.06 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:35:06 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu 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...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ZzPgeFjE; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::331 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-ot1-x331.google.com with SMTP id z25so5446375otq.13 for ; Sun, 10 May 2020 07:35:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=/IVn2NNj5XErFg+MkyPc9Gp6fTpunD0Ad4505NS+kck=; b=ZzPgeFjEXDLYb/RWFnu6G3WI2dELyhmZ9VFifNAFiAV6wAe75x8Bam8cOWNYp7vz5q dPX27DtJa5nwtUtsJAiPCYZe94vcpI2qOXeJaJdG7pDx6wKruZIuXU+6LKXeIAtnhYtS nayk5YWual10V8kQhHwCXaAuwMGhxbis1jc/8TPVnOIY8XNTLZLzLzAHMa1lZbFVlSDn 3Lr5qVBB4JOQJpEQBajcICqO3ytstQsldgfQr4KIvAl1Anp9jZw/R6lQt18dK7yBTiRG qHi2S7/ajhHvsOn7lZxRYMhFmQ+rJ+WOaCLUhKEPBm0/kpvmw03CI+AcV4Ggi7DqmFub rGsg== X-Gm-Message-State: AGi0Pua9V8A8bnWYpAsF1s4d19dM67FUV/6wvBodLT+9e1LcehVmn9NF YHd2OjuC3ShnRzhNXnChPEmb7BxL5dwDXzNQUgX1gT0ZYFJ4/ygXSHV+D3kQDPV+3LKeUld8RZM xeFdgAaIhiWY01InAbSWKXUFldvyWyEbLf8X8j5oUM+D01B7NL4+zhnb5vLkBO/ns+pdys+ZHEi huu1amUYr9 X-Received: by 2002:a9d:51cc:: with SMTP id d12mr8823622oth.70.1589121305580; Sun, 10 May 2020 07:35:05 -0700 (PDT) Return-Path: Received: from mail-oo1-f48.google.com (mail-oo1-f48.google.com. [209.85.161.48]) by smtp.gmail.com with ESMTPSA id i196sm3959629oib.8.2020.05.10.07.35.04 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:35:04 -0700 (PDT) Received: by mail-oo1-f48.google.com with SMTP id c187so9303ooc.2 for ; Sun, 10 May 2020 07:35:04 -0700 (PDT) X-Received: by 2002:a4a:4442:: with SMTP id o63mr10461821ooa.0.1589121304355; Sun, 10 May 2020 07:35:04 -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> <154D1B4B-6881-4269-8BA1-1CE8EBB0BE0D@nottingham.ac.uk> <3ec2f134-cbd4-7bfd-0a69-efb734a4a231@gmail.com> In-Reply-To: <3ec2f134-cbd4-7bfd-0a69-efb734a4a231@gmail.com> From: Michael Shulman Date: Sun, 10 May 2020 07:34:52 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Identity versus equality To: Nicolai Kraus Cc: Thorsten Altenkirch , Jon Sterling , "'Martin Escardo' via Homotopy Type Theory" Content-Type: text/plain; charset="UTF-8" Many or all coinductive types can be constructed, at least up to equivalence, using Pi-types and (some kind of) Nat. Is there any chance that "exo-Nat is cofibrant" could be used to justify the existence/fibrancy of the coinductive types you want? On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus wrote: > > On 10/05/2020 15:01, Michael Shulman wrote: > > On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch > > wrote: > >> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type > > We can certainly *talk* about simplicial types in 2LTT as exofunctors > > from the exocategory Delta to the exocategory Type. I assume the > > point you're making is that we don't have a (fibrant) *type of* > > simplicial types, whereas we do have a fibrant type of semisimplicial > > types (under appropriate axioms)? > > Judging from the rest of his message, I believe that Thorsten was > talking about the direct replacement construction in Christian's and my > abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant", > this gives us a fibrant type that one could call "simplicial types" (and > Thorsten does). But of course it's an encoding. If we decide to use such > encodings, I fear we may lose the main advantage that the "axiomatic" > representations in HoTT have, namely avoiding encodings. (I mean the > "main advantage" of HoTT compared to traditional approaches, e.g. taking > bisimplicial sets.) > > >> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist. > > Personally, I think the best axiom to use here is that exo-Nat is > > *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy. We > > don't know how to model "exo-Nat is fibrant" in all higher toposes, > > but it's easy to interpret "exo-Nat is cofibrant" in such models, > > since Pi-types with domain exo-Nat are just externally-infinite > > products. > > I completely agree with your preference for this axiom :-) > But Thorsten does has a point if we consider the "engineering level" > that was discussed earlier in this thread. Allowing coinductive types > with exo-Nat as an index makes it possible to use your paper (Higher > Stucture Identity Principle, arXiv:2004.06572) and get a construction of > semi-simplicial types which is more convenient to use in a proof assistant. > > -- Nicolai