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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-it1-x13d.google.com (mail-it1-x13d.google.com [IPv6:2607:f8b0:4864:20::13d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f4a44546 for ; Wed, 20 Feb 2019 00:22:27 +0000 (UTC) Received: by mail-it1-x13d.google.com with SMTP id n124sf7722614itb.7 for ; Tue, 19 Feb 2019 16:22:27 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550622146; cv=pass; d=google.com; s=arc-20160816; b=jTyUM3wBlYMNOgBX7H4BMXpI8XNJr2j4Ucx4ZXRURU3iYvg3gg2QJzSwhhWmM62tnn YMFhKi+fKNaNJlj56wfJLW/DTCK+D3l+6yXN3zImYkyjrLiM/4FvkkzhxUieUqBkDHd6 MI+FzkSIKSmp6zjY5u/90mbPScR/xfDmNAaMdIkUrcLbSci2Qfc9UAwGPRjvlNnGeHAR z5sza1s8G8zpz3B6QDSPegqJrfX1fjgFM6Fy1ObST+nnCmOqnzkVj1C0rxaQ0fbf9iPP /V78pCLpKy3QJLeURZCr4RIpur1QVSiJ9sS7sA99yB22kkFKCsce6juSTMIatV7DPjlQ Ku3g== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=iwmLwv/qAAU589moIaZvZCg72ly2o2Q3+JcFbnMAS8g=; b=YTwogbjTI18FcdF8hYaZiRmHmDZG4kppO2b1jLux9QX4y/BLDy0YX+Ee41c8sx4vs8 lsiiCQzB7Y2cskpHrQW5XCAjuZSrGF6oJaqRZ3MsmoSXOJo+JWJ/1e4jowVoNj0RxdIx y4FTQlQsaEb47mNj3fCHbXYHYt/BkRi6yJVYIjbywmi98RCyRoorMuTD/j9xHd4sLkaa SsDtJcuKGk32kUlKS1zqWx2K0fiSYykQehRQgJtY4fRw1FknArc93vuCsvFekxxMkTOe tkPH6PUpkHP0B0w8nJeA6eS8+fwl2swFORHJ2fdEuGqLfg0xifKRURVMf/VvdjxGIUaL SfIQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=bKVRGyNm; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2c as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=iwmLwv/qAAU589moIaZvZCg72ly2o2Q3+JcFbnMAS8g=; b=FC2r6wvcx+hdSZyJ6+SSzqmluUjWSh1sxgk31wAVvoz2PIU4Mlj7nFiIYroJUs2Cu5 hp139vH3JYJbDn3ATIBtfBkKiDxN1IamoRv0jMAWTdQVeosE7ebgDNJfTdafruR7FmdR hwfBLp3W8sADUqNN40rub8OEn6jQKoPnhZFhLu2jmZFRfETjGvvQHKgQxViflJg1RuAG vhwGQxqIg5TgAe4BKCRCom4f2bNwFM4N290VVQWBcH8w8YU5XNWDJkUTV7QB2f0PPkBt 4YW79OVqG2+0X2CRtdXjtN5eQG+CnPrIYCxIryAonImYRekLHDi9pfwhDYqJm7ZOLWZh YEHQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=iwmLwv/qAAU589moIaZvZCg72ly2o2Q3+JcFbnMAS8g=; b=rAaqbzhwJjFzCCHg8No4wvDdYIeJQf2XNtaXD2qsY4hdqxZHWbMlgdPcspG6M2aXiV nTJTsUJ50XP3/5ikAwkaxI+9eYvicY4hm3tnoLTei7CH0frj1gpk+8TOU4wcINerccHS VUJGFa3eEE/XlJdUcygczxD0xtI0S+IzLX3i4o19FhTHfUz9taYd3rQSqS7bA2qGP+W2 KTI9HJ6/mDDCY7VAw8wzjSPSDmFTelMBts2bgVDoQYcGZlR4sUtLffGDE+Qq3HceVXdk HwU9avBPY/7pC+OvFxBD49yHbnPdFGxZVNM9po04ZD15PJvB6gVWc1tVEHuk0oq9yXwh eu0g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaAzN/JtfI1PXI5d2AdO24gHyHSDxptdMxe59mMgbeEwMM2W5Nr n56l6Rx7ZoQp0nK3iVbSejU= X-Google-Smtp-Source: AHgI3IYdwLMypXkA1p2VvXECkNgqdNNq6sjxFGrLfyt14zX/NBDuGSdUNoFxnEi6I6IebUvM+X+wZw== X-Received: by 2002:a6b:7513:: with SMTP id l19mr114511ioh.0.1550622145762; Tue, 19 Feb 2019 16:22:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a02:3b14:: with SMTP id c20ls2068529jaa.1.gmail; Tue, 19 Feb 2019 16:22:25 -0800 (PST) X-Received: by 2002:a02:8a2f:: with SMTP id j44mr18657259jak.17.1550622145431; Tue, 19 Feb 2019 16:22:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550622145; cv=none; d=google.com; s=arc-20160816; b=YoUfMgLkYdIKNJ9Jg6Ufa+0OZJtDKbHKhzrxsip+blWiwYnCOULBVOTvvn0GERpdAW hMH+Mma6eT1Iz8b5rwUq+bXk4ww4yZTPWe5uc2GO2P9c73qoe+Vscjwh66owwLS4UHwe ls6LY7FdQPZSBvLMgGMCeflGBtyPMMnny47VV/O1OSFOZdGikXHhYCbYETxqqYOL6QWK /bxfnsX0KhmBTb6d8rKngigCJBfHiBV18Gko7h0jtehgHj8Kod6LD3nf0N44aLL/CBxq 3YY0c15T6/vqI7n5Gvo8/DiWOF0Bo70qNjL97XfvnKT+4J1bzVWwc8+++Tv3vawSWEVN e3mg== 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=cDC7aQyYApLEdAhcxmwgGPoKFuNweN8w6NelY4BJ0Eg=; b=eh72Lojw+L9pwMWfvzXKxLyNEzSTZXG3mT7UUvMU3a8hq8oFR3emTVIOA7Dn9xAjfn X56BNr3NE5pLURv+cCJSktIscWI+YHTQDc1L63jQhrV9nQudJersVkxTwnRcxejPR8RX FeqzqrgYAs/X3rdGbdDZPHTnTLN0KesUOlXOHpxkyy0fDaKXi898fIu3t5TFAV1tfUyk TYxZJBdY2Hrh15kIMNcWOFD4TAY9vw7maO3p0GYzOeGsRi+SNzxuHkU2CACKkBrfQI3J LmZKfSQAbxbl+oR7C2IUJ5rSwODcqmjWeEyTg0O0/xzrzgI2zakD1bVlfLDV46O9wgHm J84g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=bKVRGyNm; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2c as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2c.google.com (mail-yb1-xb2c.google.com. [2607:f8b0:4864:20::b2c]) by gmr-mx.google.com with ESMTPS id x76si143473itb.1.2019.02.19.16.22.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Feb 2019 16:22:25 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2c as permitted sender) client-ip=2607:f8b0:4864:20::b2c; Received: by mail-yb1-xb2c.google.com with SMTP id 7so8881726ybp.13 for ; Tue, 19 Feb 2019 16:22:25 -0800 (PST) X-Received: by 2002:a25:d60e:: with SMTP id n14mr16907810ybg.71.1550622144687; Tue, 19 Feb 2019 16:22:24 -0800 (PST) Received: from mail-yw1-f46.google.com (mail-yw1-f46.google.com. [209.85.161.46]) by smtp.gmail.com with ESMTPSA id o76sm14099272ywo.106.2019.02.19.16.22.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Feb 2019 16:22:23 -0800 (PST) Received: by mail-yw1-f46.google.com with SMTP id k14so8539903ywe.4 for ; Tue, 19 Feb 2019 16:22:23 -0800 (PST) X-Received: by 2002:a81:6b09:: with SMTP id g9mr14420344ywc.255.1550622143385; Tue, 19 Feb 2019 16:22:23 -0800 (PST) MIME-Version: 1.0 References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> In-Reply-To: From: Michael Shulman Date: Tue, 19 Feb 2019 16:22:11 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=bKVRGyNm; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2c as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , On Sun, Feb 17, 2019 at 4:08 AM Matt Oliveri wrote: > What about infinitary (non-elementary) limits? Are there infinitary homot= opy-limits? They are more common than discrete inductive types, right? So w= hat if I considered a stream of A to be essentially an omega-fold product o= f A. Would that have a strict extensionality principle? Yes, that might work. I think that the last time I thought about coinductive types in homotopy models I was trying to give them some kind of dependent coinduction principle. But if we take seriously the positive/negative perspective that I advanced before, we would expect coinductive types to have simply a destructor, a non-dependent corecursor, a beta-rule for destructing the corecursor, and an eta-principle saying something like that the endomorphism defined from the destructor and the corecursor is the identity. And that would probably be modeled by the omega-fold product of a type with itself. More generally, if F is a functor that preserves fibrations, fibrant objects, and sequential limits (like F(X) =3D A x X for streams), then the infinite limit ... -> F(F(F(1))) -> F(F(1)) -> F(1) -> 1 might be a model for the corresponding coinductive type with such an eta-principle. So maybe there's nothing wrong with coinductive types as such, and the point is just that computational considerations like decidability don't always match up with the principled category-theoretic explanations. (-: > 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. For one thing, I have no >> idea how to construct coinductive types as basic type formers in >> homotopical models. I think the issue that you raise, Thorsten, could >> 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. (-: >> >> 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't. >> It's just a non-arbitrary "baseline" that is consistent and 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're >> being deviant. (-: >> >> On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch >> wrote: >> > >> > On 17/02/2019, 01:25, "homotopyt...@googlegroups.com on behalf of Mich= ael Shulman" wrote: >> > >> > However, I don't find it >> > arbitrary at all: *negative* types have strict eta, while positive >> > types don't. >> > >> > This is a very good point. However Streams are negative types but for = example agda doesn't use eta conversion on them, I think for a good reason.= Actually I am not completely sure whether this is undecidable. >> > >> > E.g. the following equation cannot be proven using refl (it can be pro= ven in cubical agda btw). The corresponding equation for Sigma types holds = definitionally. >> > >> > infix 5 _=E2=88=B7_ >> > >> > record Stream (A : Set) : Set where >> > constructor _=E2=88=B7_ >> > coinductive >> > field >> > hd : A >> > tl : Stream A >> > >> > open Stream >> > etaStream : {A : Set}{s : Stream A} =E2=86=92 hd s =E2=88=B7 tl s =E2= =89=A1 s >> > etaStream =3D {!refl!} >> > >> > =EF=BB=BFCCed to the agda list. Maybe somebody can comment on the deci= dabilty status? > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. --=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.