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,UNPARSEABLE_RELAY autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wm1-x338.google.com (mail-wm1-x338.google.com [IPv6:2a00:1450:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a44931f4 for ; Mon, 11 Feb 2019 09:32:31 +0000 (UTC) Received: by mail-wm1-x338.google.com with SMTP id f202sf5942769wme.2 for ; Mon, 11 Feb 2019 01:32:31 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549877550; cv=pass; d=google.com; s=arc-20160816; b=Y8NM2dMzacQGH5oTmdlG6qT6hfk8lONa2Cd0EY6Vqdh/CB+RmejdLsD2h1NFOuHmLX YUQnq6q91vPJG1bNFHPKVyhcNlPFUotCNyHqe/+UbiNAXome3cDF4ghtUPPgefc30m4E U6PRqA5fhPby2I5AqkxqZ4sDyt/p3uXY9iDWrvm4tyalHcxUsa0k/7r4R319ceCV2Hag 8RRCnbIiEnLsEL8IEtmPm3vdW66UuUM/r6lc1Hmo95mOxW6ucknP+e43t9dKlejcZg1X GCcjJ0P6DcgIaq1zpd00XWIrf/SKNYkRFkwYlX6NJt7ZcFqhXoyzckNg0Iz1Tf8O6Oiy Rrpw== 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:content-language:content-transfer-encoding :in-reply-to:mime-version:user-agent:date:message-id:from:references :to:subject:sender:dkim-signature; bh=WkBQiz84qEcsNYT2joDwnau0Ot/bO9OpZ48FrhilaUg=; b=MCe0tCDMJ/q3yL9f/5zk3QmiRTo6WtZPAA46jxl44Z6fkzW1+I7/08yi7SRRFsNkYt r+EG5HUy0N6IetLFMGdV3OINQdub5Wt/ZVrmcgctnR3MtylDxcQIwIRHRAZm6OUWB6jv /bKuVHVGZf19w6DEBj/Rf9NHHdOfT5bKgqbGVhhAjiCqXtBUiNY70tFGTb/qAvVk+AW1 G+KDCLU9zE5/RXF95KJIxRrIoVKNhMlmeMZdMzEBHfPhfsqaa6Dsexe3BJmp1lWfcfi6 uCXWJWRG+X0NN6k8oJc/ougjSyu5Ql3sWLImQaUgzyUCKv5N2aJeJhLukG9f76v+Up82 pQOQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-transfer-encoding:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=WkBQiz84qEcsNYT2joDwnau0Ot/bO9OpZ48FrhilaUg=; b=ZrlcaJ1cyi3cDGbXaBvuGkGDKQbAHAg+5x05ISMIzLcgaFy4nxzYL6+yvHkcVzyXFp /1rqJlbBo9m6IkS3yjIH0+q3QDynVX9Yiusow6N8V1amW+QfgEXBLIIrk4VjyhR0TCwO tqBWig2cLcK70ipzBaZytPvVZRfOx6jJSyVouezx2ae6X0dsgJEfTMLDSbIdRvR4pUdL EkKAUI88plFRf5Xmw/zoWNYt3JFWEdSPjL7qZzuKBPpfp6jYhxNVJ59+r7zqi0BDv80l zYa1O44rzrJgw74PDoRj4yR75Rm4JLMIT+s8n+GD1/AH4pwUNUpW6mmAKNOEDRJviiod EGSA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-transfer-encoding :content-language: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=WkBQiz84qEcsNYT2joDwnau0Ot/bO9OpZ48FrhilaUg=; b=kt2gzX7H95fw7yer19QNqbbwFwPfLhY6xxOjDkepPEl/p/UQOdrx7v+0e0PzFWTvnM jvEba51FzbHX3jd0dagwRuvqKdAE9FJTVHslLjkLWmg0+Qt7S3Wq7mB02WQ3Ku3d5JOH 9D4vUsO0FBz2J+Wq+kNvT7XVW9d+iZUIhLmKbYBc9rXnFSSk2Tp4LOKdvICzJeVTl+Qy Ene3wCesNbF1B4HmNH2NgTR3fzTtGvEtZcgV3y8FxZ140x7yNZDVqOUUg4ZjuWo6cl+g 8gRK5FeJxlhvxm4mYsn/3XSawYc2bnskxy5iRgc99bvOefPNKkPw7sdBNm/J1bKn/2yQ v5kw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuY3hrKGpiGR2COeksiBfrJw1Ly3iKmqK/UeALYlWwM5WJWp5GUs mskQW04srMt75xFBdfR8eZs= X-Google-Smtp-Source: AHgI3Iarbr3ZB1IPSYvnMh8WQA8jYz2EF/AAXZ7gH9YBCGEVe5MfoA5VrsXqxrtotS79dD5BNY+7yA== X-Received: by 2002:a5d:45c5:: with SMTP id b5mr303714wrs.7.1549877550856; Mon, 11 Feb 2019 01:32:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:f209:: with SMTP id s9ls673503wmc.12.gmail; Mon, 11 Feb 2019 01:32:30 -0800 (PST) X-Received: by 2002:a1c:4b15:: with SMTP id y21mr738236wma.11.1549877550453; Mon, 11 Feb 2019 01:32:30 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549877550; cv=none; d=google.com; s=arc-20160816; b=GWea64GVWUPr7GZiJrjK9PSTgeUBWJrDmaloV6KXi3TBkqkWBkCGC6v4jhesK3zSLg Paozr8ojfncA9d+1IVJz9RrYV/qbgpc1BUcG6wFPW4K9UdZQ06GZUmRQHneyJqnMYOAf ZembOdczcqa/NGh6CsjGwjgqX49+uWabaUSLOMAX4F54IIAGFjZNSizkL4FMWeA39aM/ eK464CJldmsEe84zM7VqU+ysBCCzPX1BJUpRJNgIBQhGr9cq5ycZh12cmPfhh/41K31+ bT92IbOA/Eu1SGwtJafTnbF3qjQqZ0KojQvsKEocyOpXROcxwrZwTdBpZJxhJyJ09C5Q YwqQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject; bh=G7aqC4fImcR/N49akB550HEphnv8CKLDXCg07cEEQwc=; b=i2nyeH0FkFWX5MMZNtRuBsI9lDZGsSupv6CRFgIImZFIoiRGpP38NXgjjfdCvnOA1l p2NHtLHrWk/9eJ9lbJMjqFQ/L65+mXMexFPF4M1QbtoWDLaXMaOBV6JO2alSh9Rsdl0a jg+1aaiNW4xSsSUp6W214G1DTE3Ooy/U+wQHY1DRWUyj3gmnUKuTD0YEyV9lVq05i2DP 0kKUT3QeUu+0K6Io5+CJvp8pTtWnXXH6HafSG1oTDM3BJzJ7LJyFqgbBoiWkZkTyB1fD zPJs9SlaCKpQFLOnAu0ig2rWSgAyEHb9V8J7ufpj+VZbRJOBNKF8CHZBNOMqq14DjlQm p0eA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr Received: from nef.ens.fr (nef2.ens.fr. [129.199.96.40]) by gmr-mx.google.com with ESMTPS id s124si489390wmf.0.2019.02.11.01.32.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 01:32:30 -0800 (PST) Received-SPF: pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) client-ip=129.199.96.40; X-ENS-nef-client: 129.199.1.22 Received: from clipper.ens.fr (clipper-gw.ens.fr [129.199.1.22]) by nef.ens.fr (8.14.4/1.01.28121999) with ESMTP id x1B9WTiX005229 for ; Mon, 11 Feb 2019 10:32:30 +0100 Received: from localhost.localdomain using smtps by clipper.ens.fr (8.14.4/jb-1.1) id x1B9WTHI126346 for ; Mon, 11 Feb 2019 10:32:29 +0100 (authenticated user rbocquet) X-ENS-Received: (109.89.19.93.rev.sfr.net [93.19.89.109]) X-Envelope-To: Subject: Re: [HoTT] Why do we need judgmental equality? To: HomotopyTypeTheory@googlegroups.com References: <730FBE36-8E4F-45F5-9DB9-3B3A04E708FA@nottingham.ac.uk> <419b250c-491b-43de-96f8-d5dc34a5ff16@googlegroups.com> From: =?UTF-8?Q?Rafa=c3=abl_Bocquet?= Message-ID: <5ee36eda-988c-c74d-de3c-28d23c4bde0b@ens.fr> Date: Mon, 11 Feb 2019 10:32:26 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.4.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Content-Language: en-US X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.4.3 (nef.ens.fr [129.199.96.32]); Mon, 11 Feb 2019 10:32:30 +0100 (CET) X-Original-Sender: rafael.bocquet@ens.fr X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr 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: , I have been thinking about the relationship between type theories with=20 weak or strong computation rules, here is what I currently know about it. Note that in the presence of UIP, type theories with weak and strong=20 computation rules are equivalent. This is a consequence of the=20 conservativity of extensional type theory over intensional type theory.=20 (As Th=C3=A9o said, the proof does not rely on the presence of strong=20 computation rules in ITT) Without UIP, there are coherence theorems to be proven. As explained by=20 Thorsten, we can replace a type theory T (presented by generators (type=20 and term constructors) and relations (definitional equalities)) by a=20 two-level type theory whose outer layer has strict identity types, and=20 in which the definitional equalities of T become generators of the=20 identity types of the outer layer. Here, "strict" means that we either=20 include the equality reflection rule, or the UIP principle. By the same=20 arguments as in Hofmann's conservativity proof, both choices are equivalent= . What is interesting is that for some choices of type-theoretic=20 structures and definitional equalities, UIP can be derived in the=20 two-level type theory, rather than taken as an axiom, in which case the=20 strong type theory is a conservative extension of the weak theory.=20 Proving that UIP is derivable is very similar to proving coherence=20 statements of the form "all diagrams commute". (it is an acylicity=20 condition) If F : WTT ---> STT is an extension of a weak type theory WTT by new=20 equations, and W2TT is a two-level type theory associated to WTT, the=20 situation is as follows: =C2=A0 WTT -------------------> STT =C2=A0=C2=A0 |=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 F=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 | =C2=A0 G|=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 H|~ =C2=A0=C2=A0 v=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0 v =C2=A0 W2TT ---> W2TT+UIP ---> W2TT+EXT =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 K=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 L (The objects of this diagram are the initial models of the theories) G and L are always conservative, H is an isomorphism, and if UIP is=20 derivable in W2TT, then K is conservative. I think that I know how to prove that UIP is derivable when considering=20 extensions corresponding to weak computation rules (propositional=20 identity types, ...), although I have not written a detailed proof yet. The core of the proof is a procedure that performs weak head=20 normalization, up to homotopy and coherently, in the weak two-level type=20 theory. Because the strong theory is strongly normalising, repeatedly=20 applying that procedure terminates. -- Rafa=C3=ABl Bocquet --=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.