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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qk1-x73d.google.com (mail-qk1-x73d.google.com [IPv6:2607:f8b0:4864:20::73d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id cf7b7b3f for ; Sun, 17 Feb 2019 14:25:12 +0000 (UTC) Received: by mail-qk1-x73d.google.com with SMTP id a65sf12771292qkf.19 for ; Sun, 17 Feb 2019 06:25:12 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550413511; cv=pass; d=google.com; s=arc-20160816; b=XpMJdrc5L9AJNyP9GryL6+ftZ84mujGqBBVtcq4apGEz1DHOjwzYJP4ZO3/454IlYq 9jkRzyCe2GcCbEympC2GmdCLt4MnD1ODuvPYn/4Ykpiu+K73lpQt5pGfYJjPTEKd9Jbs njysJeNK7r2at/57ToxuTWSnUEPw+bgFYkF3AAJKwrAZ7ZLKsAVaGatKaZ3ygDXl8/J/ U36BZ+KDq2RlB1bmlQlVOvucmrN6SffMXreMRrZiNhCfFaWWFYacd9oL6XJ9LA/6le8m Mt3kKqSBR9CeQHIyuVGy/JS0Ey8RtZeaUBnWt5d9pl2TzSK+9NNFfmqCZ5vqonzfwNlK 43PA== 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:dkim-signature; bh=9v1dguzeWlLEppimC7CRimPMu3n1+lgTKS89VPID7IA=; b=mAdf2qulz3ZnqKUyanlF0RmTSnmO7hFXMs9rAXoKYuSZ+XsHhnqvF8xayndzZxX6QG IkX8tfPBz0f9wvz4laisCQ7MI2p02Sr+o2+e3AaAtNtU5wY4Bbx4G8AThYZZgY6FYMTs jUtLSVb6f8CtL0ItgIbJfCFUI5ZeE1UYKM2TEni4xAMZg5/knnAg/9Jxn15Edgp9qKsW Ft1hs7VH1JARp7/kmm7hJGNgm3sKPspaCUi9CNeNvAHe1KKmTwkxZfKXKxHqiKRXtLdj tQDD5Ohu9etExcsR35sQDe3X7TerqHJzK+B4hMzJhG96uhBBHXUrr7q1vLEu5cG5xzQZ ST5A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=OmjztWFQ; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=9v1dguzeWlLEppimC7CRimPMu3n1+lgTKS89VPID7IA=; b=VLcELlrDhTaHDY+Q6aojD51/1Lr+XDsUv/hZ79epbGN5M7oeFu15en55BPkzJJWV1d YQjgu59XQtbndWly65ILJ/QoiUy6XcW9oaHr/D9KKIWnJxN7xILwaEgTAGBbcQkZr5uk bO7wyUz4pbaOdtGtBi4jjOfvVPzdqeJiQVyeP6F/O1WlwGAEbOe33bvx6QPwwOGI43vK Dflf/jgPUSH+/R3PuQ+QoqaJR9WiD/O6t3XCyWXLmzLfpuQ9tRDSf+7Y3aY2k1fTjujW 95KLDNT4slY2ukS2onTTXwk7o3ZsrWWsmiNxqcCyyJP3fwThZrfKBuALa2QAaxxz73Rp YuYQ== 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=9v1dguzeWlLEppimC7CRimPMu3n1+lgTKS89VPID7IA=; b=slfePFWO7w26xUxU56be9edtMPwEN8vmZyD20SZ2rhmNYRy6O027ls2tIe4U5H2q0H MLYpOaskfKvIQ9wogTYP6XGqbG5YsHU4omwjkiTZYcToEkSL+gKB/vA2mhw1nVGkfMC8 UUUjiPGmK7V8gff491C96HHzls8kXpDfX5G1liZ4OsweRmE+Opv9RE0QOt/D4oVrYTfQ ki/CtV9U338qzv3FxuHvnzXScxekR36yLrBfIQDfJhtQqPn0YDc93E38DsqJZ8XWqj1F c5BXWpUch1WYGHkhQczQowE23gnVa3DgoI1LFFcEBU9MaJj9hD6Ngwt0VO4eBhJ/gzfV 9qjw== 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=9v1dguzeWlLEppimC7CRimPMu3n1+lgTKS89VPID7IA=; b=Fr09ge1e4DqEiq/8zg3S7uP3Rp3aaDUZZL49jqZy8wd8LHsUa2xr02AXeCIEndS3g9 WALKGk81DxKa+yONEz3sRb0suv557MMHnzk7L2GYKA07U8mmmxJHFBau2jw4RxLKl8dS ovTnHfsPP79MMUyC5TqJjx4x1mBWgCqj/NFZZXz1nUHQ/SyaVz+aQypHbOI45f7dhrCj 7jO7Ke/SVnFlVJ245vSLzuYk/sYvWnolZbMk1CTo/0eUYeDlPUAjXtrS8KhzfsS4qBHr 9Qy50x1j0Rqe5r3BXFh0L/f93r3bUCk6jZLHju+RxO8AtupKzEVxC4t24YVjlrxVuPpF likw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaAvczbLjmxO8myCAkJGEytvH/LAtBxcqOesAV/hRR8g4yul7ez x7I7cYJxprK2diSb92DPrbw= X-Google-Smtp-Source: AHgI3Iaa0TuUnINTmCKdngj1UtOEa0o8qTQXa6mx+9fugwvmRHLXAkDijGrNKxvh2xt9XJm+7wg3IA== X-Received: by 2002:ac8:7044:: with SMTP id y4mr159641qtm.7.1550413510095; Sun, 17 Feb 2019 06:25:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:2201:: with SMTP id o1ls5464582qto.2.gmail; Sun, 17 Feb 2019 06:25:09 -0800 (PST) X-Received: by 2002:ac8:2b21:: with SMTP id 30mr11499217qtu.33.1550413509739; Sun, 17 Feb 2019 06:25:09 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550413509; cv=none; d=google.com; s=arc-20160816; b=MFIQgt2/oaBVf1yryqVeLB2IvGhu/z34+jN5QUqq2l+1CrZ/mXfvZ32R1jSaY4Qg7L AEKHSAzH5g9k9c3PJ73oxgudM3GpSPhcmLoDkrBmVie5jBk6Or5L2jjtF8h0Ah9pw+lg Tpq1okVwzxaN8P6DXSSNFAWk6rt1zYgmcruJ0rKZyot+ZDWHw08sd+IQpfOtcIyU9gJC DQzVZd1UKGD+8zJys4SbijoaF0+DhE5DEhBkqFVfs3ZyZmUXjYrP8bS1RKqxFOmE4frP jJYTFNBswME+MWLOl5uMt38o5k+E9Wt83BlmWQuBMBBq0pBbth0Ph6ezNg2PrO89j8G0 douQ== 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=qQHUa8c88KvsdBGDUHwpH7vJpdv0PPinlB2DyxV/NSo=; b=uy3oJwrAPDV+DDlp7pj3dstCAYx6xt0OMyqnkUp5IkQ08wR0/51WMuquimgpV4MKns EL9mr/AYcT5XAoCawcJQZhna2dKKnJY0WVD1azspfpCxrNxpwKDOiNUriLNeinAsCvGU UcGUfRUEw2Xzo1KLt9XCzOHyzsKkIhQpm4P0N3uyaZVYlfEbgHAnQCKyUrNsos4Of0mJ 7bn8u7sV44+Fdafe29g4Osg9bkvDeecEUrBnLDTCrsTohd256v1bPFmvHpMnE2OUPdOP VvINdafuvDn7MPpHILEBc3bd4tt+p/mn25Qiuz7v9fkRsOLKRYGBnY4vS9e8S4vVKLS8 LfUg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=OmjztWFQ; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb35.google.com (mail-yb1-xb35.google.com. [2607:f8b0:4864:20::b35]) by gmr-mx.google.com with ESMTPS id m1si53868qtc.2.2019.02.17.06.25.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Feb 2019 06:25:09 -0800 (PST) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b35 as permitted sender) client-ip=2607:f8b0:4864:20::b35; Received: by mail-yb1-xb35.google.com with SMTP id 18so4147068ybf.8 for ; Sun, 17 Feb 2019 06:25:09 -0800 (PST) X-Received: by 2002:a25:ba8d:: with SMTP id s13mr15275838ybg.332.1550413509279; Sun, 17 Feb 2019 06:25:09 -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> <5831E465-6CC5-476D-8C2F-43E5B0D63017@nottingham.ac.uk> <0c48660f87d8ead6d1bd2bc5e61d8b6f.squirrel@webmail.mathematik.tu-darmstadt.de> In-Reply-To: From: Bas Spitters Date: Sun, 17 Feb 2019 15:24:56 +0100 Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Thorsten Altenkirch Cc: "streicher@mathematik.tu-darmstadt.de" , Michael Shulman , Homotopy Type Theory , agda list Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=OmjztWFQ; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , I think Thomas is referring to M-types which can be constructed in HoTT, moreover, they have the right equality in guarded or cubical type theory. I've collected some references here. Please feel free to expand. https://ncatlab.org/nlab/show/M-type On Sun, Feb 17, 2019 at 12:44 PM Thorsten Altenkirch wrote: > > > > But function types are neither inductive nor conductive. Only N-> (-)= ist > coinductive. > In presence of function types most coinductive types can be implement= ed. > > You think of terminal coalgebras - that is not what I mean. To avoid this= confusion I am using the term codata but most people in CS understand coin= ductive better. You can define a type by saying how elements can be constru= cted, this is data Alternatively you say what you can do with it, i.e. how = elements can be destructed. The function type is not data, functions are no= t understood by the way they are constructed but what you can do with it. A= function is something you can apply to an argument and you get a result. C= odata types always introduce non-trivial equalities, because all you can do= with a function is applying it to arguments two functions which provide th= e same output for all inputs are equal. Hence functional extensionality sho= uld hold. > > Maybe coinductive is a style of programming but nothing really founda= tional. > > I think you miss something important here. > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > -- > 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.