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-x537.google.com (mail-ed1-x537.google.com [IPv6:2a00:1450:4864:20::537]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 10599914 for ; Sat, 9 Feb 2019 13:29:28 +0000 (UTC) Received: by mail-ed1-x537.google.com with SMTP id x15sf3980352edd.2 for ; Sat, 09 Feb 2019 05:29:28 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549718968; cv=pass; d=google.com; s=arc-20160816; b=V2+vvQzTcNcx1Cbk1h+mAfD2uzDYSzthXJX46fDnJQTMkeb8962+jVJ/lKSTbAHJ5h AJY/aVrYD7xQP5Q0ltw5BRlPHxsSDeH2NxDHDS38j7lt5Tt3E64ug9Ry/aqMXl0qNTfe YxFrxbxqexcWSC8Y+0dBll1AcHzDFkf6RWYmcGfCsH0tc8tErzL/acO2iYTcSh8zEkTU U+u3R0eZu5miyjAd8IReCCe1l/M8k1qo1s/6yVhpV5TzlU3iLd9R9F0xlpbEtbv9Rm9b Edb4Ajgp48x5d1rNdl7LQ1QykauC0UFX/cmye5LQrTB/MGrP+82sdAMChwdBYtrrX0Rn /zlQ== 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=AR2LSqZBftx5h3YM2V4Y5H7v1QA17pX9TklZs/RWElQ=; b=uPSU90w8nPgTzJuTldfUuGbsAmduAnVmjssubrD250cQNSn4pQUdLmg/y00tKOmK6Q YBp66owdXMNyRZE4Ycv4M7BKinxY+wKkeTmCKEyFD8+7mBCO+5LMe9lky3Zya54Swu3T 0coxQLnj20CCKAz50zBA8/oAygVBei/u7pndzhFtW6TAN6I1sDwZzxpBGuFsDzi7uRaS 2Kkke16ISxSQ52bDwbhy7NTfuMKjyRY7+jPBb5+DDA1ifgkFVkSH/KHngx/V9JGCxIRJ tmkuaZxGw/6pPW4hBwcKcO5fmyG8VKweBVxFn/jCsT42NHF8I5b2P2+hEr9oJjiizgKd TIAw== 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=AR2LSqZBftx5h3YM2V4Y5H7v1QA17pX9TklZs/RWElQ=; b=SmIVa7CRV8K3hZ69CflKFw1NynU2kOz1Hx4RvYHV2rjrmSCHtWSAmECRaApMv5zI5A yoNqLpID4/6wDBc0vfrjlOC2Dk1gQ8C42RikInfrLIVEmIV4pxp92ChBFxpliICs1u4M 7qGGfFqG/8+Q4amgSLzdBJ/VkTN3uo/2SQBArpJXexVzy5EM8AeSkNZ2yKnCdhCAe+Rl ePJLIAY+ekiCOv62lb5Ug9OA91ngIRN2EA0S776oFe3EFBlwIyKgsV/b7FXGMOqORRyv eaf19PM7M8HrkUCUoEzcKtvKrFBrRXFSwmTCz5nnY4dASo7n9Cja2WWRos2prmwI2HMZ DDxg== 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=AR2LSqZBftx5h3YM2V4Y5H7v1QA17pX9TklZs/RWElQ=; b=C+whkdACXQTwRe6LFj0vfS9Vb5obRf8vZ2glpjcmsQU5TqMtd/0X557JPaw3N4OwDM xkttFQrR2cMpEVkOF7OZne4nPgknGfPcFjL44DvX9T4Gf6ob85Kfxd456C6/xgWnu2ND tmtQgbqZjDs/RpGZq8Q38ZjNO4EBV1v7ddWv6kKO9Wkcq0R07/FpY9yA8RQDkWPMz/Dq Ph+COcMYYSX9+J1Bos0BaXSeusB1HsNUeIF2vgsskYU2TFyXdF3VYqhoKIwcOnP54j8k klrC9Y3gyBwh6Fd4iRhlUptAeCSq3OpL++04XlqUWiw4yAfQtZt6T/TAdpEq8tSHRn+h YOxA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYrrM+g6rzGWf2mXRbYNCNnx2a10ipCnbofewWm1Vab/V9zzV5B d5NbPBvdrgyllTBTJh2+vSc= X-Google-Smtp-Source: AHgI3IZha0pK4/D6d7DJWPG+L4abRWqSdsMT1HGAPwsWKjYHiNyJ7EMmV3LBR1Z+c0azSTlv7wSvPQ== X-Received: by 2002:a50:ea8b:: with SMTP id d11mr32376edo.7.1549718968310; Sat, 09 Feb 2019 05:29:28 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:3645:: with SMTP id r5ls148166ejb.4.gmail; Sat, 09 Feb 2019 05:29:27 -0800 (PST) X-Received: by 2002:a17:906:2346:: with SMTP id m6mr3172365eja.15.1549718967737; Sat, 09 Feb 2019 05:29:27 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549718967; cv=none; d=google.com; s=arc-20160816; b=S/nVW1xe3HCGUnezTfO9qKOsVQFhRYWgN4Ud3lwMSgF+M9qzawM2gLMP27Eb5V7DsI 61r3XLfSWy4dFUDl59gLfe6LCRyFO9tHfmGHj68wTCVhok/IrYa0Qjq8pL1qer7cTao3 SDH2YxD7myKwjkyo6bgmeS7SMsFAoGJdn4StHw4HGUXIR7ln/QS6wM2m1ZCFvCG0w950 VWKGWUgCU4+saULq1H1D855EugJO+6GAbz+fQ6R8w2Tx3fiS/VIqSSZKxYC7reMC1HSa P+4ntq4kWHco/zir/LgOLFK8QG1gkT2Bhtm6pJK6ZDeg73JtEWkmhaMno51HHc0m0JjH AuDg== 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=dZ4esXleskjKUHjCak9lkh0ND2aA9el07Kuh95aLvvo=; b=u4aPuYAbpQqzlrR0vJKwcijWHE4gJuDyIokmUiT8Kaq2kqVo43JokyDaVa8HKfSCK7 f2WFx/hvf1sMm/uSr4v7NtNFIc2PoifY1C3kfsFbeuU4UiuROUGsbYVvmG7RQ+xnsSld VMUU+KgbBzBAmwh9ziVzsvd03TyE3dL9yo94OIZEZ5xyL1GJ+12maisQ2qrWhQd5vQjl DR/9k/PiWG5DoQ+8IjnrlZPsCdlh6F+FGujFby5sj8bJGBuaeXONWdkwa02mw5UG9l7b +sJwavhChCN6JU1XmMrv4roj9rUPNl5PbRY+wFPsNysnEfIdseBEuqry+EP+ITepYArr eGBw== 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 m24si250735edc.3.2019.02.09.05.29.27 for ; Sat, 09 Feb 2019 05:29:27 -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 5A70D3C4712_C5ED5B7B for ; Sat, 9 Feb 2019 13:29:27 +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 2E7653C9E44_C5ED5B7F for ; Sat, 9 Feb 2019 13:29:27 +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 1gsShC-0004CB-SE; Sat, 09 Feb 2019 13:29:27 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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; Sat, 9 Feb 2019 13:29:26 +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, 9 Feb 2019 13:29:26 +0000 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) 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, 9 Feb 2019 13:29:26 +0000 Received: from EUR04-HE1-obe.outbound.protection.outlook.com (128.243.226.54) 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; Sat, 9 Feb 2019 13:29:26 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB4173.eurprd06.prod.outlook.com (20.177.56.85) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1601.19; Sat, 9 Feb 2019 13:29:25 +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.016; Sat, 9 Feb 2019 13:29:25 +0000 From: Thorsten Altenkirch To: Thomas Streicher , =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= CC: 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: AQHUv/P+1kLDiUWhyEydoPARmSK7D6XXV/wAgAAfDQA= Date: Sat, 9 Feb 2019 13:29:25 +0000 Message-ID: References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> <20190209113816.GA17951@mathematik.tu-darmstadt.de> In-Reply-To: <20190209113816.GA17951@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-microsoft-exchange-diagnostics: 1;VI1PR06MB4173;6:2mrIkZbauxKPegag3xWvZBO/191h1OCC1e94XpS0HTzQLDUPTZQ9RnZ5A7Qbe3ErmKmywZh0ajP+z8EhDRJYxs8247fNap7m8JyqQGFuhMEIIgJEzcdPb2TEN3IlqgKBxB2oTspGMWoNhTaJLf/DpGJQgri9xwpU9MtN2XbsT8VtWYBbzr/n+6mGLqrRDtp6r5cI+nA6bplHMvjrPv4NW+VzPoe/oKWm0e9TmGNlZWrr4bZbIq8n17eM+fxhBXR46sb7e6dsui6BArKeI4CDeQIWmAaTVf65iRw4khptAYqGAWcYAlGG3M1026b+tYzIXQmotCuvtQ0qDZDIuD+pNP0h58S0svwYBTy4ORWeFIvDK+fxK6NQJYOtHBRzqpNb3Q7EXVv7fkrYT8mpSl1rvjLSyFZyUdBt2rsHVxGp8MIA28VeDPGynpUd6WPz3RnFrKDDxqS1HxP+moSIYEDDDg==;5:qgfx/YNWzMGxjI7+iiPD0Q4wMuScZN1eFke8nltjvm71veddy2sqN3/+7wn+R2x2EdQATtD5kMkiHBVSVekCx7GNkjaDT2gIvzqAL4GhCupt5XZuWM9LHQkhQohqheo3H5Y1/+IoE9Qc+75dzcebaJCw/OtSe7qocvLZ9TKFXD1uLim0PUFkqjmx80C5V/GlhDm4ZVtUAGdq8MeKVToNMg==;7:rHdqF7Lgemm707QVhNk0SwgVz9XewoAv9OCDhJK/RmH3CzMAVip8fCpNFDVVQncF1e3c2jnQPVGXvC5qzNRQ8/q8FuXja/cjoG/b4F43q+eVZzNcUlrcQjYcKkkGBoubRd5TyiBesecTN6k0WzbI1g== x-ms-office365-filtering-correlation-id: e1edb1e0-ff59-4155-8522-08d68e929c08 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(7168020)(4627221)(201703031133081)(201702281549075)(8990200)(5600110)(711020)(4605077)(2017052603328)(7167020)(7153060)(7193020);SRVR:VI1PR06MB4173; x-ms-traffictypediagnostic: VI1PR06MB4173: x-ms-exchange-purlcount: 1 x-microsoft-antispam-prvs: x-forefront-prvs: 09435FCA72 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(396003)(136003)(39860400002)(366004)(376002)(346002)(189003)(199004)(6486002)(476003)(8936002)(6246003)(3846002)(4326008)(6506007)(11346002)(486006)(53936002)(4744005)(6116002)(6436002)(66066001)(186003)(97736004)(81166006)(446003)(102836004)(8676002)(81156014)(105586002)(2906002)(26005)(55236004)(33656002)(106356001)(478600001)(256004)(74482002)(99286004)(6306002)(58126008)(36756003)(9686003)(110136005)(82746002)(71190400001)(86362001)(76176011)(316002)(68736007)(83716004)(71200400001)(786003)(7736002)(25786009)(966005)(305945005)(14454004)(229853002)(6512007)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB4173;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: BZronSVnya3RgZgMDiYSUthk/j3SqyLQjk3nSJ4CTgNFhlxEGgFFtQDvePqHZFztKhQJtUXtwOVaJ31R4fc/Y7sT2enN2dgs3NNjZrkvWk0UOP4OQAVr7LEd74d9aoOCPfaFwzeZz/6ylBeSK+JJSCvJBqHi3AVPGukfyzOUrfgOSs8Nfh0G3Wqpo4gVzfK/+nG5azG1SUF9hSJ+ymUogzSCXHGLyUymOEDYJvbAgT9OdIz0MW9ittW5tk36J26Knr5+N/Oz/c42ZLnBIbQ/RrJWrwx11Qi2VFjsc7G978AOeUsxCnzGLFxktmo4W1prTSd3RHYPQGm8ivsj60A0YSUJF3Gs4inf5mppPfyjXZ6Yqb/Juq02u4j42rL8XW8WIucUXaakfy38Q1XB53KjD78c2zYg0hO3DFtdqfRxraQ= Content-Type: text/plain; charset="UTF-8" Content-ID: <35202ECF61377F4CAE0462D2FDEC0CD6@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: e1edb1e0-ff59-4155-8522-08d68e929c08 X-MS-Exchange-CrossTenant-originalarrivaltime: 09 Feb 2019 13:29:25.1936 (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: VI1PR06MB4173 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: , Even LF included beta eta hence has a non-trivial judgemental equality. Not= to mention the equations for substitution. Thorsten =EF=BB=BFOn 09/02/2019, 11:38, "homotopytypetheory@googlegroups.com on beha= lf of Thomas Streicher" wrote: Working without any judgemental equality was the aim of the original LF where elements of a type A correspond to formal derivations of A in abstract syntax. Also Isabelle works a bit like that. =20 So with a modicum of judgemental equality one uses dependent types for having a syntax for formal derivations. But, of course, this is absolutely useless when you want to execute your proofs! =20 Thomas =20 --=20 You received this message because you are subscribed to the Google Grou= ps "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. =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.