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-x538.google.com (mail-ed1-x538.google.com [IPv6:2a00:1450:4864:20::538]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0097bacd for ; Sun, 17 Feb 2019 10:52:49 +0000 (UTC) Received: by mail-ed1-x538.google.com with SMTP id u25sf754204edd.15 for ; Sun, 17 Feb 2019 02:52:49 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550400769; cv=pass; d=google.com; s=arc-20160816; b=KUYxiP7nVpdQjhO4NadG59XKeT+Bgdk78AZZ2CDsqWBXDh4JKPfjw47BuYbReF3AXG 4I+LBIhHh5bQXnt1PYZCF8+XHG7N5uIskpAC01WdANYvAYTYbYGvEJSJZzd6WP1urln1 BN6gG2kACRxStaqMAWF4sGWvxa6ujquGJIg3ksXgrxjOwuz0KlFyDI9dgTB7Q+8ntjNz om5vZ2OWD425HfsmU4QPMLhvEcL9Yd3u4u7tz2l0seiBrzdBT+O8XeTK6Su/6vuHmEsA Qdyg/E6QZBHRG/kTDNs2cC0WJPDdLQYrM64Xjdm2kEzqmXs0V/ADZBKt0sZlvIaWVrJY 9zTw== 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:mime-version:content-transfer-encoding :content-id:user-agent:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:cc:to :from:sender:dkim-signature; bh=0lMOrejsBCHlYjmPd0B/85x3RP6Gu02JityB+1qAXfU=; b=G8DjVewZfhls6Wp8xeuHPlT+j6dq/1VW9v5HDVTvZlm5W8By0lRB51mM9Y0mE9PyNm B0ZLU6WdrT1VgV/MKTwAKRKbVy60ymwAr7W4IJZ1VeiPwj+kBmu8ltIMtiBaav9PXh+V gL3lKurxeLwOeU13tLYf9Ozxt80O2cvJmtYj/Dsw5Ak8zGiPD9Kd+MkMhfgkFFdAWLI0 T7V7D0kiFCs5zci+7CytUMRa+MKN3Z4Te/SIrhe38pivpw1DTQvznG7loOwZIOox5VPz Y4Fl6QL70ujgnHyyyL7Ailzf9bCHRcrR1HFPN9RG+RXJ6Ip4q2819+RJ4I5Lz9fu1Il1 Q7pQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :content-id:content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=0lMOrejsBCHlYjmPd0B/85x3RP6Gu02JityB+1qAXfU=; b=rwQ1pjoLST1m/fckk1eGzdduq/Y6zqBEy1vPOAYLMIUaDg5cq7KxqnTY4989f5m0wJ 47MKtvtHdVWUTNHmq/kMhekpUW610OG5exDhgl+NlmOwtlPQHg7mFF1ghA+7C6SFtiL6 4bo+wskJOQvaHNpjE/yW7ftASahykfAaYPpa/8RLCm2Cs/kZOMxZQ/tiJ3Knm7pYOhQA uUCcX8Mbrrj7sGuJ2JYfpig4PIl2ffJj6y18AMd6XemPTvCHcOWISUTGi6vn83GsQ5YX +bEUIVnXSkeZcZoTaLIH380AR6HwANQBAAh15cbwSlwYap+3VMH7+75jhwEC6QOIdnld hIcA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:user-agent:content-id:content-transfer-encoding :mime-version: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=0lMOrejsBCHlYjmPd0B/85x3RP6Gu02JityB+1qAXfU=; b=Szh35vTp4COYQ1rkS1n/BrmvhqJR9xou+Ii/7wX9RFvSEaNXnO8PBVWf9ZNpfcmrDN oUCIATm8WFXjOp+b3SsLgaeaj0AZfwS9ALLBux3BdO8JJlcslVPRYrdj4RgD89qJnHTB HRsEqCvrh7sYE5R/C5fNOwtW+Impq3oc/87ovXPNC+4nU6oMKVYA/XnhCRCHN448CprS TRmgVe+hXr9A6z9OIw2ZkTTBhCiOFkVqaabb7MXLdcDVwDr06wGNXQr8YzXQH72GCQeG Pnri++O4qMY7wITHKYbW44bSQwdR6djBmLBY9m6Nh3/R6bwiUuOGgGeUB7krNt9Ul5tW CUNQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAub7PbqeoQZwpOjExtjNlgDnl8Q+kCkEPmqLntIrEo/0qBJjirPO iPKHZ/pRkSHOxTnVFjs77ag= X-Google-Smtp-Source: AHgI3IaIhTjS/t+gxNdnk/fFmv4I3otRbsmbflucqGhF4g/DCBKFxAfjG6Y6hztf/03G4tLDNbvlgQ== X-Received: by 2002:aa7:d286:: with SMTP id w6mr58478edq.6.1550400769036; Sun, 17 Feb 2019 02:52:49 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:358c:: with SMTP id o12ls298103ejb.0.gmail; Sun, 17 Feb 2019 02:52:48 -0800 (PST) X-Received: by 2002:a17:906:f82:: with SMTP id q2mr1882552ejj.11.1550400768457; Sun, 17 Feb 2019 02:52:48 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550400768; cv=none; d=google.com; s=arc-20160816; b=AeWv4ZysJc+Syw1ZnW2uMs4uEdp4RBV/4LPkeuXM8KulQEhlnQxPXkc64j8Kro0OME KE6/0nN9b59E9AcBLZOJJmaSegl6um6cjYitUsZBkUqVEmzNd+KAOkMWiZH94zN+L4y2 o1gYDxF3P3hsQqMjoDF20XEDM9rZJ3CXDYw658/2co0S7FzQ+Rse1kd4ZaOKGIzs2NU2 MrIdaIzg8NZquvnuUzH/OutT/SV6OOgQ7IoE0Mkwz4OV/jPJthNdPG3prnSGcDaFYUhT 6ICT74Ahow1gSBlhG2Ytl9ojgXo0NkOQTVrkafRHwp/1qG66v9/Ph0EV+uTTC1RrIRFm p7+w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from; bh=FGcGm9jiYLMr3CVvKj0KgXL34NwxZ7tv0jr08kens0k=; b=RxhD58EorreT+IDQaEB+PJyx5VEy8x5mH9Cl1Ue9/CgzSQbV4qfzNuy0JLPsanD1QF CH1oiTtv/6hYysVJ+crnHH8GxIrrZNmjhc04/FDlja4RkEiVfH+fQUoyQolJBkKRtOwP /y3VrCUw7fWsuNJBfnJZhlLrZlGNB6GAhWq0hMb2oYNBkThFd6R6f0DgMKaEPNBfMjU7 SkRcai3gB4HQJThxqXg8oHJkKWJbYEGjjd7/wJ5UJtvdB35OmmTnYjVlguKF/dwM3rMA 5WdaYpAiEdW1e77Ie7gUrjSdhl71G5XV/qm+ImP260iOepuWPBx/TAP+u4B9BK0qwVqb 2DtA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTP id dv7si142062ejb.0.2019.02.17.02.52.48 for ; Sun, 17 Feb 2019 02:52:48 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 123276CE6C7_C693D00B for ; Sun, 17 Feb 2019 10:52:48 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id BD45C6CE63B_C693CFFF for ; Sun, 17 Feb 2019 10:52:47 +0000 (GMT) Received: from [10.159.172.14] (helo=UiWexEDG02.ad.nottingham.ac.uk) by smtp4.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gvK3z-0000CX-NQ; Sun, 17 Feb 2019 10:52:47 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Sun, 17 Feb 2019 10:52:47 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Sun, 17 Feb 2019 10:52:47 +0000 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Sun, 17 Feb 2019 10:52:47 +0000 Received: from EUR04-DB3-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Sun, 17 Feb 2019 10:52:47 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5839.eurprd06.prod.outlook.com (20.178.81.88) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1622.19; Sun, 17 Feb 2019 10:52:45 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::85b3:de9c:4991:b687]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::85b3:de9c:4991:b687%2]) with mapi id 15.20.1622.018; Sun, 17 Feb 2019 10:52:45 +0000 From: Thorsten Altenkirch To: Michael Shulman CC: Homotopy Type Theory , agda list Subject: Re: [HoTT] Re: Why do we need judgmental equality? Thread-Topic: [HoTT] Re: Why do we need judgmental equality? Thread-Index: AQHUvaaYYqfVw+3Xi0mp7irBTonfqaXSKVkAgBB8egCAAJ4wgIAAbUwAgAAW9QCAABpGAA== Date: Sun, 17 Feb 2019 10:52:45 +0000 Message-ID: <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> In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.15.0.190117 x-originating-ip: [86.28.226.182] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 4cca025d-14a9-4d9a-57b2-08d694c60c9c x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(5600110)(711020)(4605104)(4534185)(7168020)(4627221)(201703031133081)(201702281549075)(8990200)(2017052603328)(7167020)(7153060)(7193020);SRVR:VI1PR06MB5839; x-ms-traffictypediagnostic: VI1PR06MB5839: x-ms-exchange-purlcount: 1 x-microsoft-exchange-diagnostics: =?utf-8?B?MTtWSTFQUjA2TUI1ODM5OzIzOnpqVW1laDZ5akx3aDcwaG9Dcllma1YxMW9Z?= =?utf-8?B?Tk5LK3hCMlB6QjB2ck00cS9yZE5zRFpneVhSRWFJeGlrWUFtcGlsNmpUclNV?= =?utf-8?B?c0FVZnBPOW16ajErc3RzUTJrTldneVBWQ2RsclB3ZVZ2MmRMa3hvdjNqM0Vx?= =?utf-8?B?c3VieEkzdzRadnJ4WUZGL1RVd0JGTGtRaXd2VitIOTUrcWtaSEt2WTc1eGpz?= =?utf-8?B?eTkxZE9GTnlNdDJuYUM3Z2M4RUgwcG5pemhlUkQzcXNIYzdBZGZhQnVSSHlY?= =?utf-8?B?VFFkbVlKUWFDNklaUGdmVTdxb3JxNFhtZ0s4clF6RXJRME1IK1VYbUhMbXZI?= =?utf-8?B?Y2haaWtjYzU3UG9qZ1F4UFZxdFVXZGtFNzRZNWxXVXNKTjlqMmQwWGpQUDJS?= =?utf-8?B?KzBFd3NDcHhab3hwanBIRlZ5K0lWMlFmU1RmS0crdDhLd1Q0Z2dWREEzMnRH?= =?utf-8?B?eFV2UGMwb3o3a21tN1BzUVFFYmhNbis2Z0R0OXFpNEVpRWRNUnZMcGluZG5Z?= =?utf-8?B?RFE0Wm9hY0Fic3lDVEdWMDlOT2Z5ZE1WcjUvYlYrZ05TSzM4SXliWG12SGpF?= =?utf-8?B?b3J1aWFDV3VqRGVvTEs0MndlYVMrRk5ydnYvYkhiRk9OcDBDUDlkQ25INXhl?= =?utf-8?B?TzQzS05LcGp5MThNQXNKYUFCa1VWdGtrVVVMdWZzSVZQYVBaK25EVXZhWFpa?= =?utf-8?B?enpPWUk0MlFLM1dMT2JrSlFzNUxySmxNNFRqUlY4ckF2WGxNZTlXSXJhcVNN?= =?utf-8?B?L1JReU4rUys5enpRcU5pMFB4MmhTVnJZU1lrNmd5U0hVK0xBMHZqaEtRZWF3?= =?utf-8?B?RC9ENHpzYTNCdlpmQ2xDRS82eGVGTUZLVzJZOGVDOTBnRTkxK1BSaktoeU9p?= =?utf-8?B?VGkxckdWM2R1UVh5NE5rVnBFTW5NeVE5d2gzQi9SUHcyKzU1VlNZTkhEUGQz?= =?utf-8?B?Nm9UcXJQVXpOUW52R0lUaURpWUZWNys3aG1MRHMyc0h6YWhWOW4xd0I4TDFC?= =?utf-8?B?cXl0dWJTbTlWcjdBcGQ3b1Z4b2JPNmxzV1VOcDd1SWFhMERZQVNRVVJaRUFP?= =?utf-8?B?ME1xcE02VFIxd3g2K21IaUtWcE9tK0xBTE5tcFNCODVHaEViM3FpWUNiSzlV?= =?utf-8?B?enVkUXZvelprNzFrRklySWJNRldVRmJKRVhLVlh0ZE1saWhRa1BlQ1NwVEhO?= =?utf-8?B?bDdjTDNFU3h1c2dJcTVaWUxWSDU1YklCam9jU1djNko3ZGgvSlV3VWljc2p6?= =?utf-8?B?ZnBJYUh3TkJOOXNLUzNTaUFYcFRKOS9HS0d2Zks3aitsUm5PRU1EQXZUZWRt?= =?utf-8?B?djA5L1FKbkdkZXl0bDlNVGozWmh3SWJtdTNQRG5KZVhaa2NqVkZlRW9hUENG?= =?utf-8?B?Vit1a0Z6L3JqTDQ4L3RZOVhjZkJNSUpxcU9YN0VtMnRsSWlNa1hoMEdsT0pB?= =?utf-8?B?Z1BsVWt3MzFzakJTSkNrWjkrdHBmTk1pRVZLTVYraXVHZi9uYnlob2pvMTI3?= =?utf-8?B?TndTNkgzeHBUREVYYzNlSm45bmFpTW5BT0FRVmtEY01ZWTJSME9GL2NBajFK?= =?utf-8?B?dElGb0w0SzRtSmk2SU5yUXU0YmM1aVNLUFFoWm9uUm5DVjE2UTlNN0dvS0sy?= =?utf-8?B?Smx1N29MUWYzRzBhTHFFOXhUM0R6WWFyUUQ0V1VqRDd2WEhiK244eXJRTXc0?= =?utf-8?B?Skg2OWFDRFdzbW1FMzRacWxmajRIRjNtanBHS1UwNDZhdjhFcEtxTVFYaXJV?= =?utf-8?B?YmFkbGRpUElSVVAzbnpUTWRVWVEzQWhidWdML1hDZThNWEVmTGNwbnpSZm5y?= =?utf-8?B?V1IyMWhTZndqZEtYbGpQUjU2dDRSSTM5K1dWcFF4SDdLa3cvT0dodWk1a3p2?= =?utf-8?B?S0NjSlhtaXBZV01ZZ2c4dzloMHdQN0FFSFJtdXhVWUIweTJxQUM0bTZpSzl2?= =?utf-8?B?MTlLYXpYZ1RwUXpUeEZOaTNhVDdVbFhqVUJBNU5ibUpCZ2NTRy84WHRSOGE5?= =?utf-8?Q?sQiUuk?= x-microsoft-antispam-prvs: x-forefront-prvs: 0951AB0A30 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(376002)(39860400002)(396003)(346002)(136003)(189003)(199004)(316002)(2171002)(58126008)(786003)(54906003)(106356001)(53546011)(76176011)(102836004)(14454004)(55236004)(82746002)(53936002)(6246003)(446003)(86362001)(3846002)(68736007)(105586002)(6506007)(6116002)(66066001)(36756003)(305945005)(71200400001)(256004)(2906002)(71190400001)(5024004)(14444005)(5660300002)(83716004)(7736002)(6436002)(93886005)(6512007)(8936002)(97736004)(81156014)(6486002)(81166006)(8676002)(6916009)(966005)(6306002)(74482002)(9686003)(4326008)(11346002)(486006)(476003)(186003)(26005)(229853002)(25786009)(33656002)(478600001)(99286004)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5839;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: Wzsqg+jm20LbZONL37yJKFOO144yWIke+GXEPznhGzVc6/+RM6tXNiUKI1c60ITeugDG/f6sRHTNS+ngFFiT3Y497CdWwX1XC2HbJ2ESXRQlpLL62FjaohkEqeZVScOt1FW13t0tUpBH2XheGgCma2Aa5FTA5pBIc/rGn20+FIoVGZa3P+bLSVSRDTAcsAcacRniLjUbjlq6WS3iVqdpErgm4K6wAY2aQpTZHFGyiUZyG0DS0A1QbxDv2+NrHnWMbTWNKb59pAqW4Wyxx9BoqbF9rfkh3piCqftwk+gLbkeZQPD3XpuvFytd3NgiQDdtfFOzREs1Eqy9/LZm3twZTPqxhahwJwR5ujde5t6TSeCQ2kAsrIqxZFdRg0HphY1APlaQQxgxhQym+kdFjtldgoPp98MGTaSIhEH0eDjcmyQ= Content-Type: text/plain; charset="UTF-8" Content-ID: <936C21F73596E6449CED69C58F2CEF77@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 4cca025d-14a9-4d9a-57b2-08d694c60c9c X-MS-Exchange-CrossTenant-originalarrivaltime: 17 Feb 2019 10:52:45.3620 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB5839 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk 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 ag= o data vs codata is an important basic intuition which comes before formal = model constructions. Types are defined by constructors or by destructors, e= g coproducts are defined by constructors while functions are defined by des= tructors, namely application. That is a function is something you can apply= to arguments obtaining a result. Lambda is a derived construction, I can c= onstruct a function if I have a method to compute the result. Similarily na= tural numbers and lists are given by constructors, while streams are define= d by destructors, to give a stream means to be able to say what its head an= d 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.=20 There are reductions which just means that certain type formers are univers= al 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 codat= a 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" wro= te: 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. =20 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. (-: =20 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. (-: =20 On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch wrote: > > On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf = of Michael Shulman" wrote: > > However, I don't find it > arbitrary at all: *negative* types have strict eta, while positiv= e > 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 pr= oven 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!} > > CCed to the agda list. Maybe somebody can comment on the decidabilty = status? > > > > > 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 Gr= oups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, sen= d an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. =20 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.=20 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=20 where permitted by law. --=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.