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=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, 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-vk1-xa3b.google.com (mail-vk1-xa3b.google.com [IPv6:2607:f8b0:4864:20::a3b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 7aeb7ece for ; Sat, 10 Aug 2019 12:31:24 +0000 (UTC) Received: by mail-vk1-xa3b.google.com with SMTP id d21sf1269193vkf.5 for ; Sat, 10 Aug 2019 05:31:24 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565440283; cv=pass; d=google.com; s=arc-20160816; b=OwaY6RpvWY7H/54TabVvIvtpa3h2rijqPmkJGH1/6TZgoryuhQfC5cQwr4tPn6FNEn NioblRk9vvHkyXj+9L/hA8ZoQV/wk9xIM4ivKYJta8ts2QzDgVZ+JxhIK+Gok9mdClLC 5DGgp2ywrs/VXJND78TtMiwo2k+omKRwfhKFH6ZrcmB8He31R4p+Tkgp9DuGZFbRkZ3j mbk1YBYDm2FP/jfbNVnY2JuVdbICMs3re1RUEt2ZVU5MsTfSwjhKXjXO7v4AoIt33fF9 t4btf8bcesMbKsW6mkrtTvXBaetDeTmHYCIB4Bvjj8JQs8zZX7rucr6nr/khl4BSKLjh Z0tQ== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=RnQqEBLYB82pOb1KNHtohd6L0MYrkptL3XVLHdoaYo4=; b=JS00h2uK0M3rQrmolMMGNVt90Hzo/QhYLSeCnOKaoMzHn2FxzxuP8lH1fgO+jHNwht aKlimpANVrXi1jybpRW9vrJvbwoM4PRg1kAZqGbR8/R9DJSrnkhisAtOpuvIF5Zi8zfl GbFUdWU/81I+Gf2XS/VcRIZEU9Tf5dc4QxetWy7p+WzV/eQsBY6aXuIN4xD1CITg09du iz0TMZ8xxIPeTKwXKS+v7MhjuXAB+86M0ITZzm3NfbHTjIBU/79Fi6/8yI5URSHEHCET NMnp9q6wRx7DjHW3LuyJT2bosN2bQa6VQFqb9cETjic/9CQS8j370eYzC3RMpvapdB3h SQlg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=AnD72uwy; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::336 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=RnQqEBLYB82pOb1KNHtohd6L0MYrkptL3XVLHdoaYo4=; b=X3gbveUCcDIXJbVc+s+5er9xQt6eo0kUMqlxBX3xDLjE33GhtuOC6LntZ/4bceQCp9 Kxk8Wv/IPOpeyoEOm6veyhMpGR6QIYbsUE7H5j/WAFYeLzB8RoCWLZQpuLWtlEbtGwXZ ab7VWXYXpc9rg18bCUyNKbi/XdwWA5jAuM+RN/ut69Ds+6uqJYedwnHpVD1TrZINbPxI CCZN8scR8OKMr+tpcB2LfgahjYpWyAXIKi9bh+mfoVP/9dY01qj5lnS1HauKbAHWO7gJ zSBZP6A+KLD5AFnFolZcy5VuqfXaeEDoNBajM3Bq800bra1+G8uOyv6Y48w4eNqS8qt8 xGzw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=RnQqEBLYB82pOb1KNHtohd6L0MYrkptL3XVLHdoaYo4=; b=uKEXYXkQ9j5uxUK2y58IDX6e84cnnRIOqkj355Uvcfuq31TBBsA9qrF/3Ycg/mqkRG 5WLwIAKMrQkS/wNJFFuXgtoGdXqT/I6xil9N/lCNkEZwuQsjG/D+Vtu9zc/VISG+yEMc wTRqW7aIFg2vUgn4OAv9wsJuuG0bTjsU+i+A+n4QbvoW21BW7GZnRd6yabVzI206pJ30 OSJyyB+895dwy0kiQbCOI6nKymz+4m3eUzrFyCtb1zy2tHmElB1pQnLvvpbG9ZagSkxO iWO06MZlcvgv3GszLf1uxgp+zu5DkLC+0TUWmXHwMfOajqGy/DHfjzXJ8NvRgeT1LpGG 01Rg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=RnQqEBLYB82pOb1KNHtohd6L0MYrkptL3XVLHdoaYo4=; b=bSz9++EiycmPe4B6wSz5wRoxQ6VyYa0hTSLhr5ZVmVlnvfhTaNTUCplavec8IQX7XV /OsgmkbLxzA9euUMVlsOp61V00D7aIaRRgr4dyH6fFmzT+Kx3I6eDVt8hb0cRLZvM9VJ AQOQBDVZSz1En2K8QlK+DmTFClVmJqG3GInyCviZMcSmp4yWkU5x7k+4rtEEO6HjLgeI 4m61ssgbEj7XQoyq25RaFW6JrLJWSmyfJLGOjQmNNLphxcFu7fVhgx1l5MwTsxid7eCN Q1HlGmK9gWC0Cln5lYechNoYUimUGEWCkfZC9XsJh5MRv97n75NKofAjNJ+mYgSbx5HT UCTQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAU2KhZl3gnyHjcnKw8ioP92dE91oSLiyqtHGiMeOSFDO94JmEvm 4wu1399Ldy2rHEC4MflVEQY= X-Google-Smtp-Source: APXvYqxptV4yiRJ1OKXKCOeJISEbjywIR6D+GrUbKNtUDzk29OfepLQdeun4+0VmBABR/nDAv1vjRg== X-Received: by 2002:a9f:3f4d:: with SMTP id i13mr15203781uaj.54.1565440283546; Sat, 10 Aug 2019 05:31:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:6195:: with SMTP id h21ls7115763uan.10.gmail; Sat, 10 Aug 2019 05:31:23 -0700 (PDT) X-Received: by 2002:ab0:7491:: with SMTP id n17mr14962320uap.102.1565440283244; Sat, 10 Aug 2019 05:31:23 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565440283; cv=none; d=google.com; s=arc-20160816; b=M3Or9D/Tp793shTbTrth5UJyxcr58PKydLs8Xgoepx4B/u627ALYdExnSkLwhxnbQ/ x74VYVw3fEK93AFaco9xLwd/en7lGIEVdr4koALkiBwnWspg9U+r8yY/Uvj6zkeMAQqz 2uLFpI1vAHea9kxROCjwHmfIjdfPMfDjlsOi2145tHZeFXRgS45iJ7RN/xQim9rPlsrf xSfXNJzCAhUYeOw3nNKxyGgXnZJ21YuCZky3kIev5vLenWwtKFl0My+H8k4oGQvSLhrt 9VZPH6texeSikMVRc+Gp6edCPDBHoEzyEZTh6/Oha3fXPYeDx5RwoNy/T2l3ElFw3vpr I02A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=Efy+MTCdOD1PKPKotHSwWPzzUEez2d244s+RwRnS0RU=; b=mu7/k4NixqM0MzK8kT/LzS7wDwpFUy70JPkTm7+yXDrpcfZgyNEHcLqKkIzVjJ6iKN Y42po2S64/VB18o8sB8kvsbPChpXxx9wlw1fPMPBRyjYxBYymSEyhsMKd8DGFaS418rt EGeOHft5yhrm7Lanzgw3/rcWVFeqrz7Tc0/W4pa1OqChRE64mwtC3ulvtFzkhPg2kvO4 JDoearxSTnaXfA8gkzYgB+7zWQZoCkw9RFALhGn0bGPMO+TYqPIMt4G3tOccmR7Z+SQn B1saWk9HGNDc82nTtcQykQ2TudebQjmixBxCqXsx9oQTehQij2JeG/H7m7vdKQwljzJK thqw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=AnD72uwy; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::336 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x336.google.com (mail-ot1-x336.google.com. [2607:f8b0:4864:20::336]) by gmr-mx.google.com with ESMTPS id i9si6849416vsj.0.2019.08.10.05.31.23 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sat, 10 Aug 2019 05:31:23 -0700 (PDT) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::336 as permitted sender) client-ip=2607:f8b0:4864:20::336; Received: by mail-ot1-x336.google.com with SMTP id d17so143153701oth.5 for ; Sat, 10 Aug 2019 05:31:23 -0700 (PDT) X-Received: by 2002:a02:3b62:: with SMTP id i34mr28342522jaf.91.1565440282767; Sat, 10 Aug 2019 05:31:22 -0700 (PDT) MIME-Version: 1.0 References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> In-Reply-To: From: Valery Isaev Date: Sat, 10 Aug 2019 15:30:46 +0300 Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: Michael Shulman Cc: Nicolai Kraus , Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000f8b54b058fc27772" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=AnD72uwy; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::336 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --000000000000f8b54b058fc27772 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable In the theory, the rule looks like this: A : \Type0 p : isSet A ---------------------------------- F(A,p) : \Set0 and we also add an equivalence between A and F(A,p). In the actual implementation, you can do this using \use \level construction. If you can prove that some \data or \record satisfies isSet (or, more generally, that it is an n-type), then you can put this proof in \use \level function corresponding to this definition and it will be put in the corresponding universe. So, you can define \data F(A,p) with one constructor with one parameter of type A and put it in \Set0. Regards, Valery Isaev =D1=81=D0=B1, 10 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 12:47, Michael Shu= lman : > On Thu, Aug 8, 2019 at 2:56 AM Valery Isaev > wrote: > > You can say that they are hidden in the background, but I prefer to > think about this in a different way. I think about \Set0 as a strict > subtype of \Type0. In comparison, the type \Sigma (A : \Type0) (isSet A) = is > only homotopically embeds into \Type0. It is equivalent to \Set0, but not > isomorphic to it. In particular, this means that every type in \Set0 > satisfies isSet and every type in \Type0 which satisfies isSet is > equivalent to some type in \Set0, but not necessarily belongs to \Set0 > itself. So, if we have (1), we also have (2) and we do not have (3). It m= ay > be true that A is a 2-type, which means that there is a type A' : \2-Type= 1 > equivalent to A, but A itself does not belong to \2-Type 1. > > How do you ensure that "every type in \Type0 which satisfies isSet is > equivalent to some type in \Set0"? Is it just an axiom? > > Also, since \Prop "has no predicative level", does this property > applied to \Prop imply that propositional resizing holds? > --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAA520fuDN9yffbCT6Hxv9kvB%3DWW%2BiUcTf%3DJuXi7kuD5NknWbf= g%40mail.gmail.com. --000000000000f8b54b058fc27772 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
In the theory, the rule looks like this:
A = : \Type0=C2=A0 =C2=A0 p : isSet A
-------------------------------= ---
=C2=A0 =C2=A0 =C2=A0 F(A,p) : \Set0

= and we also add an equivalence between A and F(A,p). In the actual implemen= tation, you can do this using \use \level construction. If you can prove th= at some \data or \record satisfies isSet (or, more generally, that it is an= n-type), then you can put this proof in \use \level function corresponding= to this definition and it will be put in the corresponding universe. So, y= ou can define \data F(A,p) with one constructor with one parameter of type = A and put it in \Set0.

Regards,
Valery Isaev


=D1=81=D0=B1, 10 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 12= :47, Michael Shulman <shulman@sa= ndiego.edu>:
On Thu, Aug 8, 2019 at 2:56 AM Valery Isaev <valery.isaev@gmail.com> wrote:<= br> > You can say that they are hidden in the background, but I prefer to th= ink about this in a different way. I think about \Set0 as a strict subtype = of \Type0. In comparison, the type \Sigma (A : \Type0) (isSet A) is only ho= motopically embeds into \Type0. It is equivalent to \Set0, but not isomorph= ic to it. In particular, this means that every type in \Set0 satisfies isSe= t and every type in \Type0 which satisfies isSet is equivalent to some type= in \Set0, but not necessarily belongs to \Set0 itself. So, if we have (1),= we also have (2) and we do not have (3). It may be true that A is a 2-type= , which means that there is a type A' : \2-Type 1 equivalent to A, but = A itself does not belong to \2-Type 1.

How do you ensure that "every type in \Type0 which satisfies isSet is<= br> equivalent to some type in \Set0"?=C2=A0 Is it just an axiom?

Also, since \Prop "has no predicative level", does this property<= br> applied to \Prop imply that propositional resizing holds?

--
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.
To view this discussion on the web visit https= ://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520fuDN9yffbCT6Hxv9kvB%3= DWW%2BiUcTf%3DJuXi7kuD5NknWbfg%40mail.gmail.com.
--000000000000f8b54b058fc27772--