From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33c.google.com (mail-ot1-x33c.google.com [IPv6:2607:f8b0:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a175adac for ; Sun, 17 Feb 2019 12:08:54 +0000 (UTC) Received: by mail-ot1-x33c.google.com with SMTP id a1sf11977983otl.9 for ; Sun, 17 Feb 2019 04:08:54 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=8zz1BrTKU44vcNYNsfwtUQY+t8kdJqyaIwN4DwBDDDw=; b=G+Cv9589rgXAWJpmtdGLdUdSJPEGnFPyrqtAudI9XwjR/aJ7vaFqJdxQWqGE88xXXh eW1agOtTgWf2auHvNwIecOOCZXgRgUiA0cZorXxBHdpnoHVabzhNFtYCUZa5wdOXQLoK 0Wq+MYUpmRTLOqdGARwPXdlD0p/483iuKd73mlWaT5ITOAd8SMNYFgsBrsBE6eh4maQK JRAEJ0ckP+SVK7RFJ0urKHzbHixLbKGaqYew/bxME28UPNanFWXcbygcmR/l2MAjI1NG SzbJoYWt1S0MskuLoq3jPts3Cvb6cJnY5YiE5o5sLE4AWJP8cWf91dqv0dPki6nHueoj DlaA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=8zz1BrTKU44vcNYNsfwtUQY+t8kdJqyaIwN4DwBDDDw=; b=K7+RlCLFPm7BctwskUGUi7jrtsiRzelCoiUXgEwt9bPG3oxfCUJKfnS/je3ua0yIIk GB0z/evF/56BszsFK6LelWmDr3FI307oZEl10yZe9D8V3kh+BfV2Eo4bbyd+0iVf1vVs fsOMTCTELvfXZwIVWMSkqbPYh66Q++TCBDr65PdZuBp0eHKOr6NUEGMLmcugL7VSV4Em h+zuTZWoUdnb+ZHjYUd+XJoeOWfGleGU8M/8IxglSjX+UTsv1XBy4C4Tz7G2kYYgGiBe G9xrTBcD8+7fNp9/CaGK6a9FwFDtnq1k+lFEjjwjPJytZRWdmfNngztMxfdi50QWjWly nfjg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=8zz1BrTKU44vcNYNsfwtUQY+t8kdJqyaIwN4DwBDDDw=; b=HikFabCw/JRFY0+UDH6Hug8KQw40pMY+qsKvKsyFFDBdj6ae/wsigbmnSMNT8+VqVx MXXZ2alGqv5NU6aQv0rc8+TvZpN0vCxzi3yjFt2j343bBfG3nJyJXAagDwbPnBpi2suc QftSGgfhRirajw0jabEtRqylATnmU+8w2StevSh1IZh3635YGvqUZ0N0MpHEgjMUwZh/ M1CyS37fSHt5qHSMfraTWaC3NSQqSmTrlxaQhtN/9n1oqbspioUsb4pfhshHu+nhfUyc deulOTrzQ9xquCzbvOjQssAm9XE9yO7Vtc2GOz3MQ8CU3VYkl4DYiRCgs18kBRbooZbC 4KIQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAub1se3yeNMrGUSirbzu96qy/pkXV+mpjtO6nrP/IsG8SNp6nO3d oMODSBEec3KsckJgnOhNP5A= X-Google-Smtp-Source: AHgI3IZbGz++MUkxM17Bx9FYJ6jYbNePDK5JYELcEoLuB/GzsjqUO7mETkYwzEXtyMRiEt9XsLiRZg== X-Received: by 2002:aca:cf4f:: with SMTP id f76mr168946oig.7.1550405333594; Sun, 17 Feb 2019 04:08:53 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:d685:: with SMTP id n127ls1959632oig.2.gmail; Sun, 17 Feb 2019 04:08:53 -0800 (PST) X-Received: by 2002:aca:4b89:: with SMTP id y131mr171256oia.3.1550405333058; Sun, 17 Feb 2019 04:08:53 -0800 (PST) Date: Sun, 17 Feb 2019 04:08:52 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_276_1105039915.1550405332443" X-Original-Sender: atmacen@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_276_1105039915.1550405332443 Content-Type: multipart/alternative; boundary="----=_Part_277_101432266.1550405332443" ------=_Part_277_101432266.1550405332443 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable What about infinitary (non-elementary) limits? Are there infinitary=20 homotopy-limits? They are more common than discrete inductive types, right?= =20 So what if I considered a stream of A to be essentially an omega-fold=20 product of A. Would that have a strict extensionality principle? More generally, I would try and say that a coinductive type is some limit= =20 of an external diagram of elimination spines. This might address Thomas=20 Streicher's objection, since the collection of elimination spines is=20 countable externally. On Sunday, February 17, 2019 at 4:19:01 AM UTC-5, Michael Shulman wrote: > > Well, I'm not really convinced that coinductive types should be=20 > treated as basic type formers, rather than simply constructed out of=20 > inductive types and extensional functions. For one thing, I have no=20 > idea how to construct coinductive types as basic type formers in=20 > homotopical models. I think the issue that you raise, Thorsten, could=20 > be regarded as another argument against treating them basically, or at=20 > least against regarding them as really "negative" in the same way that=20 > Pis and (negative) Sigmas are.=20 > > And as for adding random extra strict equalities pertaining certain=20 > positive types that happen to hold in some particular model, Matt, I=20 > would say similarly that the general perspective gives yet another=20 > reason why you shouldn't do that. (-:=20 > > But the real point is that the general perspective I was proposing=20 > doesn't claim to be the *only* way to do things; obviously it isn't.=20 > It's just a non-arbitrary "baseline" that is consistent and makes=20 > sense and matches a common core of equalities used in many type=20 > theories, so that when you deviate from it you're aware that you're=20 > being deviant. (-:=20 > > On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch=20 > > wrote:=20 > >=20 > > On 17/02/2019, 01:25, "homotopyt...@googlegroups.com on= =20 > behalf of Michael Shulman" = =20 > on behalf of shu...@sandiego.edu > wrote:=20 > >=20 > > However, I don't find it=20 > > arbitrary at all: *negative* types have strict eta, while positive= =20 > > types don't.=20 > >=20 > > This is a very good point. However Streams are negative types but for= =20 > example agda doesn't use eta conversion on them, I think for a good reaso= n.=20 > Actually I am not completely sure whether this is undecidable.=20 > >=20 > > E.g. the following equation cannot be proven using refl (it can be=20 > proven in cubical agda btw). The corresponding equation for Sigma types= =20 > holds definitionally.=20 > >=20 > > infix 5 _=E2=88=B7_=20 > >=20 > > record Stream (A : Set) : Set where=20 > > constructor _=E2=88=B7_=20 > > coinductive=20 > > field=20 > > hd : A=20 > > tl : Stream A=20 > >=20 > > open Stream=20 > > etaStream : {A : Set}{s : Stream A} =E2=86=92 hd s =E2=88=B7 tl s =E2= =89=A1 s=20 > > etaStream =3D {!refl!}=20 > >=20 > > =EF=BB=BFCCed to the agda list. Maybe somebody can comment on the decid= abilty=20 > status?=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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_277_101432266.1550405332443 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
What about infinitary (non-elementary) limits? Are there i= nfinitary homotopy-limits? They are more common than discrete inductive typ= es, right? So what if I considered a stream of A to be essentially an omega= -fold product of A. Would that have a strict extensionality principle?
<= br>More generally, I would try and say that a coinductive type is some limi= t of an external diagram of elimination spines. This might address Thomas S= treicher's objection, since the collection of elimination spines is cou= ntable externally.

On Sunday, February 17, 2019 at 4:19:01 AM UTC-5,= Michael Shulman wrote:
Well, I= 'm not really convinced that coinductive types should be
treated as basic type formers, rather than simply constructed out of
inductive types and extensional functions. =C2=A0For one thing, I have = no
idea how to construct coinductive types as basic type formers in
homotopical models. =C2=A0I think the issue that you raise, Thorsten, c= ould
be regarded as another argument against treating them basically, or at
least against regarding them as really "negative" in the same= way that
Pis and (negative) Sigmas are.

And as for adding random extra strict equalities pertaining certain
positive types that happen to hold in some particular model, Matt, I
would say similarly that the general perspective gives yet another
reason why you shouldn't do that. =C2=A0(-:

But the real point is that the general perspective I was proposing
doesn't claim to be the *only* way to do things; obviously it isn&#= 39;t.
It's just a non-arbitrary "baseline" that is consistent a= nd makes
sense and matches a common core of equalities used in many type
theories, so that when you deviate from it you're aware that you= 9;re
being deviant. =C2=A0(-:

On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
>
> On 17/02/2019, 01:25, "homotopyt...@googlegroups.com on b= ehalf of Michael Shulman" <homotopyt...@googlegroups.com on beh= alf of = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_277_101432266.1550405332443-- ------=_Part_276_1105039915.1550405332443--