From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7KF3MJXIPBBVU36TMQKGQE5D2BMVY@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 8d392991 for ; Wed, 4 Jul 2018 18:11:37 +0000 (UTC) Received: by mail-oi0-x238.google.com with SMTP id e29-v6sf4229837oiy.2 for ; Wed, 04 Jul 2018 11:11:37 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=qPEqZIixl2RlZeoE0snKHLVUj+Nmte5jAMk1qpmjJts=; b=CYJEk7bC9aZiwAC2gl/2klj09SnFgCGz4Zy6jvGY+h/KQzfMzC+UkkWdHIsgyoEtlX URdtDphlClU5MwJoIZsItkn6DdBdv4cpF4o7Wo7ka9MTl7L2Kl7ANDtXG54OK9AIDeX/ NE/3HH+q/VgtfbhKDsw5zTkd/i0n+vGXzQXCz06LJRvhGJZtGVYJGtU2LfjEpKL77WBo ID+c82Ne5iWqZDj9EkLw6veFfk3g1lKl97i7MmJ6OIQGhIU07QUFkSs08jwJCJVw5iQ3 8pXJJZb/ptelOgHfnmd5RWVO8oK6d68Xn4A335o48Bb561YYb3V9SZhHqm1oxZy7tI+a 3ttg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=qPEqZIixl2RlZeoE0snKHLVUj+Nmte5jAMk1qpmjJts=; b=GNQFbJOt/dhURi3GCWIOCgeI1ywm8sL1XyEK5o9xL9CWBa2T/8wKIQ/HNkp5E1BgJG 34eYAxdJcBxf3LpNGzd5rbHdxnb71bR5HgJI9pwCHmkQhvqXGJb2Bb3Hdp7aQC1O13ia XLDJrxRHydA2vcNSt506/FwF/qL5VXA1H9Wk0FwmmImIRZ2NGKF0Ro5hfqCOQsb96es6 kdu9ZKBhG73EQ8Xbqg8ZenhlxukvgrMPlZUirHUyZSuJQE2efm7C2v8f6uocfzoniiQm W/D2cw5RoPm3IwUd8uXUs7Z2oeNLnCqOrrRX7RjcjTAqCSg1hHbZmlmlb5bGFiIBB46U rVww== 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:in-reply-to :references: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=qPEqZIixl2RlZeoE0snKHLVUj+Nmte5jAMk1qpmjJts=; b=YTa4wbIxn9SrEFzqQifHCUHH10uo2PTxMnZcS9KApKJONzFdXumDZ2NyNGHgKgS8oA hoH5DP9fpjNm98WQ2xAA6hOqRCwbrIY0szHdVLz69tewCr1ZxEVD9VpsFq8zyItfBLbo v1klgxRvJQenbdEAWb7pMQgRspjHaDqFRHx2QyRv8pgNX0jX2bHVs1j06XxAoEiMvKNf OsxSsMCqIxaaDzHTbwYGQjasR883zVUBsLRXsW4R1Xrak2IEk0clOoJ/Hd8J0SxkUcHC LW/XviJDRk6d+I9CLoK62lS2TlQFCiKrj/ptZr/GCJX1lL14V1SC/DvW9GeLorWqEYG2 X1RQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E0mb/or9fTkNISErdkaFmR/c/01FK47GYVP1pw9iFdUgCRX8zlb /3rV9Uew/HTZB/lrFU6KifQ= X-Google-Smtp-Source: AAOMgpcdPnbstcE6506/rRzA7ullCRIQQ672N0jbmgAKIDUKk0/PKOcuSXYGU0WmIwp/2VNLeU7IdQ== X-Received: by 2002:aca:f495:: with SMTP id s143-v6mr584772oih.7.1530727895137; Wed, 04 Jul 2018 11:11:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:908:: with SMTP id 8-v6ls1564578oij.20.gmail; Wed, 04 Jul 2018 11:11:34 -0700 (PDT) X-Received: by 2002:aca:c6ca:: with SMTP id w193-v6mr582979oif.1.1530727894613; Wed, 04 Jul 2018 11:11:34 -0700 (PDT) Date: Wed, 4 Jul 2018 11:11:34 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <0137f575-f414-47ea-9264-47ddbf5d38f6@googlegroups.com> In-Reply-To: References: <67d3932e-aa85-41dd-9845-db62e2472772@googlegroups.com> Subject: Re: [HoTT] Equality in the Model Type Framework MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_47484_225495909.1530727894088" 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_47484_225495909.1530727894088 Content-Type: multipart/alternative; boundary="----=_Part_47485_1964029762.1530727894088" ------=_Part_47485_1964029762.1530727894088 Content-Type: text/plain; charset="UTF-8" On Wednesday, July 4, 2018 at 12:50:03 AM UTC-4, Michael Shulman wrote: > > We are still working out the details. I'm looking forward to more 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. Basically; yeah. In more detail, your approach seems to have three stages: 1) specify a mode theory 2) specify a theory in the resulting doctrine 3) use it I figured the user could only add judgmental equalities in stage (2). The equations in stage (1) seem like something else (usually "WLOGed" away in the syntax), and the equations in stage (3) are typal equality. I was guessing/hoping that the nice syntactic properties would only cover the type system corresponding to the doctrine, and not cover the additional constants and equations added in stage (2). Dan already pointed out in his third Hausdorff talk that MLTT doesn't have the subformula property. So it sure looks like user-specified constants and equations at stage (2) rules that out. My impression was that you should not expect the subformula property in a theory with logical strength. Arbitrary equations rules out normalization too, because they could add equality reflection. Although I don't recommend it, it should be possible to impose a restricted way of adding equations, so that the system remains normalizing. Justifying such a framework would be tricky without putting an upper bound on the proof-theoretic strength of the normalization metatheorem. With equality reflection, the operational semantics and judgmental equality become separate. Computational type theory is a way of getting a lot of flexibility for equations while keeping canonicity. (Strong normalization is not available.) Judgmental equality of t and t' in type T means that computations t and t' implement the same element of T. But it seems like that would be a big detour for you. Really though, I don't think the nice syntactic properties should be a concern when designing the *categorical* semantics of a full blown dependent type theory. That's why I was hoping they would only pertain to the bare doctrine. this isn't > really a question about our modal DTT specifically but just more > generally about what a dependently typed "theory" is. > Wait a minute. Looking back at your "What Is an n-Theory?" post, you were thinking of things like HoTT and cubical type theory as doctrines. I don't understand how this fits with the modal type framework. A mode theory will not be enough to specify that kind of doctrine, will it? And if those are doctrines, why do theories also get judgmental equations? What are theories used for? -- 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. ------=_Part_47485_1964029762.1530727894088 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Wednesday, July 4, 2018 at 12:50:03 AM UTC-4, Michael S= hulman wrote:
We are still work= ing out the details.

