From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:90b:4d09:: with SMTP id mw9mr18134788pjb.55.1589123777476; Sun, 10 May 2020 08:16:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:4b5c:: with SMTP id k28ls2874019pgl.0.gmail; Sun, 10 May 2020 08:16:15 -0700 (PDT) X-Received: by 2002:aa7:9f5a:: with SMTP id h26mr12381178pfr.281.1589123775676; Sun, 10 May 2020 08:16:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589123775; cv=none; d=google.com; s=arc-20160816; b=jFSGyfuIoSrpEOL/1/Pze4MJpA4f06bBO6pyI0Qya2M5rQsAK43fz4SIWp+WVh+iU5 zVpW1AbEqkFJlrommD8nT1WO/n6GITowqGpO/BQ5fKQPgesBVG83fL36WTrAct2phmzG cOv7N464Ful/mpDoqhFLsXF8tMnNFwQYoWpyfAbrk2rqjFQkKjkR0mBU2nInS3h1NgHl 5OZPVg0zpBBFY6GpvabQruelcf9yeb7b2yL4Q6JSBRuioC7l0BYXQJH7ffDCwtx5De0T pyHRqsELl7IvkDrC+xG6MIkM0dMeFT+ByKpN3gb6t5cB4UBoKfyYxzDo3J4gmhAq+VMh CiRw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=UdzGQcxuSBP+ecrD7Y7n36dJFyYYDfNOBoBZqEfYexQ=; b=cqSbfhw/I5lY1BTqCNWQn/vi0VgAyH62B+F56syAXQgzfH0k9BRt0t772zf/MK5AHQ g0RhcT387MQH93DdOK3V62xdGO7eNWysIXjyIJmfObcEVOZhX9x0Y1qq768xo+M2oBGg mAXc41y2Qh/SHN1gEA0sC8TD5pX4nBxAqkFMKIXmbFUNrITRk6H3fS3B3yhIScUb6QGH r+GBQsJ1OHFvd1/bXscMtl679qnQ0/PuZk22nsdM8wEsxeUtVUuH6WPYprCwexks576T 7ZDfUk8GINQDMYxHHzNNI5X/1OVO/GodS/h6i/078dfeohpzHLnb3zjUKRzbGkQSs+cS 3thg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=P6tOinHS; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::334 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-x334.google.com (mail-ot1-x334.google.com. [2607:f8b0:4864:20::334]) by gmr-mx.google.com with ESMTPS id w8si476238pjr.0.2020.05.10.08.16.15 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 08:16:15 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::334 as permitted sender) client-ip=2607:f8b0:4864:20::334; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=P6tOinHS; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::334 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-ot1-x334.google.com with SMTP id m33so5533808otc.5 for ; Sun, 10 May 2020 08:16:15 -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:content-transfer-encoding; bh=UdzGQcxuSBP+ecrD7Y7n36dJFyYYDfNOBoBZqEfYexQ=; b=P6tOinHS+2nklx7sCroQs27vq8QCp21b/9xIJkDdRWfGYegGA0PqOItSjg1Eq0GdjO ukEA1jO6uWzjiKto+f/dfGpgy45pe4XkRfO2V67TaE077SsDGNz8MFS9POVNtW4p3bR5 7DwVoHmUbfVqw4L1FjAgjDUCvLNvqBNYnESwMOsSBfuQbmJCsXve/682xYZJMB9IyDnd B+PkJCWGm3VADKwwtIXPCg4xvaYNzMvAsi1m0dIjFuFfSlBH9ttq+kEfp0Kn66FQU0hM W/niQb9+dT1lOvYsRP2QimGoWoNS1vFETl6zE6zlOAA2ulqfwz9RKOwTuiF8r6pN6LRv Y9CQ== X-Gm-Message-State: AGi0Puai2ecVQZYSIYUrS/BXeI/wvw3IEbzoM0N3YEzdKit4L6GCgT4O LEd5Ep87JYudnMIaQQ7jIh86Y4Gf6No0gqnOwYy5MVSuuvL71y6+nc63iP45be5MTk5/svX4KeH o/TQo2cxpNk+k/fyudHHGs0zCJfr9okwKOc5RJm3gmrDOZzHcfP+RI3eDN11+IDXrZ7n5AKjLPt 84CXpc/wjQ X-Received: by 2002:a9d:69c9:: with SMTP id v9mr9747987oto.267.1589123774644; Sun, 10 May 2020 08:16:14 -0700 (PDT) Return-Path: Received: from mail-oi1-f175.google.com (mail-oi1-f175.google.com. [209.85.167.175]) by smtp.gmail.com with ESMTPSA id i8sm2085051oom.15.2020.05.10.08.16.13 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 08:16:13 -0700 (PDT) Received: by mail-oi1-f175.google.com with SMTP id c124so12743443oib.13 for ; Sun, 10 May 2020 08:16:13 -0700 (PDT) X-Received: by 2002:aca:6508:: with SMTP id m8mr17117277oim.54.1589123773354; Sun, 10 May 2020 08:16:13 -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: From: Michael Shulman Date: Sun, 10 May 2020 08:16:01 -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" Content-Transfer-Encoding: quoted-printable I forget -- does "exo-Nat is cofibrant" imply that exo-limits of towers of fibrations are fibrant? That's another useful axiom that holds in models and might make it easier to construct coinductive types with judgmental computation rules. On Sun, May 10, 2020 at 7:52 AM Nicolai Kraus wrote: > > I would guess that "exo-Nat is cofibrant" justifies the coinductive type = in question, but not its judgmental computation rules. And the judgmental c= omputation rules are probably the very reason why one would want this coind= uctive type. But this is just a guess. > -- Nicolai > > On Sun, May 10, 2020 at 3:35 PM Michael Shulman wro= te: >> >> 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 wrot= e: >> > >> > 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 kn= ow I suppose), because Delta is not directed. We can do semi-simplicial typ= es as a Reedy limit, i.e. an infinite Sigma type >> > > We can certainly *talk* about simplicial types in 2LTT as exofunctor= s >> > > 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 semisimplicia= l >> > > 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 m= y >> > abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant", >> > this gives us a fibrant type that one could call "simplicial types" (a= nd >> > Thorsten does). But of course it's an encoding. If we decide to use su= ch >> > 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. taki= ng >> > 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. W= e >> > > 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 assis= tant. >> > >> > -- Nicolai > > -- > 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/CA%2BAZBBr0Zh-uLfEZCXUapK5KHFDxkzxyvLW22zyjmrB8KmWtYQ%= 40mail.gmail.com.