From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7KF3MJXIPBBSG75PMQKGQEARPNBOQ@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.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,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.1 Received: from mail-oi0-x238.google.com (mail-oi0-x238.google.com [IPv6:2607:f8b0:4003:c06::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e29ad082 for ; Tue, 3 Jul 2018 03:38:50 +0000 (UTC) Received: by mail-oi0-x238.google.com with SMTP id q11-v6sf233589oia.21 for ; Mon, 02 Jul 2018 20:38:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=qjn7gQskVigiHs46hO66CbL5kHXz7OK1QN5d1nSdju4=; b=dsXky2S2bt9UfRZlMif693nh//zxJ+DWFQhVoFhDOHvE1avqSe1IsG/8+bDWMxKtN0 tPGHetQUS++FucMsdVi557NHsxRtrLathzBuawVAFaAR1IY3d+lyH2jdRWrq9sGS+9YA LA637IEcdatXm4FSnJAQBNufF/168LJniyENcsR5TqoU/LNHu2LBLHY2KXJ9DxvoCPwp MmgKAOclAU9FtrZg69NyPJzg0yP7l6yHTbSDeeo4C5EubCCW9lKnqrucod8MYkGilhz7 gxiRGi6LaCS3MUy0ocSyGsOm72/8YdUY6mctsrqlnm/enEbGmim5wb1PVfkCXGP0ciFi zcoQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=qjn7gQskVigiHs46hO66CbL5kHXz7OK1QN5d1nSdju4=; b=LxkAgoi1pLQhhLJnWq7WPB0lLcb6OtNSruzsDQAbyWXARhfxVwf7pS8LNpmHQ0TWsa IpFmYftNHF3drTgLX98iJsJmbjDFdMwFBNoeM2IQW3NBFdpOsFLPti5kh2XQ/BsoERkA cBjXNvSaESKwdr6yTF9uNFcnvyri0AjV4pJ5qdPVBj9EjaHKwFOQvS3+380xNDyOhvyi /AtEabBBYtvuFjEcmaniJ9690+k/v0yxOO6us3NXoCqDHEeLMVSEXD2sG6oTYeEVBlxG Qlsl5jmhQOIjlW9EyJCeKiBoqmkzWoi4azug0aLhegbdYBIvD4qtJYQO7XxgIJ73matn hRzw== 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:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=qjn7gQskVigiHs46hO66CbL5kHXz7OK1QN5d1nSdju4=; b=rvIamc1DHmO/Q/dMOehAp5nNlvTVWt6ZSjhTrai4TNJsCz+kBPR/d2imkQI2mX8rQE PS83XC5S+IHvfXFNNKL1tJ9eW07P/behn/JpURbyrqJUQzt0ICWHQxpkFSw704i2WOBv eJT7YTxCWraSsf9lr21vamPSB7+qWB+Yf7mK8groGLuNytwD6y4ZfQfm5SRaSgXEWb8u 5Inw9zHqf+xXCPvYjoUDFfoxZDxL0l8qGW5tWykZm3DdvMKNpETty5wghQ9v7QCMynBa d0RPiS1dExWTUjNMubLEVyTsyhWBQPYYkpAmKpgM8cymKFXOtAndSYUTV29ZL/eaa81d bOVg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E25Z4r+oPVyxUV7divv+Nyo49sQY509O2+FAp/T7Qf2eLPgeXkI 0bqH69eOYDFPeOBKPx+7Hgk= X-Google-Smtp-Source: AAOMgpciarY58InveMqMx8QHq/t0w9a+L7we85b6A/ZH2A+vXheeJeC+rgLxfZu9jeX/eIO6U617nQ== X-Received: by 2002:aca:eb15:: with SMTP id j21-v6mr2856623oih.6.1530589128561; Mon, 02 Jul 2018 20:38:48 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:6748:: with SMTP id b8-v6ls1658632oiy.1.gmail; Mon, 02 Jul 2018 20:38:48 -0700 (PDT) X-Received: by 2002:aca:4787:: with SMTP id u129-v6mr2603687oia.4.1530589128111; Mon, 02 Jul 2018 20:38:48 -0700 (PDT) Date: Mon, 2 Jul 2018 20:38:47 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <67d3932e-aa85-41dd-9845-db62e2472772@googlegroups.com> Subject: [HoTT] Equality in the Model Type Framework MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_34211_1908583715.1530589127238" X-Original-Sender: atmacen@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: , ------=_Part_34211_1908583715.1530589127238 Content-Type: multipart/alternative; boundary="----=_Part_34212_2093751437.1530589127238" ------=_Part_34212_2093751437.1530589127238 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I saw Dan Licata's Hausdorf talks about the framework for modal type=20 systems that he, Mike Shulman, and Mitchell Riley are working on. As I understand it, a "mode theory" in this framework specifies a=20 judgmental structure, and the bold F and U type constructors provide=20 certain type constructors for each judgmental structure generically. The=20 resulting type systems correspond to certain doctrines, and each system can= =20 be used to specify theories for structured categories of the corresponding= =20 doctrine. Neat. Except... theories usually involve equality. What equality is this,= =20 on the type theory side? In the case of simple type systems, I guess it can= =20 only be judgmental equality. But what about with dependent type systems?=20 What's the plan? If dependently-typed theories could use judgmental equality in axioms, and= =20 if one universe (without type constructors) was added to the framework, it= =20 seems like each mode theory would yield a system analogous to Martin-L=C3= =B6f's=20 logical framework (MLLF), so a full constructive type theory could be=20 specified at the theory level. This sounds nice. --=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. ------=_Part_34212_2093751437.1530589127238 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I saw Dan Licata's Hausdorf talks about the framework = for modal type systems that he, Mike Shulman, and Mitchell Riley are workin= g on.

As I understand it, a "mode theory" in this framewor= k specifies a judgmental structure, and the bold F and U type constructors = provide certain type constructors for each judgmental structure generically= . The resulting type systems correspond to certain doctrines, and each syst= em can be used to specify theories for structured categories of the corresp= onding 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 de= pendent type systems? What's the plan?

If dependently-typed theo= ries could use judgmental equality in axioms, and if one universe (without = type constructors) was added to the framework, it seems like each mode theo= ry would yield a system analogous to Martin-L=C3=B6f's logical framewor= k (MLLF), so a full constructive type theory could be specified at the theo= ry level. This sounds nice.

--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_34212_2093751437.1530589127238-- ------=_Part_34211_1908583715.1530589127238--