I'm looking forward to more d= etails!

Semantica= lly, I would certainly
expect a "theory" in a DTT to be allowed to assert judgmental
equalities.=C2=A0 But such theories might be poorly behaved syntactical= ly:
allowing the = "user" to add judgmental equalities in a DTT tends to
break lots of nice type-theoretic properties.

Basi= cally; yeah.

In more detail, your approach seems to have three stage= s:
1) specify a mode theory
2) specify a theory in the resulting doct= rine
3) use it

I figured the user could only add judgmental equal= ities in stage (2). The equations in stage (1) seem like something else (us= ually "WLOGed" away in the syntax), and the equations in stage (3= ) are typal equality.

I was guessing/hoping that the nice syntactic = properties would only cover the type system corresponding to the doctrine, = and not cover the additional constants and equations added in stage (2).
Dan already pointed out in his third Hausdorff talk that MLTT doesn= 9;t have the subformula property. So it sure looks like user-specified cons= tants and equations at stage (2) rules that out. My impression was that you= should not expect the subformula property in a theory with logical strengt= h.

Arbitrary equations rules out normalization too, because they cou= ld add equality reflection. Although I don't recommend it, it should be= possible to impose a restricted way of adding equations, so that the syste= m remains normalizing. Justifying such a framework would be tricky without = putting an upper bound on the proof-theoretic strength of the normalization= metatheorem.

With equality reflection, the operational semantics an= d judgmental equality become separate. Computational type theory is a way o= f getting a lot of flexibility for equations while keeping canonicity. (Str= ong normalization is not available.) Judgmental equality of t and t' in= type T means that computations t and t' implement the same element of = T. But it seems like that would be a big detour for you.

Really thou= gh, I don't think the nice syntactic properties should be a concern whe= n designing the categorical semantics of a full blown dependent type= theory. That's why I was hoping they would only pertain to the bare do= ctrine.

this isn&= #39;t
really a question about our modal DTT specifically but just more
generally about what a dependently typed "theory" is.

Wait a minute. Looking back at your "What Is an n-Th= eory?" post, you were thinking of things like HoTT and cubical type th= eory as doctrines. I don't understand how this fits with the modal type= framework. A mode theory will not be enough to specify that kind of doctri= ne, will it? And if those are doctrines, why do theories also get judgmenta= l equations? What are theories used for?

--
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_47485_1964029762.1530727894088-- ------=_Part_47484_225495909.1530727894088--