From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a37:8606:: with SMTP id i6mr11654069qkd.282.1589122342491; Sun, 10 May 2020 07:52:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ad4:528b:: with SMTP id v11ls2042106qvr.9.gmail; Sun, 10 May 2020 07:52:21 -0700 (PDT) X-Received: by 2002:a0c:b78a:: with SMTP id l10mr10564740qve.121.1589122341267; Sun, 10 May 2020 07:52:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589122341; cv=none; d=google.com; s=arc-20160816; b=JBNrozwPJHKAIg5ii6Mp8DnwSh3JWf6cv4IYu53Rx3k+51XUsE51svbTY9Fi4JQrT5 VER0jjRvR3TQZZS/9E7/ZC76FkM4mmrywhEPWXA9gZJuJzjgHkZF8KajEsBi5BwHJ/HJ b6DXlVV0KnRGGCm3ucXUgpz/lSPA6A1NIYsTzF3yLFm116ByG8BrjauJuhqY1raJBcxg C1qiDoc5JG7yySN1TMEkWzILMi0vPHLR7qfA+sk4f22SHGWKBeSCd4j4+1HxZrxXvaYN CODywHnHsplndPHlvWjs8GGR8WXaxKD43uATIKjx4uiDvESCLXa9sN2sVtfEam2U676E W/xA== 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=juKrALvuZ+0wkwdCLu1srDiJtAXStBnZvTUnRwz12fc=; b=leKoPS+JkxiPaA8r47uuJqKoxc1G3V1q1ex8nQRMVZRQ2zl4WlxWFJg5ggeIKr93U3 gjzMJw+uJXApnFjTCmQ9G9E1/jsmffIFVdFav8FQEw1m+ogFsJfGazbrVCK7akGJQSqg w/hSmwNDg+N87H7c0xuTl7lnqFN1i5jyfznn9K+Xrf3+fm3ySbyqvbBHDdZZ66PlZSgQ 6qxT7tYo+31K6F6DAPFuUr23e4UsaNaYRZMlxB0lnds8rI8ZGaqsZWF7F1PkNmIEDee5 dxFlFfXXsP2wORic2/4rolFvvuMQdBKzZhsPRXebVMuj0jrl973wO4RipyspoCQKUmjU sfxA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=cwWwEmaw; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::334 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-x334.google.com (mail-ot1-x334.google.com. [2607:f8b0:4864:20::334]) by gmr-mx.google.com with ESMTPS id 2si427654qtp.1.2020.05.10.07.52.21 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:52:21 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com 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...@gmail.com header.s=20161025 header.b=cwWwEmaw; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::334 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-ot1-x334.google.com with SMTP id c3so5483276otp.8 for ; Sun, 10 May 2020 07:52:21 -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=juKrALvuZ+0wkwdCLu1srDiJtAXStBnZvTUnRwz12fc=; b=cwWwEmawyprZwVISkTMH6cdlJ4jhGMLJiXejkT9oeqZrToqhiqLf4Sl0ZDVgHXdSpT GJ8fqvd0jG5hQENf/0zOFLIAbtdF542qZIpf71Tur30Fr11EcTSb+F7MDzbhdugI/18H EXy2tdLaxgXDNa7FJkHR7vpAh1bgr248c1roGdnxVq0f5LJH7xJbYwJX3CgCjO2vAk7T WLNSy9kpp5Q1V053+rGWuqcvTlYXGKb1FKvT/++7bOrsGzGcj/9kxAePW0BwJQbPVYYN yUKtwXs/MsI8gSFzHim3+lSu+0haAbembwW3zVPyHc78nWIe+Z7x5wfxKlskL0Y1j+Hl rdvQ== X-Gm-Message-State: AGi0PuZP0ecpzHhW0XQLxEv0P3DXJaAzxIRX24ge/MX2QppwUgXGPnrV lfJq6cveaYO8iNzfAYBnI4BiEWtZ4t2Tg11alvg= X-Received: by 2002:a05:6830:1303:: with SMTP id p3mr9665370otq.186.1589122340983; Sun, 10 May 2020 07:52:20 -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: Nicolai Kraus Date: Sun, 10 May 2020 15:52:09 +0100 Message-ID: Subject: Re: [HoTT] Identity versus equality To: Michael Shulman Cc: Thorsten Altenkirch , Jon Sterling , "'Martin Escardo' via Homotopy Type Theory" Content-Type: multipart/alternative; boundary="000000000000a397f605a54c6061" --000000000000a397f605a54c6061 Content-Type: text/plain; charset="UTF-8" I would guess that "exo-Nat is cofibrant" justifies the coinductive type in question, but not its judgmental computation rules. And the judgmental computation rules are probably the very reason why one would want this coinductive type. But this is just a guess. -- Nicolai On Sun, May 10, 2020 at 3:35 PM Michael Shulman wrote: > 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 > --000000000000a397f605a54c6061 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I would guess that "exo-Nat is cofibrant" j= ustifies the coinductive type in question, but not its judgmental computati= on rules. And the judgmental computation rules are probably the very reason= why one would want this coinductive type. But this is just a guess.
<= div>-- Nicolai

On Sun, May= 10, 2020 at 3:35 PM Michael Shulman <shu...@sandiego.edu> wrote:
Many or all coinductive = types can be constructed, at least up to
equivalence, using Pi-types and (some kind of) Nat.=C2=A0 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 <nicola...@gmail.com> wrote:
>
> On 10/05/2020 15:01, Michael Shulman wrote:
> > On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
> > <Thorsten....@nottingham.ac.uk> wrote:
> >> Defining simplicial types isn't entirely straightforward = (as you know I suppose), because Delta is not directed. We can do semi-simp= licial types as a Reedy limit, i.e. an infinite Sigma type
> > We can certainly *talk* about simplicial types in 2LTT as exofunc= tors
> > from the exocategory Delta to the exocategory Type.=C2=A0 I assum= e the
> > point you're making is that we don't have a (fibrant) *ty= pe of*
> > simplicial types, whereas we do have a fibrant type of semisimpli= cial
> > 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 a= nd my
> abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibr= ant",
> this gives us a fibrant type that one could call "simplicial type= s" (and
> Thorsten does). But of course it's an encoding. If we decide to us= e such
> encodings, I fear we may lose the main advantage that the "axioma= tic"
> 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 fibra= nt 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.= =C2=A0 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" i= n 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 lev= el"
> that was discussed earlier in this thread. Allowing coinductive types<= br> > 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
--000000000000a397f605a54c6061--