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-wm1-x340.google.com (mail-wm1-x340.google.com [IPv6:2a00:1450:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6ed935ae for ; Sat, 9 Feb 2019 11:38:17 +0000 (UTC) Received: by mail-wm1-x340.google.com with SMTP id y85sf2856930wmc.7 for ; Sat, 09 Feb 2019 03:38:17 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549712297; cv=pass; d=google.com; s=arc-20160816; b=VlBK76NIE5Pn4PvoXsOqgfJd4yCj6GKI3ZADgGjEgMEK5rvJuXqYJ+VfBA8zVYtZ1j eSQcdpey0D0Q/c+UKVZK8DZAuya35dFkOyEed3hao+iZU6P5+WO6XI58aLzLJT3pKKYI tztni20DDhg3L5TlaqY0s0mmyFqJZ8yueXOwY571VIh2Yf8/x/PqPjVkS07Rtc/Q+rv7 ktLVxBU/3nFCrW4sAwdV7vPlu7v1cWJy+rVVJeLWlaB7du/mpOpK4A7Z1J0BxvDwBVEw 1qhZPouRAqrZv5w6I10GTEgfSpe8DQT0NDyvhHhtcjZvfpuywvQZVrqCig52cmBhv1A/ yASA== 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=4p7isMuCeHNDGXLnQEZXKNq0xIUFrV3Tjek/S1lFB2s=; b=HHfPpoo5LJh5TiItDVONSEEY6IJbMYI4WaSnN1nTyq9dnnx+EDTbGq/XuDkytbCYnz thvrMhCxdNG7897jrcA/NzmqTmMm4uVqZkfZpl5wIqb+8uYLQ6Ax7xnGvoa7G6dfONhD z9gnyHKF+T24xqWQIoEwD1/9oWdk4o+SsHhbKiu/TjYoAOONvGAxq3RZGeKg+X2Cm+hz kpyE92HRo0w7q8whSmGGt+xjZubbN2/pK4LlAJIj8pg59dXfUBKLpqO//19ahjrMl5ix 4qtb2+7b2qG6toCUDyseHG/YP1s8VLLVmLDTpIcoVFDYEPFYiiF33Yzi+6jR5bclieyA Zsfw== 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.252.150 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=4p7isMuCeHNDGXLnQEZXKNq0xIUFrV3Tjek/S1lFB2s=; b=eBeu3+eViiyJIP7GTihNdXBlh0cLAH1hmhVG7dnT3Q71Ni3yDXrXI+qRUE2JPggX15 L912xVAdg2xNTFbpCTJGOBF2aIs8AaDWeArX5Zzz+FkEy+jNHt2t7moS9hx/RpicmXzg ZSGatGcXgVl0VP4n/rt6WTs8elmSkdKHpmcIBBPdTTRjuJC4HI8juF5wNZ1qHsDR1yuR IO5/dU3HYwXGxj9tCoxnYUwNtRP88YThDeA0ed21BL2xW+PO3bg8w/dRRtXtMzJHloEW uqLcuuXjwWRypBSe3Iw0XhiXXyiPq4+JCgyD/nijd6DatYkuYtJBH33QFwiYo2fXjsRH z10g== 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=4p7isMuCeHNDGXLnQEZXKNq0xIUFrV3Tjek/S1lFB2s=; b=Qd4GOJAeUHDYHPds9ltX8IrAHgx61GVRnihrIvg4S/34aLcuSqIybrbQJMsrhCeRI/ OHB6MielD1nTWm2USP1/KkSvpdLgmL9jq9k5gNHCJVmhYcpLum49ujtXyWGaUpa6o8J5 Dbxe/66N3Xabh/RLOwKUlMTieoNb9p6NjZvyUOq8wCIs6ezj6Q0QSIbqR6S1rglPAqFt YUI7MdLGCZtzg+uOGPF5Lkj0bwpgVJo4CWErrCIuvQO3xF5bfcfbyhLuWXiVdlT9be1Y N/1VNY9r2IOKVhclTtdDnKHcTTEPQcXMlCHCmeVucCTsLQ9xdfxUQL7cMItB2o0oH/BP G4PQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaomRqdz5L6G7mLYI3ICUd9yLa0bvURoEnqeQwbqMMP+vLmi+4w 38Yt/jA9dbRwcf0J5gqIeMg= X-Google-Smtp-Source: AHgI3IYqaYci7E41SPpLp9f/pTE5WaMTiWhlbh8xhzcauTqYyNSOXPoYG3YenDlu/+6w8r8nGZ2YjA== X-Received: by 2002:a5d:45c5:: with SMTP id b5mr230203wrs.7.1549712297195; Sat, 09 Feb 2019 03:38:17 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:149:: with SMTP id r9ls1620173wrx.7.gmail; Sat, 09 Feb 2019 03:38:16 -0800 (PST) X-Received: by 2002:a5d:6041:: with SMTP id j1mr1365796wrt.28.1549712296707; Sat, 09 Feb 2019 03:38:16 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549712296; cv=none; d=google.com; s=arc-20160816; b=bfzjT4IbIYM93bI0S1Qp9bNSBIDxlmnc89tNkYxhFgIyt31hSKLu1O9tBbGK2Ze++B 6UzyJlMM3IyZnz8W44aoCngPB6HHyKqXEDj8nAqg6dgEpnHFmemabNwuGAEUHucz7g78 dsd/q2KfOw5wGUVR2ElVh5/ASCVCuSOOHHNe4sYiOQ1jDQiOmWtNr+cu8yLfMCOThdah pgyyUlUSQ6ZZRzxfz9v02Xk3CyFuw9MUoAkN+KiYG0v6JKfIl6t1UW4ajMi6/b04BDrZ f6xrDvTEI0ihZejvkhzLB8IKJPde25I0AUfbNMfQTQjUR8e55GGTXh/QqQziH1gD/n6n j3og== 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=gCJ1ixbXQsBHyB9HBjocgC0Cb0rF6e13OtCRinOacfo=; b=dck+lCTO0XSn9Vs5o7NoUYYQnjYAMQZXhd4R+egaTIGPcq80M1+nLmWbiBk1Lxu7df xfBUk7CLyjw4l+3urLNwuCVyQ4oM+k0PY6YGMZUTwBevsW50bWxJTdo9oXpprglVbdoE MoB192giGaz/op3Nj6LBH8CC/IJ4bt4fP/Ac1CiECpEc49IJF5kDcY/kqTXqWpwIUsRF H8dmjP4xRy+65u0gf/IHH5YAtp404e9X0vechJGII9eu/T070sbift04+G0+bF8iF+x2 3VhYmlA+BqqR3HjkHromuvbLj/TFBj6S7QGneTJHedyI8QFi7GU9WYegstc/PCsMo5b5 a1KQ== 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.252.150 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de Received: from mail-relay150.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de. [130.83.252.150]) by gmr-mx.google.com with ESMTPS id l22si472028wmg.4.2019.02.09.03.38.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 Feb 2019 03:38:16 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.252.150 as permitted sender) client-ip=130.83.252.150; 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 mail-relay150.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 43xVRX2yjXz43t0; Sat, 9 Feb 2019 12:38:16 +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 x19BdulB020353; Sat, 9 Feb 2019 12:39:56 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 39018C6BF0; Sat, 9 Feb 2019 12:38:16 +0100 (CET) Date: Sat, 9 Feb 2019 12:38:16 +0100 From: Thomas Streicher To: =?iso-8859-1?Q?Mart=EDn_H=F6tzel_Escard=F3?= Cc: Homotopy Type Theory Subject: Re: [HoTT] Re: Why do we need judgmental equality? Message-ID: <20190209113816.GA17951@mathematik.tu-darmstadt.de> References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> 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.252.150 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: , 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. 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! 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.