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,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wr1-x43b.google.com (mail-wr1-x43b.google.com [IPv6:2a00:1450:4864:20::43b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4117cf03 for ; Sat, 16 Feb 2019 15:59:18 +0000 (UTC) Received: by mail-wr1-x43b.google.com with SMTP id m7sf5286400wrn.15 for ; Sat, 16 Feb 2019 07:59:18 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550332758; cv=pass; d=google.com; s=arc-20160816; b=KBqovmBAIEDsrsUdr2mNL9ECdZj7rQ06viTxg36lMr4ZdtCddY3odrkKaMabCWoClh rkPK4HEVfXssRCoKCNmegM+oWDDsIs9y7sqirXHGOiuJola1ZPdl3+PcimZdQINzDTWe 2GAZQ6yLQdZwMUVhK6jhJF3dHqEb/jlzou09AGVfUxTWFqD4RudGkTgN4cSA2nIXmVbC yNCX2BVjmoztGpxfKkL6ZjmId3ZZdZifSluuJK7+6Iw+N1hN6owL/r42aWnBGSnxrNlu kB6vcGLMeVcMV2M0cmyNNKkf0qyuyB3qOeZEjeQPm1qV+LpciLC6AIYZjiIhOjeN9HcU USdg== 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:user-agent:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:sender:dkim-signature; bh=i9jV4EFQSFGy7jTpG5iRTVIj0x6cCpgijPlbVyAxMWM=; b=trvnUS2nOIk86iaoJNRnvTJivOKKPppAis/bS7AASQ25V6OZ6WOA6di2izkXMszIzP m7h0/HmM5q6UlhZ3/T/tuivOb0ri2shk/rm+LtqE3QrDXGj0TIeHwu70XG052Wgb3ZwP +qevDmVKDlu0MgCru+ly2QZd1BZAlFXZRyMclqpWh27/a1e9pPCpfS+tbiIZK1R0ijjM zgQjhr3Sf2NiH6XwDZkRn0xHLvHL6Hx827Go1vqUxy3heQDzDO2DhiX4L6ZnSqJ2AD2y sBQ18b1x1arMRVO9HotkzaOOqKsqEg38eipG2akZac+qMzkISVxbZbWmPqjZ5KSyxwC/ 7uxA== 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:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=i9jV4EFQSFGy7jTpG5iRTVIj0x6cCpgijPlbVyAxMWM=; b=h6lVpHr6r1PkqjcATmp2fM0Y/MDH0O3ejauk5+536wMP9coGBVAUaVoPOz2VqB0XDT 7d6fL83sy+4BiL0w/NDZMK1rKXgz3hvcOFiQZO0BDTK/Rw4Up4NElWqq8+ARb0GY8SIN VhxDn7imVgKZ9goB3uiqJ+0UvWEWJsAiNYWFJviRNweqDrJLrrNiZBPZqcV+RduAr+AF YemhFoQDpyZIhCOSlqeEMiKhiHYubImR2xO5YLw3ElQ3FN15ppbEfISDb/CSTCk0Ydvz Ln+dq2r65AGftvm0mwFiiV3ypsrYDn9UhrOXlwoxvZdhwBSX8nV3LTSSsi3m2yEnT2hS 9wPw== 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:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:user-agent: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=i9jV4EFQSFGy7jTpG5iRTVIj0x6cCpgijPlbVyAxMWM=; b=p+AD0cASFVcAN6ctcUqYWxvivp7Tb+V0qyh/4kgMfaixiqR6KvtQgjqEdjqjK8kB5G OUXdc/ydglpqh+N6NYoa+uj0SHJCphj88JxhkHtvOvgrHh2RfLXf4um0X4Y6/6RkYb7M wfebqEFUzcqbCuQoC9y4bxwoA87ZSwSGllYrglY/GYSvDS//jccff2DWmnwZ8H/ywr9i N1mfWDUtGM3pfuHrxjyTwpXOgiW8Tv8wx8AOPlBY+s/9HduedYfV2QliKBJZfNmomeeo +pSbB0P8A6H79E6TB5REbwItEZFw/oXbFQb2Bw//I9e/i+eMt9o76VnSua64RGC57oly vVbw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYQpC876Jb7x2KYgWYzUTCUDRnDMj/dAVLo7Oz8U9gat/hEVn3R iyyeZ6f79i9U7JxwA+qHHlg= X-Google-Smtp-Source: AHgI3IZtK1tZtAPC/pIWv6sB9x4lf7o9kSS9RB3fYbW2u2VSqOsCqZ8K7iIfT6e7ehy+KZGjt0Z4yw== X-Received: by 2002:adf:83c6:: with SMTP id 64mr118118wre.2.1550332757881; Sat, 16 Feb 2019 07:59:17 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:b1c5:: with SMTP id a188ls1126949wmf.5.gmail; Sat, 16 Feb 2019 07:59:17 -0800 (PST) X-Received: by 2002:a05:600c:21d4:: with SMTP id x20mr963921wmj.25.1550332757234; Sat, 16 Feb 2019 07:59:17 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550332757; cv=none; d=google.com; s=arc-20160816; b=J7+Y8AyA0H/rBQH1oArduC1aimFIrwOVWBQXSovPsdbxR6bF1+uSD87d+Lui/vKUli IqT/gOyMNCaTAG+/Wf9G5u/vN4scwKCqiIgHUvsJB59c4lJPiBl9JsAZxZuYDxz3SZkP Jokx0hE4vpEDL0vRcHSf9UU9L7qvS694v1EhqxasU6Mh4CWmef/8Bcv4l8hCT01rpPDV yCr0H1BS1l3V0XQBJm0Fi/cuBX7o3ECf3KiqH7Cu0QxZEiDNL6dyJys5LZW7GX4EBUWr vBfGhVUmmPtK7zPrimskXCZ8hdYjDZaMEs5cZPEuf/KWnUsl8ZGQUPv00jyP/eAjr6uy IgpA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:user-agent:content-language:accept-language :in-reply-to:references:message-id:date:thread-index:thread-topic :subject:to:from; bh=rdGVu33RWGD/7ElWQ2MCgK+u6AFuOMSW2JoXmIEsjeQ=; b=vIuPLvfTzkGZYKcDFOYpBhu+M52TwagkqhuO3x2UBuvtpndeCcKmv7S4RNnsTuvk/J J/kiwGoZxbJGA/Yc5HZHU3LrIIwUlpTqhTKg9b2Oqgd3MBV5ugmDTJLcuWKpe7s0sEs3 KK1IUoO2KcqssW+qpCnk2Y9ASQdfbJMLA1gapA/jPmXO7/pBdZZTPcquIeYVx8ux+/rv G7widCmQr5CXs+qp4m3kI89SlY9mbS8kUaq37ToEMvUSkKmFBfq9TtDYlT9Q5kKKyjOe VVt/NPDvN8haltolFBCd3wWUEiQ3LHQ1z5h8EQDxqoJ1pb5tPCahJqc1xkoDDozY+/C7 YcXg== 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 r15si161164wmc.4.2019.02.16.07.59.17 for ; Sat, 16 Feb 2019 07:59:17 -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 E7EB76CE649_C683354B for ; Sat, 16 Feb 2019 15:59:16 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 7D2986CE64E_C683354F for ; Sat, 16 Feb 2019 15:59:16 +0000 (GMT) Received: from [10.159.172.13] (helo=UiWexEDG01.ad.nottingham.ac.uk) by smtp3.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gv2N2-0007dT-FY; Sat, 16 Feb 2019 15:59:16 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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; Sat, 16 Feb 2019 15:59:16 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.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_GCM_SHA256) id 15.1.1531.3; Sat, 16 Feb 2019 15:59:16 +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; Sat, 16 Feb 2019 15:59:16 +0000 Received: from EUR04-VI1-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; Sat, 16 Feb 2019 15:59:15 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB4176.eurprd06.prod.outlook.com (20.177.56.88) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1622.16; Sat, 16 Feb 2019 15:59:14 +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.1601.023; Sat, 16 Feb 2019 15:59:14 +0000 From: Thorsten Altenkirch To: =?utf-8?B?QW5kZXJzIE3DtnJ0YmVyZw==?= , "Homotopy Type Theory" Subject: Re: [HoTT] Re: Why do we need judgmental equality? Thread-Topic: [HoTT] Re: Why do we need judgmental equality? Thread-Index: AQHUvaaYYqfVw+3Xi0mp7irBTonfqaXSKVkAgBB8egA= Date: Sat, 16 Feb 2019 15:59:13 +0000 Message-ID: References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> In-Reply-To: <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> 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: f22ebce1-a520-4d9c-1bb4-08d69427b2cc x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(7168020)(4627221)(201703031133081)(201702281549075)(8990200)(5600110)(711020)(4605104)(2017052603328)(7167020)(7153060)(7193020);SRVR:VI1PR06MB4176; x-ms-traffictypediagnostic: VI1PR06MB4176: x-ms-exchange-purlcount: 1 x-microsoft-exchange-diagnostics: =?utf-8?B?MTtWSTFQUjA2TUI0MTc2OzIzOkhCL3dPM2p6amRLbWJnc3kwK1B3dlFaNzlh?= =?utf-8?B?alNUZ0lTa2dWSmIySUFJaW45ZlRQT0tIajRhNjVGK3NhRGdmT3V6U202L1hk?= =?utf-8?B?cGpvZHkwbG5Xd29xK3VUR3FveHkwNVBnOXFFMVU1U2QxMkZYa2t4MWlmOEhT?= =?utf-8?B?R3kyNG94Yy90YTBleC8xR0ZMTFRJMDFncWlYL3QvalpqeStOS3VyOEVTaTRz?= =?utf-8?B?S3Jhd1hTUTNCSUE0N2lOVjVNTnU0dzA5c0htZHdtNi92c2VqQkNFLzVKb0Va?= =?utf-8?B?WWZIOTg3Y1N2ZDltdjI2WURZNm5aY05mYjI2VEtPMi9jQWhtRzZZcFNSM0RX?= =?utf-8?B?TUZPL2M2Q0xZeG5YQW55aUhoWnRDMlRKV0pFNTZPYzh1VVdPUGhmaUNXT1V4?= =?utf-8?B?RGJVK3dGaC9IOHoyY3IwaFFrRVVZUVhzRU9KZGh5K3l2Y000NXJkeGRYL3g0?= =?utf-8?B?anNQaUtqYkpsZzNGVm1xcW82Q1VvMExkdEdIbjQ4RU5tbDZ1VUxLVmdCcitH?= =?utf-8?B?c1pPQmplTjBRSnhqcjNjV0dWdkNJbVBHVENRQTlQUEQwRVduTjZsNUkyNGpF?= =?utf-8?B?dU9LZUJnUTVzVVpFbVYxNHVtSk9BZGFKSU1FYU5JS2xVWlZuQkhSNjgrMzhU?= =?utf-8?B?bE5xYmFnVDRVV1RlNW1FQXorZ0FUajlDQ09mZlJCVnNOUU5RRjB5MVBJWWVU?= =?utf-8?B?SFBONzFuSDUreERTVjdINGJUajFvSHpCdG5ONEZmSzd5RlIvQkRBNWVKOVBW?= =?utf-8?B?NklQOGdLNjZjRFN2RTdMbVN4V0xuWnZHTmhkL3NmVzQ2ay9udGFJRmxKMmlC?= =?utf-8?B?Nk1Bc1Y5OVlta2M3aER1aUtqekVvTE50V3kxZ0RSR213WVBTNUZ5WmYzZEJl?= =?utf-8?B?eEZIL1QyQWZvRVVhYTZ6Q05rT1RZUlcwaU15cDV6enRFc0hxTUYvWU1pU2xm?= =?utf-8?B?aVJVK2szN2VlSi83d2lIaXlUaG1uaFN4TlU5QUhhbFZZdzZxOHFMOEhKQWlL?= =?utf-8?B?Wjl4TFlYOEl1aTBwNWtlMmIrcmZZVFFPMUllTmkzdWtwSlNaRmJWVEtQajc1?= =?utf-8?B?Y29xMmNXVUs5QUNOUzd0MXNLalNNV0VOSVl2K2JkcFRmc2g1eUN4eHAyVGxs?= =?utf-8?B?VjJHQ1NEaGY5eGR0YVpZU1Uwd0xUVjE5enNybEJsUzh5N0lxZ3ZkUG80LzFl?= =?utf-8?B?ZUZhKytQSE5BLyt3VEdUV295SUZwaW11dXk4R1c5VlQ4ZVlFbi84eHdkV3pZ?= =?utf-8?B?a3RtaktIYk5vWGJHaTJDVG0yUjNSUDFIWmZncEw1Vm8ybHlwcTBCUm44T1JC?= =?utf-8?B?Z1JFTFFzSkFqWHF3ZERmeDZmR2ZRbmNpd3ArWDRJNlI5UGtzZHliMUJ0U1lz?= =?utf-8?B?Nk1xYS9yMy9aL2RQdjVPQUEyTWJtZHZjQUEySU1QWTNzZjE2eDBoRmpxdmZ1?= =?utf-8?B?WndkTEEzSHpVd1JoTEFoU051OHdobVFRVStnblEzY3N4R1A1eGVUaWYxR3Zz?= =?utf-8?B?bEpQazYrbVVBRkt5bGlzRzNEc3NBYzBacWhDSEF0Sk50dTUyaWw1b3JDMjFG?= =?utf-8?B?MnFTK1VjZlZaWjZKeDBheEVXSzR3N01UYmtRNEZ2dHBPZlNoc2dQTG5nbkNS?= =?utf-8?B?V3lkTE1QeVZBdHNPYnROdzlLQzhUWlpnNlNMeFhRVU5qUE9WMVhrSU8yc1JR?= =?utf-8?B?aHJtdmc2cUxWWngzZVo3RmduTVlhS2U2TDdUcTVQZ3A1OE9MdC9MQWtuTnlr?= =?utf-8?B?QUppblVXT3JvdU16LzNWdDVBUC91ZGpBM0h4MFd3cEQ5Wnh2ZGc4SVZ5WHJr?= =?utf-8?B?NEFjRDVSTGFUd0JsekxsNGVGWFo2V0FtK0UwN2dIMnMzSWNZTTgvS0FzV1Vu?= =?utf-8?B?aUlzK0tNN0MwRnVlaktmRENmWlpzN1pkSUUzZS8wVFZRcklmdlJkSXBXcnZt?= =?utf-8?Q?TQKFd85rGEO9FDQP7NdnN7vj+sjHn8=3D?= x-microsoft-antispam-prvs: x-forefront-prvs: 0950706AC1 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(39860400002)(396003)(346002)(366004)(376002)(136003)(199004)(189003)(53546011)(5660300002)(36756003)(256004)(229853002)(97736004)(478600001)(14454004)(102836004)(26005)(6486002)(71190400001)(71200400001)(486006)(186003)(33656002)(53936002)(6306002)(606006)(786003)(966005)(6506007)(6512007)(82746002)(236005)(9686003)(14444005)(9326002)(55236004)(54896002)(316002)(74482002)(81156014)(8676002)(2906002)(8936002)(86362001)(446003)(6246003)(99286004)(110136005)(66066001)(11346002)(76176011)(68736007)(7736002)(81166006)(105586002)(106356001)(476003)(6116002)(66574012)(6436002)(83716004)(3846002)(25786009)(58126008)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB4176;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: KNyBvSTJa56YO4SFBlnYM162F/PqaHVjLHUARf/x19YWCw2PVLbevgpQaoQuQdtglUZGeCNc2ZfygM6Ic97nmR3+X9lTwA0CCmA/9PTxbPujJFC/Rk6FKI2S8KU2F/ikwKgOr/1t7xDyQmheFSkXAzbc5yKh8MsMa0bdaJXN3RY9DKOEjvKiuJZLrYS6hfq3UbObyN+4s5DBLgtTjqIbutcxaIwLFLgmNXZx46+dqDlt0hk5O5Qq9OnYckCDXtEdq0v1GF3+caC0/8CgAmFzIxYXMfeaXLFU2NnNekp6UeX8wbU5zsprAcNFtfvkYxoWrv2KPUgTkGZFJV7L6AQZIGYZVykjmGcFKgY1rC6PxmWB2k+LjCOnWzNw4kmkOwCPM6yqD867LPhfAETDzGYN6XaZef6sqlWo7gqnJXg2rwM= Content-Type: multipart/alternative; boundary="_000_D0B540BF4D8C4507AD4FFF5B6B335D44nottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: f22ebce1-a520-4d9c-1bb4-08d69427b2cc X-MS-Exchange-CrossTenant-originalarrivaltime: 16 Feb 2019 15:59:14.2739 (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: VI1PR06MB4176 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: , --_000_D0B540BF4D8C4507AD4FFF5B6B335D44nottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi, I have already written on this topic but I had some thoughts, actually this= is related to my explanation of judgemental equality when teaching type th= eory. In Set Theory we have the element relation and equality and both are propos= itions, so in some sense dynamic. Eg whether a element relation holds may d= epend on some assumptions you have made and the same goes for equality. In = type theory as in statically typed programming languages typing is a judgem= ent, i.e. it is static (Actually I think there is a nice anology of set the= ory vs type theory =3D python vs Haskell). The reason is that we only talk = about typed objects and as a consequence a phrase in our language refers to= an object whose type is known statically. In particular the type doesn=E2= =80=99t depend on some assumptions. If I say that x is a natural number the= n this is not dependent on some other assumptions I have made. Once I have = dependent types this static reasoning needs to be extended. If I define n = =3D 3 and I am checking that (1,2,3) is a vector of size n I need to unfold= the definition of n. Actually I am already unfolding the definition of Vec= anyway. Hence I am introducing a static equality judgement accompanying my= static element judgement. Now what exactly are equalities that are known s= tatically. It seems very natural to include beta equalities and the unfoldi= ng of recursive definitions. It is less obvious whether we should include e= ta equalities because we can only do this for some types and not for all. H= ence one of the issues with definitional / judgemental equality is that it = is not clear what exactly should be included and what not. With the introduction of HoTT another important aspect of judgemental equal= ity became apparent: it is a universal strict equality. As I have argued it= may be a good idea to have a stronger universal strict equality, in partic= ular one which is not a static judgement. However, now we end up with 3 equ= alities: judgemental, strict and propositional equality (I stick to this te= rm even if propositional equality may not be a proposition). This may make = it difficult to convince the non type theorists that type theory is cool. H= ence maybe we can only have 2 or 1 equality and reduce judgemental equality= to a mere convenience but not a fundamental feature of type theory. Thorsten From: on behalf of Anders M=C3=B6rtbe= rg Date: Wednesday, 6 February 2019 at 04:13 To: Homotopy Type Theory Subject: [HoTT] Re: Why do we need judgmental equality? Note that judgmental equality is not only a convenience, but it also affect= s what is provable in your type theory. Consider the interval HIT, it is co= ntractible and hence equivalent to Unit. But it also lets you prove functio= n extensionallity which you definitely don't get from the Unit type. -- Anders On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote: The type checking rules are nonlinear (reuses metavariables). For example, = for function application, the type of the argument needs to "equal" the dom= ain of the function. What equality is that? It gets called judgmental equal= ity. It's there in some sense even if it's just syntactic equality. But it = seems really really hard to have judgmental equality be just syntactic equa= lity, in a dependent type system. It would also be unnatural, from a comput= ational perspective; the judgmental equations are saying something about th= e computational behavior of the system. On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote: In section 1.1 of the HoTT book it says "In type theory there is also a nee= d for an equality judgment." Currently it seems to me like one could, in pr= inciple, replace substitution along judgmental equality with explicit trans= ports if one added a few sensible rules to the type theory. Is there a fund= amental reason why the equality judgment is still necessary? Thanks, Felix Rech -- 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. 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. --_000_D0B540BF4D8C4507AD4FFF5B6B335D44nottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable

Hi,

 

I have already written on this topic but I had some = thoughts, actually this is related to my explanation of judgemental equalit= y when teaching type theory.

 

In Set Theory we have the element relation and equal= ity and both are propositions, so in some sense dynamic. Eg whether a eleme= nt relation holds may depend on some assumptions you have made and the same= goes for equality. In type theory as in statically typed programming languages typing is a judgement, i.e. i= t is static (Actually I think there is a nice anology of set theory vs type= theory =3D python vs Haskell). The reason is that we only talk about typed= objects and as a consequence a phrase in our language refers to an object whose type is known statically. In par= ticular the type doesn=E2=80=99t depend on some assumptions. If I say that = x is a natural number then this is not dependent on some other assumptions = I have made. Once I have dependent types this static reasoning needs to be extended. If I define n =3D 3 and I am c= hecking that (1,2,3) is a vector of size n I need to unfold the definition = of n. Actually I am already unfolding the definition of Vec anyway. Hence I= am introducing a static equality judgement accompanying my static element judgement. Now what exactly are e= qualities that are known statically. It seems very natural to include beta = equalities and the unfolding of recursive definitions. It is less obvious w= hether we should include eta equalities because we can only do this for some types and not for all. Hence one of t= he issues with definitional / judgemental equality is that it is not clear = what exactly should be included and what not.

 

With the introduction of HoTT another important aspe= ct of judgemental equality became apparent: it is a universal strict equali= ty. As I have argued it may be a good idea to have a stronger universal str= ict equality, in particular one which is not a static judgement. However, now we end up with 3 equalities: judge= mental, strict and propositional equality (I stick to this term even if pro= positional equality may not be a proposition). This may make it difficult t= o convince the non type theorists that type theory is cool. Hence maybe we can only have 2 or 1 equality and= reduce judgemental equality to a mere convenience but not a fundamental fe= ature of type theory.

 

Thorsten

 

 

 

From: <homotopytypethe= ory@googlegroups.com> on behalf of Anders M=C3=B6rtberg <andersmortbe= rg@gmail.com>
Date: Wednesday, 6 February 2019 at 04:13
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>=
Subject: [HoTT] Re: Why do we need judgmental equality?

 

Note that judgmental eq= uality is not only a convenience, but it also affects what is provable in y= our type theory. Consider the interval HIT, it is contractible and hence eq= uivalent to Unit. But it also lets you prove function extensionallity which you definitely don't get from the Uni= t type.

 

--

Anders


On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote: =

The type checking rules= are nonlinear (reuses metavariables). For example, for function applicatio= n, the type of the argument needs to "equal" the domain of the fu= nction. What equality is that? It gets called judgmental equality. It's there in some sense even if it's just syntactic = equality. But it seems really really hard to have judgmental equality be ju= st syntactic equality, in a dependent type system. It would also be unnatur= al, from a computational perspective; the judgmental equations are saying something about the computational beha= vior of the system.

On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote: =

In section 1.1 of the H= oTT book it says "In type theory there is also a need for an equality = judgment." Currently it seems to me like one could, in principle, repl= ace substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. = Is there a fundamental reason why the equality judgment is still necessary?=

 

Thanks,

Felix Rech

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to Homo= topyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.


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.

--
You received this message because you are subscribed to the Google Groups &= quot;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 http= s://groups.google.com/d/optout.
--_000_D0B540BF4D8C4507AD4FFF5B6B335D44nottinghamacuk_--