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-wr1-x43c.google.com (mail-wr1-x43c.google.com [IPv6:2a00:1450:4864:20::43c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id df827296 for ; Sun, 17 Feb 2019 11:35:06 +0000 (UTC) Received: by mail-wr1-x43c.google.com with SMTP id v24sf6209668wrd.23 for ; Sun, 17 Feb 2019 03:35:06 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550403305; cv=pass; d=google.com; s=arc-20160816; b=YQak9rPfZ97BZSQUivi9cogtguR4L+hqVAn67u+Y4b0y4ynyy2ogC2EG2w7gZ9NUSQ AQYfsqXCW4906btT1QAhJY6v6WERYnKvu6mgYoanhqBP+i9Fw+ZI/1Lrs2wTUcBZSMvv D+bCDlDs/snOwydecr4PtwojON/e64/Te5sJiVrbd6KLt95/UYQ7/T1yaqoTmSOmVrEt pOk70W6enCrG/EDlWSo8NwzS6EovEpPDBEsZV1c/4J48keLcrtCcVvVuosFpSgv/+oNq VTGsGqVLQrZWfPCZbdamfMFqMRFeEUeANGm1luI6Dw11LnQtaX+o4VlrJVhARmGwjNgi uZgg== 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:importance:content-transfer-encoding :mime-version:user-agent:cc:to:from:subject:date:references :in-reply-to:message-id:sender:dkim-signature; bh=0gCxyH4KadB0c8BesV+J+2+UmZG6Ah7Thx6IVdhilTQ=; b=BTalpleO8nSUUWs+ZGJAL3UljZqiJiuWMmvPe7DrYU8jD+yAm7R1LBHzch+z2d8qOv WNo1ZhGDe+vPiyTzwfITvwjbkegIErVzSbBRs9uws6zxikztIcDFJm0YqRCdpfVTRGHr Bz+mnTK/W4VG2jVwW1FZjDbRgMjELbhnZXW41GStCzQUP7DDGEi8HyYdn08T8XRDF2lh G3RYb73EqWbjRmFd9w8LpkGxwPaSjFKVhLRDNZPtJ/n9mJZxn2/UKoUrsHLftEcse1bC WzFbqHc09PpL5oGvjmwPgaMl6VwsxajGWtMMEvNVt1psZjm6E6HY8WVfdu0K7Ai2dQGo UqZA== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:message-id:in-reply-to:references:date:subject:from:to:cc :user-agent:mime-version:content-transfer-encoding:importance :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=0gCxyH4KadB0c8BesV+J+2+UmZG6Ah7Thx6IVdhilTQ=; b=S4eQCeJqyqu0+M8ycBebwvuPNmPiQd2rCilT1hDDGpr1ZJFssThTYGLdcNqWGkro61 aeOu5BlXrOBh3yE+T9JgZgF862h9MGWgxiebu/gBgUOtG5h6te6LnU3g3C2k43Ho8v69 NnvLdfURT8BnvsvsQGKCF0FvQdBomcJ4b5DYsbjfEZQ0F6kHyq0OeX6uEgcW3TUo2IE2 H6UTjHkr3tsP2I1b3kYCmgZ3kfPB5lBSRF9XiB59BJx04NcS7JHCXmcSy8edwJhxWmj5 3Mq/E+7GuadvjmbEcgNENWrtgg1XPJFkWwtwStYB5Rclr6BOvpt5UYaomjiPJqdQ8xA1 tFJQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:message-id:in-reply-to:references:date :subject:from:to:cc:user-agent:mime-version :content-transfer-encoding:importance: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=0gCxyH4KadB0c8BesV+J+2+UmZG6Ah7Thx6IVdhilTQ=; b=k4W4X84HKfb1iHVaLcHcLMxowJk8Ph3ttslnWSqYYq2khPPVuDNgSSh4jUD3PUuozl hIbbOFZ7xujItFcZbk+dDGOtY9Xax1NKQ9ZrdPRB8UwKVnY69UFqSpFH5S6Hka89+2jJ PqCY96kOvTjteJimRyb58jGkvFX421L9NCqgpeIvf+/O5hCvTKv2xCRHKyLcChCpqSCY 476cSMiX4iuDyBL7NJMwLS6wJHNCQkStLwSSbJWlFuwiBkMIHaq8aq/IYIfE9LG8E7VB v9amr7onegueU0M5LPsldDMmhrrgquZ+KgDEUiLHIZ7KGIZ9UTz2v2TBRddccAcDFsby Mpmg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaOn+njchOklgIGAgaq60biKz5LY6BkIXZFWjFGjJIaiuzwvnDK ++MRL7++j6P9Q/j7i6hkqGo= X-Google-Smtp-Source: AHgI3IYShIdC6fT1WMx1q/YWrgZd8yBcWcDxnpELDZr9xoI0dlWRwNk7uaCep+j3d30q7QxIImETfQ== X-Received: by 2002:adf:8206:: with SMTP id 6mr141824wrb.4.1550403305606; Sun, 17 Feb 2019 03:35:05 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:f506:: with SMTP id t6ls1360032wmh.0.canary-gmail; Sun, 17 Feb 2019 03:35:05 -0800 (PST) X-Received: by 2002:a7b:c207:: with SMTP id x7mr1227857wmi.5.1550403305120; Sun, 17 Feb 2019 03:35:05 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550403305; cv=none; d=google.com; s=arc-20160816; b=VTovyaVDHuAGVISKdpxnRyf7SJI2DsFp9k7wurLZGdHsNuBMC57N1pRjffajDCY93t RMrqd9SxQaPPLz6Sqyi5myg/hDGRNCNfEKadOab/agzhq0+0E5knKvBJoCr/zmhImkVb 913ewT7JVDi2WNt1SF9G7YNWZw3WP6eqtbvo7zniIBh3SS0jZdr/eK23WLqony1PbVwR +bq2QBpUabpz6NDYq6QnYv5P33TZPl851SF49PLylXWf9JZYIwm6qxHmFODq1zmVQx5A a446vnOXvqtUmY5qz7eM6CURyXoezME9vAk59LbUYxrRFoY01wd7fP8AD6DXOQFrufvA Ysjw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=importance:content-transfer-encoding:mime-version:user-agent:cc:to :from:subject:date:references:in-reply-to:message-id; bh=zv7Y5zKENb+IfNNBFaVWLaGVv95vuIi2vQUbiU8lHjc=; b=IXbE4YWIKi0+aDre88hib5cZ4fqfQXyXjCtdX9KPU+UfEKq/UdGH0CO/3yBBoWRA5E 3wULys9GMuFdQqGERj3oqA8JCubcZ+l7T5eikrmSbyF+Wv9oVa9hoxM7xYf/Dg1gb2Tu ScHNk3TJMec/v0qBLHmllmJgLBn6hO4BK32+Mvw8qjODDF5MlJwlT+8634+fKV5ZuXQO v69xdcpqAf13HJ206YRkYbQUog3y0wJ73kltxOZPvHdoaEGbCCBMUtQfFTlzEfEdb4hL 97IYgacSexIhXOFVTUSb2LQHozMOKmxBBJJsvsVeHKphrzSt0TycvqMeUhfsfs5vLh0L Gsbw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de Received: from mail-relay231.hrz.tu-darmstadt.de (mail-relay231.hrz.tu-darmstadt.de. [130.83.156.231]) by gmr-mx.google.com with ESMTPS id 109si523352wrb.0.2019.02.17.03.35.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Feb 2019 03:35:05 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) client-ip=130.83.156.231; Received: from mailout.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de [IPv6:2001:41b8:83f:1611::150]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mailout.hrz.tu-darmstadt.de", Issuer "TUD CA G01" (verified OK)) by mail-relay231.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 442Q086KdSz43qJ; Sun, 17 Feb 2019 12:35:04 +0100 (CET) Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mailout.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 442Q085v2pz43pK; Sun, 17 Feb 2019 12:35:04 +0100 (CET) Received: from webmail.mathematik.tu-darmstadt.de (fb04277.mathematik.tu-darmstadt.de [130.83.2.17]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x1HBas9D023610; Sun, 17 Feb 2019 12:36:54 +0100 Received: from 79.208.250.203 (SquirrelMail authenticated user streicher) by webmail.mathematik.tu-darmstadt.de with HTTP; Sun, 17 Feb 2019 12:35:04 +0100 Message-ID: <0c48660f87d8ead6d1bd2bc5e61d8b6f.squirrel@webmail.mathematik.tu-darmstadt.de> In-Reply-To: <5831E465-6CC5-476D-8C2F-43E5B0D63017@nottingham.ac.uk> 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> Date: Sun, 17 Feb 2019 12:35:04 +0100 Subject: Re: [HoTT] Re: Why do we need judgmental equality? From: streicher@mathematik.tu-darmstadt.de To: "Thorsten Altenkirch" Cc: "Michael Shulman" , "Homotopy Type Theory" , "agda list" User-Agent: SquirrelMail/1.4.21 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Priority: 3 (Normal) Importance: Normal X-Original-Sender: streicher@mathematik.tu-darmstadt.de X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de 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: , > For me the idea of inductive vs coinductive or how I called this a while > ago data vs codata is an important basic intuition which comes before > formal model constructions. Types are defined by constructors or by > destructors, eg coproducts are defined by constructors while functions ar= e > defined by destructors, namely application. That is a function is > something you can apply to arguments obtaining a result. Lambda is a > derived construction, I can construct a function if I have a method to > compute the result. Similarily natural numbers and lists are given by > constructors, while streams are defined by destructors, to give a stream > means to be able to say what its head and its tail are. And that is > perfectly right Sigma types can be either given by a constructor or by > destructors so in this sense they are twitters. > > There are reductions which just means that certain type formers are > universal in that we can define all other from them, e.g. function types > together with some inductive types are sufficient to derive a certain > class of codata types. That doesn't mean that the dichotomy between data > and codata isn't an important basic intuition. > > =EF=BB=BFOn 17/02/2019, 09:19, "Michael Shulman" w= rote: > > 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, coul= d > be regarded as another argument against treating them basically, or a= t > least against regarding them as really "negative" in the same way tha= t > 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 function types are neither inductive nor conductive. Only N-> (-) ist coinductive. In presence of function types most coinductive types can be implemented. Maybe coinductive is a style of programming but nothing really foundational= . Thomas --=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.