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-x539.google.com (mail-ed1-x539.google.com [IPv6:2a00:1450:4864:20::539]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b7aa54a9 for ; Sun, 17 Feb 2019 11:44:31 +0000 (UTC) Received: by mail-ed1-x539.google.com with SMTP id j5sf2300227edt.17 for ; Sun, 17 Feb 2019 03:44:30 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550403870; cv=pass; d=google.com; s=arc-20160816; b=ooc9+Nmwn5RZnflOgBuwXzZPVJyxBSzF4jFkV+Ox+vDn4vdVQ5LArsPS2hzuMZgjyq HDcfH1eVupjkJD+WNBNCyiLt5KtlgDzY/7PmWN+kuVNWiaWkRbHkBQqaHQl28k9y7weK v2vWzj7n1lSA8cDUVQb7UMWyxEmaoPjfuWNwxf4j7mCiuGPKVkhdAxSaRd0laIOZQij9 k4I2XdEsjrv6Ee3VOYXKS2eLPPM2G6QYHvobrlMdI5eeDTgEDSJB3Fey6l0LIOiyCwL5 rMwTtDqhu4dsl9suMeI+q0T69ZgDPCcBTvxqK1gmOqGp0LNQW4s58YkcHRtLY/Uz8Abf eg7Q== 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=+a0XfXSTscZYh5Qd18i+d3PJXPNFPjJpTZcw5JcQekU=; b=Xa1ZuuM9ZxbvXO5qEV8kTFoQliOkjWHcoENo3v6xGUZVHCDv3CB0Fap6p1DXioNKF4 kFxr0AvXqkqrCSAYB+FXpnupM4qNljewaqGrozNSm++O9iRx83UQh7oHYGX5UUTfjfKc JB7SthCjJue9TrRBUw7oGv2oliT4nITRUvg9GBex8/i8QklBmUQ2Do7U0eEUe3zyz43n sIowDwUaCjzYB+3brlge0pPsR/bvII56en26QR0ONZwUhgqSa5fjBiJLZ/hw6ux6+gLt QY++Wm+uItM6c57YljVUYGVCa4AWZU2J/arWcda2ku61Tawu2x5wdvktOnV25QZE/q3I D+tQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 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=+a0XfXSTscZYh5Qd18i+d3PJXPNFPjJpTZcw5JcQekU=; b=Aiwwtvv8FmruV+2ecd/K/JqgbY15P3qI0ZaVoFbSjPEUbnK6/qfk5QUEuwEHjyqsYU ELVDrqFt9YEHKSDsXsFAHA0etyn7hg47QM+j79cu2jquvQyruephBKb4BvYV+aKrQug7 Lx0iSTuI2Xy7KlGQi1agclYKAJL2bSHgm1gogSLvK50eRDfsW5GD1+Zle2xGaF3dwWgb KeoEZD1u10fELpuj70eH1C0Ev0vUHHXUJKQ+Z3IvOCR8yBFb9g3sHRuHfDSY9l/E1cBR +Vn3UCiIa/pt7W5OAOnuS6SHGWp5cVB4AMIscuFxVkN1bvuzu2YyiQvacoQRTb7NzFZv kPiA== 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=+a0XfXSTscZYh5Qd18i+d3PJXPNFPjJpTZcw5JcQekU=; b=F8IfPnXH9rDMLNXTHbR1WyEK0G5XxmSqdOWlPS46ENm/7Bw7zvk1NnUxvGQk9/codW u2DKWpo6BmZ9cVT+bEyk1PVPRfmRxdq5p17pWhFk32QymfSlOk0n7qZdfv2wqPUbyvSl ZiPj3xVc9T/8RNkt3ECQ9m6BlQ0dOTIZiq2krpTC/Hf1wjZXeYmMgpKyzlt1xpr247lA m+c/6deudTBAJIBKp5MW/7lQzb6Txn9e/4V481rPnnJnMrJW9JvL//kxwWbt1m0lirU/ D2z8nzBW4RcKpQyiFM0VkLQAvAUaIOfJXlEWvTRLfV7zCISL/Y3umyzJE/3kQTUHI57D oDig== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAub/xp/bUbw39dXsyfpILnCQlwcVgQDo3/f73wnGKjTozhmGwpUT 61iTrqColpqKFoSW3Tooe+k= X-Google-Smtp-Source: AHgI3Ia/a7gYy5ARS2KpEJCERCtO3vN8clTngrti3jNYI7IGxy50Q4tC2akQJCmSZYZDwv/vQxwisg== X-Received: by 2002:a17:906:410b:: with SMTP id j11mr44910ejk.0.1550403870616; Sun, 17 Feb 2019 03:44:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:3555:: with SMTP id s21ls2002471eja.3.gmail; Sun, 17 Feb 2019 03:44:30 -0800 (PST) X-Received: by 2002:a17:906:3c3:: with SMTP id c3mr1899152eja.0.1550403870000; Sun, 17 Feb 2019 03:44:30 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550403869; cv=none; d=google.com; s=arc-20160816; b=L525huiy1GKQI7XAEqXvycN9TfQlSjDwIDEgtRWfzgF0wMy35rwTOI7Pv6H6vZHOpe kQ+fqCxPbXVYVNbWgA4lye9kTbmL9XNEIyNlxWPJJbus953rqCsQEq7ZJLCiIjhFmvaa CiiipG8+dgt/MJIUMIyrQg/wfJ7e0cytAG2HDcL24JbZ09Gd7ulz3KFNiUNy3k0tHIXq Y4hY0bN9W7XbkaQ/TvY/keDOo1gtqCLJQTtPap0g4zKwtBKryAEuxzYwgb9o3PMw7mmq fREl37huzTzR+6Wl30EROWUL1a7UkwyGa+TWAPYHE0rWFso2ar/V41EgMTGUMyILy5mX FR3w== 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=I+kKgoptE96V2cYfDXa/jNqZHex2iZW6ZcWq7qs3RAM=; b=spIvmjxUKKkU1CctZ9kBwKLPw6fCCbhOwLj58SGtm8qJ6wtLYRosO4c/uChUB7uS7l ey1/P9jlNAo2ZCDaUqoQfL1Y5q4/u8uV3gY8IeUaBtmfc2GExLUgMxv2xspfoKOSyjif +0oZci008Yof1PNVVpEsDVXpfO3Oh67oN9g/PIqjxjvWXaYCildoQr+sr1848oE4D1QV y3kzEYEa8D8I1avSuX6ePM4PvWzr+Oln3oW0WfJgbZc13vkhU+w4DUbf89Q+Jl8Ut97s F01vPNGuiqCAdmvETwgnADKjYaIuJgLbI+KmXurYc1KKQqLhVCv///NoRayIT96+x3nX R7wg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx01.nottingham.ac.uk (uidappmx01.nottingham.ac.uk. [128.243.43.124]) by gmr-mx.google.com with ESMTP id u9si599895edp.1.2019.02.17.03.44.29 for ; Sun, 17 Feb 2019 03:44:29 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) client-ip=128.243.43.124; Received: from uidappmx01.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 9442A3C4042_C69491DB for ; Sun, 17 Feb 2019 11:44:29 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) by uidappmx01.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 6E3093C3FFD_C69491DF for ; Sun, 17 Feb 2019 11:44:29 +0000 (GMT) Received: from [10.159.172.13] (helo=UiWexEDG01.ad.nottingham.ac.uk) by smtp4.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gvKs1-0001V9-8D; Sun, 17 Feb 2019 11:44:29 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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 11:44:29 +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 11:44:28 +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 11:44:28 +0000 Received: from EUR02-HE1-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 11:44:28 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5518.eurprd06.prod.outlook.com (20.178.120.156) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1622.16; Sun, 17 Feb 2019 11:44:26 +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 11:44:26 +0000 From: Thorsten Altenkirch To: "streicher@mathematik.tu-darmstadt.de" CC: Michael Shulman , 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+3Xi0mp7irBTonfqaXSKVkAgBB8egCAAJ4wgIAAbUwAgAAW9QCAABpGAIAAC88AgAACoYA= Date: Sun, 17 Feb 2019 11:44:26 +0000 Message-ID: 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: <0c48660f87d8ead6d1bd2bc5e61d8b6f.squirrel@webmail.mathematik.tu-darmstadt.de> 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: f6b9760c-1f55-474d-85db-08d694cd450f 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:VI1PR06MB5518; x-ms-traffictypediagnostic: VI1PR06MB5518: x-microsoft-exchange-diagnostics: =?utf-8?B?MTtWSTFQUjA2TUI1NTE4OzIzOit2NGJNRXhIVXFIQlQ5MTRwcE9RZk9xK3Np?= =?utf-8?B?cVRRVHVjS3EyUzJiWVpBWVZaQlc3ZCtRSVFmaUw2cjMyNStTaXMvZ2Z5RFp1?= =?utf-8?B?RmpZSVViK1c2STFsM3BxTWpuT2hiRHU4R1ZLZjRoVytCNGx6RWR3NUxmOVVr?= =?utf-8?B?M2FZRUk0YXVEQUJrZ3ZNTkdKbVBocjNGVFo2YjZsYWNaWDByVS9UWGR3dHJU?= =?utf-8?B?QjhJZjhQeUJaK3ZQUHFBTUZhVTVNbS9Xc3hoU0dXY1llVW4wMks4THU5eVht?= =?utf-8?B?OW54U3ZkdTI2V0dmR0phWThsRUhJQzhQUTdnak9ldGZaWnBYL2dGYmVEQlky?= =?utf-8?B?MWdzNU5JWmRzWVAxajdOMytZQWF4RHYycVEzZE8rQ1pOYzA2dXZZdVIvN1Vs?= =?utf-8?B?Z2p1YzdjT3AvK2NydUY5TWdpelNqNmttTEF6Yk9qbzVIczdFay9RNWRBWXl1?= =?utf-8?B?OEFaVVp4Ly9GK0k5U2lyUGU2a2Z1cE1aWVFvcWFsOEFoaHFWYStWdG5hbTZx?= =?utf-8?B?cVlvR0tuOHhXcGtLa2FWK1MwU1Y0aDRpQWRXNFVWbkNhVUZLc0RQV1R2ZWln?= =?utf-8?B?R2FueGZFWllWTzdWeitzbkp0RFlDMWFtQ1g4b3lYVmMrWUtVdUVNYUVnS3Fx?= =?utf-8?B?NDNCTHo0YUFVNHR5NmJTSzBwWWt4YnZSV1VNRjVGQlpDR0lMTzlFNjZKM29W?= =?utf-8?B?TnYvK0hjSm10VmtVVGRaUXRGeEZzaE51NWNqZzNjc0VRRDR6Ulc2VEdtNDhp?= =?utf-8?B?aS9kVDhtSWowNDZKajNYRmM0RFlRQ1JSZDJhTXhDUkgwYTJxTkZPN2EyVEt5?= =?utf-8?B?OXF1U3Jqblh2aTk4TkhzaE5nYjhQRHlTVzhxL1dmczg5WDdGWjNQNmhOZWpI?= =?utf-8?B?QXozTXFQMHdHUGJWUXdWWUtzVFVsQVVUck12UHgxZlZRNmlHSm9YdUp2ZENM?= =?utf-8?B?dWRsK3NRYTZ4elhaTVJnZ252SFBKWEEvdzg3UHpRME5jTFl4VXd6Ni83SXpB?= =?utf-8?B?NEtpaXErOVMrUHJMR2ZzUEpuWSs5V0FVanhnTVVZMCt2NnNxVHFlRGhGK2F5?= =?utf-8?B?K0tKaEI2VDRJL2Q4L3RWYkIwL2VVSUowVllrT1d1Ykp6blM3TWtZVFhOaGlo?= =?utf-8?B?VjlwTHQyQ1l6MWw5SHM3YWxSUS8xQXU2ajlPTEU0VitXMjUzQzVWaUl5TmVx?= =?utf-8?B?b0M0T0ltZHZHYjZyZ3RCVDRzWWlsYkZESkdQMS9NM3lXaVZKQ2VhWUI5eGNR?= =?utf-8?B?VW4xQ3JOc2ovclhmVE9LZnlRcjV5YVlOcDA5VENkNEZUcW5mRmk1REdzVHlm?= =?utf-8?B?KzlUVG9mVzJUd3lzQVVOcGFSSWxZUTdkUEx3dTRMYnBJTkhJUVBnVFBFMDlS?= =?utf-8?B?cVQxMkU5emFubEZ4YUdRdUtrRWFjNGRobEEwa3JLaGJwUEFacnZBVCtQTUQ0?= =?utf-8?B?N29GeDRHV1BkQmJKck9uWUFsSzI3MUhoVG85azZpMXZURnY5amhRVmt5Z0h5?= =?utf-8?B?eGVkcnVoSE1uVlpiaGVTb3BHMlF3MFVCZHFhcWE0R1p6Y1JCNGhsUGcxZjBz?= =?utf-8?B?U0k1UkR0U3owbG94d0JSK0JzYUQzUjZ6VFB3NXMzVGVsOGdKMmRXTEYvam9G?= =?utf-8?B?UnFlOUNFYWp4QWRxWFlicm9tVWZwUjhrNFlsUk1lRzlSTnIzMU9yZGVlMG1L?= =?utf-8?B?UzRYUlVpTDUvb0dyMkZURHk5OEpsNldTWE83a1dGRlBNd3BiVm1rRksycHN0?= =?utf-8?B?VWs1RU84STlxd3BEVXhFeWpiOVlWS3hmK3IvQ2lNTEdVbHE5eUEvaU05NDB4?= =?utf-8?B?NDQ5VjU3VmRieHloTzdEd2NNY3lVNVNubTdlWUlpc054bXRlWWJnbWNpRFpR?= =?utf-8?B?cjBlaU92ZkJwbkRRQzJacVFuQ1dEYWdDTERtQXp5MnNYRXc5YnEydWtCNk5r?= =?utf-8?B?T1FnZXY3Q2FHWC91WVh4a1ZMOXFkbDFEK24xa2xERzlXTXY1TTk2SWJJV0Iz?= =?utf-8?B?emdLUFRJQURGN2ErL1E2eThSU0hpMEdRRkFkUT09?= x-microsoft-antispam-prvs: x-forefront-prvs: 0951AB0A30 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(136003)(39850400004)(376002)(396003)(346002)(199004)(189003)(256004)(55236004)(305945005)(6486002)(11346002)(6916009)(74482002)(5640700003)(76176011)(476003)(478600001)(8676002)(486006)(446003)(2906002)(68736007)(25786009)(71190400001)(26005)(53936002)(71200400001)(6506007)(83716004)(6436002)(102836004)(58126008)(14444005)(99286004)(3846002)(81166006)(93886005)(81156014)(786003)(86362001)(1730700003)(54906003)(316002)(6116002)(66066001)(5660300002)(2501003)(6246003)(14454004)(97736004)(229853002)(2351001)(105586002)(36756003)(8936002)(6346003)(9686003)(6512007)(4326008)(186003)(33656002)(106356001)(82746002)(7736002)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5518;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX: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: //Sg1Z5Xw/avymjdAuwdKQJrNINiASW7MzVIs12BRf8s3XnMzstDM62hisOVLgEIWyIdE+KD1A2r1CW8lrZqFj55Vtukvdnpbvc+q1/w9+jSORgCTEfzv23HYJHd0QiE4FnG7pDi+Nlj4Kr1qs2EGQqqb3z6l5eRqhJY/OTzTsuVRz+k7JzIqghdHFDin3VhaEr6pTUrPl46fxYzQpC+Xq5o8TskJ8pH+yVN5Q0SwRRoH0Dw/A7g4CVEIEbAb7F/wlyoESVoRYThPtQEEqOkDQwU/EOC+PnpfhLHbmkMO8G+L2yCh/dTsfoQfsDd/jsHrbbID/+aPRtNztKsFKbW2ZWMFQp2WIzPyGxJYtmW31g/wtw/ZZf0GkUbNgvMJlUatBDrCe4w3dUPMO2KvPxRT+qCDqWZFfyRSPjTP/9OaQU= Content-Type: text/plain; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: f6b9760c-1f55-474d-85db-08d694cd450f X-MS-Exchange-CrossTenant-originalarrivaltime: 17 Feb 2019 11:44:26.5624 (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: VI1PR06MB5518 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.124 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: , =20 But function types are neither inductive nor conductive. Only N-> (-) i= st coinductive. In presence of function types most coinductive types can be implemented= . =20 You think of terminal coalgebras - that is not what I mean. To avoid this c= onfusion I am using the term codata but most people in CS understand coindu= ctive better. You can define a type by saying how elements can be construct= ed, this is data Alternatively you say what you can do with it, i.e. how el= ements can be destructed. The function type is not data, functions are not = understood by the way they are constructed but what you can do with it. A f= unction is something you can apply to an argument and you get a result. Cod= ata types always introduce non-trivial equalities, because all you can do w= ith a function is applying it to arguments two functions which provide the = same output for all inputs are equal. Hence functional extensionality shoul= d hold. Maybe coinductive is a style of programming but nothing really foundati= onal. 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.=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.