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-ed1-x53d.google.com (mail-ed1-x53d.google.com [IPv6:2a00:1450:4864:20::53d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 978f7f6b for ; Sun, 17 Feb 2019 19:36:16 +0000 (UTC) Received: by mail-ed1-x53d.google.com with SMTP id u25sf1082104edd.15 for ; Sun, 17 Feb 2019 11:36:15 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550432175; cv=pass; d=google.com; s=arc-20160816; b=IUaZDjCgCgO76snKXywSLFNSrbBg0PGKMTzBSA9kn4P00X+gTS2ehC0eLrb8b/Gedu znjVCExjPRJHngH/Q4iO6BFaqg/q8JQCHTxYUWNEqlGNILx4lOZD8A2LgPa38Qd/HXVs eK30b1bRVjS0JUkem3cgtxM/khoftDGC6yzCSP2qd5oHWQ963oRkIJlZDL5S3upDukrq nnxQhLFQ3jN4JmGBXfcbstVhyeB93pPuOvMOCUzb0+6SX/AueGXphc6IHnO40Mdx/SZI IjQpvf7Fxotdc2OVxUUfUYJTmQdgo1TAvf6gE18bF2w6WnV0a1sk7qiNGzua/NMzdPrS eQpA== 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:user-agent:in-reply-to:content-disposition :mime-version:references:message-id:subject:cc:to:from:date:sender :dkim-signature; bh=C/6Xvas/QbxiCNaXjdKifdLGm2HUxIhuiXCdDxdzwaQ=; b=MOF4+qvqoWF6/fDKhCfwCkmmByBq4JCLJB0ha9g5zpkvg4pnZ6Nc8BEoCOW5TPYY6a lvTiq+8eAB2P299e9miPIMcGMyvEdqczJ+GTSd80DfTNKDp7T+wkPp1tkGzYWsTLpJ5+ R73ebdlr7cQUDCQCym23yTZFAs8CsIgy7YZVGrCVL/+VfbGb1MqCCH/TPn7ZgQhIQ+g7 e5SkgiBK36n4SmshTDQ4FJCvaslOQNP3jpX1krAAeGUlmWy/AtMAiG3xsxyGruXMcqz9 004XpRzxh5jBGrTO8OzChAfOmXOwBptFHXcduHloe39zNo05NlHADJg7/l7lE3+OXcRJ ZgDg== 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:date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to:user-agent:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=C/6Xvas/QbxiCNaXjdKifdLGm2HUxIhuiXCdDxdzwaQ=; b=QtfM7NAjwZF0Agdcqek4cLOoN2W9cwRTzgKQMKs+ktcc8PB+1BbZ3UU4CS0cfpb8F/ frQ2W80aM1mMZL147g8gp1bvSzB7U+jiMRTKUSuNfvpeMjdwKJbPPuDVO4yTkUiZxjj/ 8zjZdPqPG+64x2JywuEa9kwwh8MPUbpbunP4NI+RQmgP6mttueHAKU5axdmXFNEVx0PZ o+j6qkvlxfAoFB6UXvECZ+UOpU21zZQRZyttWvQuP0LsVqElHg+pA4Hi0P97yk1M1cR3 5Ud7+8QFKz/QbdM54ETTA3Mv+UrKt0RKgEMsyqksC0aMcihekTsGPIfKqWMeX1OI45w5 zptQ== 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:cc:subject:message-id :references:mime-version:content-disposition:in-reply-to:user-agent :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=C/6Xvas/QbxiCNaXjdKifdLGm2HUxIhuiXCdDxdzwaQ=; b=D/m8MgIP2XAxff1DvM8UgCWTecJ6BfwZbqqYqUZ6e4AiMYJ8DOd5GQijXbjF/8cLS+ tQN+kpmevO6HgsXhMj0g5MAd7vkWmkT3UZNieptbCvCyjtQFHXygDQnt0IE9C3K6y/Rg uTuvUfJekpeThXheWMppqP2y/PpQKdEa4mvEAyBq9TTpFg64cSNEg6jjwcD+2Ddm3QZ5 9jy9FOCUnKTN2McnajQXvH63vk2tYBZPumTmnT0Rfi0PYtV+hUlSarUythdMa836AqkH P0wNQTWP8DQN1omLj1MiEd6ohG1FEILM57j9LUNzzBgrOasVYI/qGmYbXOGxaTBIBTbO sffw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYZtQGwljM94Ktxkv1b07ct4O7EObui8VerBAUZM+CXut9ul4mH pbHc1P9NooTlKPfMNHrLjO0= X-Google-Smtp-Source: AHgI3IYoTXGNaijbkJ1Lyoi4ihQIbQLHJKNOccOa60WwI8/Wy96zBTClWU7UaiQqR00TKKwWSNFQIw== X-Received: by 2002:a50:986f:: with SMTP id h44mr65309edb.2.1550432175482; Sun, 17 Feb 2019 11:36:15 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:3555:: with SMTP id s21ls2127295eja.3.gmail; Sun, 17 Feb 2019 11:36:15 -0800 (PST) X-Received: by 2002:a17:906:3286:: with SMTP id 6mr2012051ejw.10.1550432175015; Sun, 17 Feb 2019 11:36:15 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550432175; cv=none; d=google.com; s=arc-20160816; b=ZJ8YUuw8KdG1dGOLFczNjGVbJAgLPqGABcelT/FMlhX9lkF/KsrG4KACndl6XxCJGd /ncM1W4XwWSYF9us1to46uZKrXqTjQuSgPP/dBmkKNtTKbXI8ZTbdBRKGK137EzBigFQ SGvSgxIm0j0JwmLWtbnneGJM2XDXJ7hGDPNB6MQAhqbZEBrD44inC2VJ/A1QldHZJPUT SQ91Egd/7DOzqjGI3GY7HrdGE09CNnFQwyoxDelBzQ3uZeGChh9SJkXz6+ZJ8Oow4iTN STaMIb1vV0bGDpFICfNcpvjJoSYrlrdVB9Cv6m+L+5TlSjRUvTR5Ge/lPfCXkLqv2V5I 9x6w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date; bh=TDP+6RIiWivkiAsx34r5r0woileioxyq2W+DNW8y3Fk=; b=QDvUvYvzOFWM9i5z51kHvQKD9MtDjojbK9H2Fdpgjn4ix5rP00HhiGJj9eq1emqfg6 LsEYV/4facbjIjDoJocMm2SEeKl7H6lr4teTl7JH6y1GXBYUnFvFyfFqZ7/IRFQFpRvU w9YrbDhW6b9VqtMk9M6Iw6k3jorO++JyzH5yqpCshepgtlgV+8NJOB0FM/4DuxDMk4vB 5cpHO68LWEwjH5BmntZRiX3KbBC7/6cpcN+M83a3XBaGAHy0sz3Jk3jerbB0ni7Ruy7a 4NfovNWjenYhh+yfj+7OFz4V0FkBJDSBMLGOBLToUYIqdhLAp8bTDtu9Zav5VRAD9Ib0 cMEA== 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 i17si456550edg.2.2019.02.17.11.36.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Feb 2019 11:36:14 -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 442cgL4L1xz43rh; Sun, 17 Feb 2019 20:36:14 +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 442cgK3wkCz43pK; Sun, 17 Feb 2019 20:36:13 +0100 (CET) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x1HJc3Yo005033; Sun, 17 Feb 2019 20:38:03 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 2EC0BC5D18; Sun, 17 Feb 2019 20:36:13 +0100 (CET) Date: Sun, 17 Feb 2019 20:36:13 +0100 From: Thomas Streicher To: Thorsten Altenkirch Cc: Michael Shulman , Homotopy Type Theory , agda list Subject: Re: [HoTT] Re: Why do we need judgmental equality? Message-ID: <20190217193613.GA676@mathematik.tu-darmstadt.de> 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> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) 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: , admittedly, by coinductive I understand terminal coalgebra in MLTT even function types are inductive though that's a bit of cheating in my eyes so I must say I don't understand what you mean by codata types technically I know positive and negative polarity in the sense of linear logic people presumably, that'scloser to what you have in mind thomas -- 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.