From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORB6VD6HMQKGQER42KPFA@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-yw0-x23d.google.com (mail-yw0-x23d.google.com [IPv6:2607:f8b0:4002:c05::23d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d799a9b9 for ; Wed, 4 Jul 2018 04:50:04 +0000 (UTC) Received: by mail-yw0-x23d.google.com with SMTP id i77-v6sf3730824ywe.19 for ; Tue, 03 Jul 2018 21:50:04 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1530679802; cv=pass; d=google.com; s=arc-20160816; b=iPqoEybyrB3W+OngV0Yzk/3b/v5P3t3o+uL2ax/y+k9G1841z92Wjb7MHOaTIVGSah lkDu0KmlzydpCtWEd6jnN23x8HMeJCShioxEk4grqGHCI2SyfFpvJocWXxgkUWwaAZlj ZupNjS5i3/08+1JIS0Dn7+irKEoJanDbyd45mmE1tqYBo0ZQAadNNZPCmMnmKQ5sjuuL oX4cE8AGsbBVrI3GWG2PxNOXpUb2EP5MywBHTdamZkolWa/2P84qMJH0uDBYJ7/iXSVO dwsQEV5Zq4nWxpbA9KSL8P9FiTNgXwKkczMFYXbAF/IejlKDfMeeHcrfXmeFgbBKqS/r 9/dQ== 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-transfer-encoding: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=m2NrxwDvChOFQATvPhyO6WrKppV3TNDH2bNaFtDC1J8=; b=hpyuNed43oVJaHHQDV7CKqhjPU8cqkaSLKdwzkQ0/ej5eVhvxIJjerqnRRoc/Q3lNs IyaXlyGsXy9quokKUVM5E5rEaVfU9Rjx2zCHVmYcvLvmg7iG86dGk5awTgzKtGHGW5Hm uJwFwhtuRHALbkEix/h5OlfW9gVOcAfxJ6wECVKNvCIOBvuU2Uw90/rWIoNZuDWYHbFw FIcw+qweSyHX5gj/86xjC0beQ2UNRq/PEdJ3HXqxP9U8xtwrDkuKZLCMcta0ovn1KKyg Sw+y0juMqdZVCulrqh7kfkog37oKqT9YPkDhtPckD9bqLfz5dEI50G7eA4n2GdQRx8xY 3nAw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=crzO+H8I; spf=neutral (google.com: 2607:f8b0:4002:c05::233 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=m2NrxwDvChOFQATvPhyO6WrKppV3TNDH2bNaFtDC1J8=; b=LbABwtCumyKF/FtwePwEWR10qG94SiJwfvzKK64fG9snX5fb4Y7+IX3kePW3XHcTaR inAGgv6J3+lfitYgRzIhH8/04BhApuuuE/dJTrZELwo5psL6rWED3KfWcypIhQXk96vA Sxtmxd58Cig+dZUIbCNrA0khnbhgMtSADegdyrDaJJZmTRmne/q/58wih9oZGs4xlxFz C1hNrgMN8iv7KY7sSNxgkLK/yw/Qs5QGAq1B855ie11uMi9Y2qExItKUsKRCuJE00men 6I1qVGSh5SqU5nJ0NPrlo9ge4Vge0hidd8Lih4JUjWFIuvoQLF+2vGclIMakl1GEUI3j JMaw== 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:content-transfer-encoding :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=m2NrxwDvChOFQATvPhyO6WrKppV3TNDH2bNaFtDC1J8=; b=IjV6LbQWkh9AG0SBVm7EzX0a8S8YieQ5x0U2+zube2F8B12LGC/VSsIyqahpUR9Ygu 4Wb5s7JnVZnt/Lc/KtPjQSgaqdQKUXD1aLpOmoQKcrCDV7vXm0UM5w20cYq6N8vKSFAr /FIB3A6Y1q1w1V01xul79DiC8xhwbg4PyKMZM4a38dteqDZXz5cTcB5ZOU5LS2dhbKqx PNawx1OMYeuWv8aDGf2qPS7qN6HhxEGeOEke9EQrxP1+vtkYffNna35vocgo3L7DKeM6 Py4jXNdpJfMdcPefsxGKE3OiPefmrE9gewq+JeuEwJ8Y32mhifUif57TXU4JijxcrY1g kKeA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E1j+M6Cqx4k7mcBWy1xwu8200/NXzEQxPvxO8OauQ6nzb9WC2DH k7UXS2LELa5gx4K1x+SoIgg= X-Google-Smtp-Source: AAOMgpft4u9f0r+80E/6GJU0avGKPKpSPZLtwmL4ZNELmp9EHCJL9HaJM/veBGaeN0qyA8K4FKHl2g== X-Received: by 2002:a5b:34f:: with SMTP id q15-v6mr73611ybp.7.1530679802477; Tue, 03 Jul 2018 21:50:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:2288:: with SMTP id i130-v6ls78256ywi.26.gmail; Tue, 03 Jul 2018 21:50:02 -0700 (PDT) X-Received: by 2002:a0d:cdc3:: with SMTP id p186-v6mr95611ywd.30.1530679802101; Tue, 03 Jul 2018 21:50:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1530679802; cv=none; d=google.com; s=arc-20160816; b=a8StBTuWch7tamzAVgk9c4nJNrleTTxGYFBvUh05CvQ4EvRVgVLuC4iHvjCJEyy2ba STLZIa9R6NqNHc1da4LJp9I2G9c+KFUx7PRpifvdTKaT1ajztsY1e66SB7Rax4fSr9mw I8dEiKnFGg9WpVBPffoZZi9zo3C8sfzcEC+cRi9hKUPS+gRW52NC9JCjnH/5jjGSpt6K tIMQkkeA2CLlOlZOYtxHDi9Xd5CH1K75usKCrWoD+WHa6SIF4p1HICTc3Q3KrpA345bT /tx5WOWV8wDl4SPAaq8fYlKjf+4KR+g78YCqNKm8RoXFk1FSteu4KdEQ8KXKdt21k5iH PMaA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=dHBrJYf1v1crKiNYRtnJmCCC+D6mXgaExuQTvUUB7Ao=; b=xd4x3nYYn7g2UqK2dxOMmIL8kNRc6A5h8leEb7cRPx12xRYPFNpLBBBrPEtaDG585O ov/cHarW+a5483UPCTfVYPTscEmjLCdUbvTHbuSgNE5Sp++x/c4LsHofD/XaRzHxsqxD cUCwL7hCq6IC8Nh89jhxph00+4qHAYET7HzUlTsttSyLzoxGoc433lcpFkdeqdIDR43j kxpxCa+44v8xqy5w7Dmy9Lvw/JPqR/oSDHB4Vga9kcH6a0RFIN3LbrLRcrCxkQKgnvZo KX1zgIMAoJHdF+orvDQO7T2vKnfXaOS9ncOggjjWqGPzUssgTYty9EFqWxuhLxtNhNPK +ckA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=crzO+H8I; spf=neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw0-x233.google.com (mail-yw0-x233.google.com. [2607:f8b0:4002:c05::233]) by gmr-mx.google.com with ESMTPS id y4-v6si67853ywe.0.2018.07.03.21.50.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 03 Jul 2018 21:50:02 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shulman@sandiego.edu) client-ip=2607:f8b0:4002:c05::233; Received: by mail-yw0-x233.google.com with SMTP id p129-v6so1495486ywg.7 for ; Tue, 03 Jul 2018 21:50:02 -0700 (PDT) X-Received: by 2002:a81:5194:: with SMTP id f142-v6mr205938ywb.46.1530679801735; Tue, 03 Jul 2018 21:50:01 -0700 (PDT) Received: from mail-yw0-f171.google.com (mail-yw0-f171.google.com. [209.85.161.171]) by smtp.gmail.com with ESMTPSA id 131-v6sm1088265ywl.64.2018.07.03.21.50.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 03 Jul 2018 21:50:00 -0700 (PDT) Received: by mail-yw0-f171.google.com with SMTP id k18-v6so1493941ywm.11 for ; Tue, 03 Jul 2018 21:50:00 -0700 (PDT) X-Received: by 2002:a0d:cc8d:: with SMTP id o135-v6mr211360ywd.178.1530679800369; Tue, 03 Jul 2018 21:50:00 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:4094:0:0:0:0:0 with HTTP; Tue, 3 Jul 2018 21:49:39 -0700 (PDT) In-Reply-To: <67d3932e-aa85-41dd-9845-db62e2472772@googlegroups.com> References: <67d3932e-aa85-41dd-9845-db62e2472772@googlegroups.com> From: Michael Shulman Date: Tue, 3 Jul 2018 21:49:39 -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" Content-Transfer-Encoding: quoted-printable 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=crzO+H8I; spf=neutral (google.com: 2607:f8b0:4002:c05::233 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: , We are still working out the details. Semantically, I would certainly expect a "theory" in a DTT to be allowed to assert judgmental equalities. But such theories might be poorly behaved syntactically: allowing the "user" to add judgmental equalities in a DTT tends to break lots of nice type-theoretic properties. I could be wrong though, perhaps someone more knowlegeable could say more -- this isn't really a question about our modal DTT specifically but just more generally about what a dependently typed "theory" is. On Mon, Jul 2, 2018 at 8:38 PM, Matt Oliveri wrote: > I saw Dan Licata's Hausdorf talks about the framework for modal type syst= ems > that he, Mike Shulman, and Mitchell Riley are working on. > > As I understand it, a "mode theory" in this framework specifies a judgmen= tal > structure, and the bold F and U type constructors provide certain type > constructors for each judgmental structure generically. The resulting typ= e > systems correspond to certain doctrines, and each system can be used to > specify theories for structured categories of the corresponding doctrine. > > Neat. Except... theories usually involve equality. What equality is this,= on > the type theory side? In the case of simple type systems, I guess it can > only be judgmental equality. But what about with dependent type systems? > What's the plan? > > If dependently-typed theories could use judgmental equality in axioms, an= d > if one universe (without type constructors) was added to the framework, i= t > seems like each mode theory would yield a system analogous to Martin-L=C3= =B6f's > logical framework (MLLF), so a full constructive type theory could be > specified at the theory level. This sounds nice. > > -- > 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. --=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.