From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORBZOX7DMQKGQE4GPE5LQ@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-qk0-x23e.google.com (mail-qk0-x23e.google.com [IPv6:2607:f8b0:400d:c09::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 17730560 for ; Thu, 5 Jul 2018 14:32:06 +0000 (UTC) Received: by mail-qk0-x23e.google.com with SMTP id d25-v6sf7972112qkj.9 for ; Thu, 05 Jul 2018 07:32:06 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1530801126; cv=pass; d=google.com; s=arc-20160816; b=JtQYr6y6f3IxkLSa4/qJjARLU9ESvO2CL8LVT8yrG/4RvN8gtI5z8Li8bcr2FHzAL9 PsYQLJI4Sw4KdGVSLkL6Nw57Qm/H+2z7JvJ9al1VOM0vznuWB4Tn/TkqpXGFTiBhqM8S bIZ3gw525O6HzkDnPXwXTDq+yQOA2Jg9kNov4es9MhCNz7JgrUI99ryR3U9CXgslzrlo e++XtMeuPBw1qm3f1C6m90aerULu6NEbjKGkKS6jd8gAgMqk05ppQQNEeXXNhP5ksyMD 9ob4EjnUIXAnP8aOlKHqWoGZtI7Ft3sojhowlLVXzeWZD/BeSJhz6+OMbIUBaf0/uvFO JohQ== 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 :references:in-reply-to:mime-version:arc-authentication-results :arc-message-signature:sender:dkim-signature :arc-authentication-results; bh=A907S7ikn6EgCVFzI6ZAkCnCcnDSiYoErBQrPPnEWJ4=; b=ECW+kS/VuYMlMa0JFs3W/EL5OBWB7/UPJ88Rqx8dMWSKCH48omcGRErWC9BRa2Qlix EReMyF+MXlRV6e2E0LvDjbYQyxvmHS0ynB2bBMwTSIVc5QFXbqNash0Z8JPefWpytK1k ZHMHcq57XKzZX9y3S2YTrHB80jIrZGyufIwvenXxz7CIHs3AO+Iq06nWc6eCjRuiildk rqC8aW36Uq0ADFbGwdhFOqKMj9mCkbyI5gKkjhSY9XSBWdans6/5Q86V/fxWTCwwiuRO x3lAdQpuK2E8+8gH2/PxEmjiMlRhe6CuRSMDap8o9Ku8Axxp9qH7+ty6FVxq/LRiaaeR vHew== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="z75n/wl6"; spf=neutral (google.com: 2607:f8b0:4002:c09::22f is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:in-reply-to:references: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=A907S7ikn6EgCVFzI6ZAkCnCcnDSiYoErBQrPPnEWJ4=; b=QW35j9L+8/mD1av6EhN9W3iXxSCcfXPrsXwfedWcjKFuXfnHXOGGiETiviNM7slLx8 URo13/0MR2a8fKn/umcmIMzV6N9Fqozoi7G1CqBBDts9VZow9IHmwyIHud7y9YtQxokg IYRKiEa704RBjzp/1CEDWlVn/0vM4XmP6/xu5TLQpRr1ipijwhfFNRo8Gn7yhP5/0EWr TnsdkN0Pg035EBcYUVh/l3s07PE9bY8eNLQ8FMP2ejsBGEsRVRknTkluGOuiN7OXdJLw doa/jzpGz0Ux/YEANRIlhM3Pv80qbJsAgTLb7F8I9BjQjC7zi6PhqkWZ7hDMXOziX4st M+7A== 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:in-reply-to:references: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=A907S7ikn6EgCVFzI6ZAkCnCcnDSiYoErBQrPPnEWJ4=; b=p0VjZmNgtD2BVxhAJdmKCVu+8lgNwrbzS1lpUVUw7BAehm91qE0bqo5yr25TkrsA1p S0ecTdRpxc9uMuEwVwqqkPVoa5xqCa2MAcJPQUp2Ge10Rcknw9g78YqCwqHPsipeNZFr Ua4IHr1VvRMcJXKTL85PWN0wfq46TlmpZNX8vcH9I4wweneGcfPB1dzGpiosKxnYIjOp /66JE2moy8+EahmdR/Xz6TbA7j2qFpm066NoVNDNRGs/0AAOloq6QDoFAIzRhgo5nSd/ MdWrfyuoVMarXgiN3efJSPZi4k2zr6R5ROXCvYKX8q+uusXDQzQzmLZYt6HZoi8Alh2X rLyA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E3hV8YAHu6GYNM4oJChB3ZLEIyvIIHiTmhVJ7UXiE/kkXIxsse7 LWjJ5aL7m+E4rAYwx3SnKFw= X-Google-Smtp-Source: AAOMgpcB1ASRYgsd0DxWeVgM4oukmeZkCaJ27xjD9XkWPtpLsHhmVt0ckK1S49R8pY68f0DNWO6mdw== X-Received: by 2002:ac8:68b:: with SMTP id f11-v6mr461390qth.3.1530801125798; Thu, 05 Jul 2018 07:32:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:ba1d:: with SMTP id w29-v6ls483196qvf.3.gmail; Thu, 05 Jul 2018 07:32:05 -0700 (PDT) X-Received: by 2002:a0c:bd2b:: with SMTP id m43-v6mr3554387qvg.52.1530801125222; Thu, 05 Jul 2018 07:32:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1530801125; cv=none; d=google.com; s=arc-20160816; b=Thq60Jp3o7OgQ1maZSgE8S3GJKRm2QhvTMV8UOA+38T0fteoCDThT464M6Vx8LPPGd XcVzRTXDkLM4NMx6EuORLd+/24yxx4Qg2cVv7YMMb6UBj+xBsu9NQCGoN+h0rGDFiI9Y jaghALdhcGZy2py8oQQfWFMMyMOETTvFwusYPIUOuBcVUU8W2IBPU+aFtJ3e8v4DbE1t rXLjcPKCxXRzsYvKRW46J3acATUjvzEWtXjgvDxSLpuxtfQX/dT8xOszutlCOf0g5cpt p7OGcmn8R0WgVvEMEAxJqcd3rAhPTs0t1JWQvxVaOZv6Fmh/A+Wjjddq8Pkbl8JTB1k4 HwuQ== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=0lC7PMAIA3fx5XTKVU/6+cSIWEA2PV9JbR8rDgp60Kw=; b=cCQV8ATVMEvFP/PmxPjOoGzBEnWeS1R20DnLCX+kc80Lc3nQfyOetCoLPdsqAxAQv7 ByK2rdfej600ON0DbyOT5zwdZOCDAV3cpgeJ6Kuq/gldJ1PPleOO2JMRObJyIRHow+B3 sgjOKwNcjDYzMdTHz4DInZzMZlQNyBgwBd+GAr7DC7ImSnMhKpVYJibSEGCMtFid+GOb KcY34ttXvginK7WEBnZSFzZFHzQ1pdshlkX7TvrconSn/dBD2JUQJDAGWbAw4DuLnNAQ fu2W5R6XzUMTRuX7cPIRwLrOd40DOEMgRsBckINYi1h7AyX3CPEY/zlF2lJGVMAnf5P2 5umQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="z75n/wl6"; spf=neutral (google.com: 2607:f8b0:4002:c09::22f is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb0-x22f.google.com (mail-yb0-x22f.google.com. [2607:f8b0:4002:c09::22f]) by gmr-mx.google.com with ESMTPS id o8-v6si386272qtm.4.2018.07.05.07.32.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 05 Jul 2018 07:32:05 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22f is neither permitted nor denied by domain of shulman@sandiego.edu) client-ip=2607:f8b0:4002:c09::22f; Received: by mail-yb0-x22f.google.com with SMTP id s8-v6so3281992ybe.8 for ; Thu, 05 Jul 2018 07:32:05 -0700 (PDT) X-Received: by 2002:a25:a08a:: with SMTP id y10-v6mr3135996ybh.219.1530801124789; Thu, 05 Jul 2018 07:32:04 -0700 (PDT) Received: from mail-yw0-f169.google.com (mail-yw0-f169.google.com. [209.85.161.169]) by smtp.gmail.com with ESMTPSA id s67-v6sm2271207ywe.74.2018.07.05.07.32.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 05 Jul 2018 07:32:03 -0700 (PDT) Received: by mail-yw0-f169.google.com with SMTP id t18-v6so3025609ywg.2 for ; Thu, 05 Jul 2018 07:32:03 -0700 (PDT) X-Received: by 2002:a0d:cc8d:: with SMTP id o135-v6mr2984323ywd.178.1530801123013; Thu, 05 Jul 2018 07:32:03 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:4094:0:0:0:0:0 with HTTP; Thu, 5 Jul 2018 07:31:42 -0700 (PDT) In-Reply-To: References: <67d3932e-aa85-41dd-9845-db62e2472772@googlegroups.com> <0137f575-f414-47ea-9264-47ddbf5d38f6@googlegroups.com> From: Michael Shulman Date: Thu, 5 Jul 2018 07:31:42 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Equality in the Model Type Framework To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="z75n/wl6"; spf=neutral (google.com: 2607:f8b0:4002:c09::22f is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu 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: , On Wed, Jul 4, 2018 at 10:59 PM, Matt Oliveri wrote: > So on the syntactic side, this is saying that theories can't add constants > or equations to the mode theory? (Like flat and idempotence of flat.) Yes. > Would this support W types in the doctrine? It's possible that there is a notion of "recursive F-type" that would include W-types, but we haven't really worked that out yet. > Universes? Do universes somehow > pop up out of the new U types, or are they special? I think universes are special. In particular, they don't have a universal property. -- 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.