From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7KF3MJXIPBBKWD53MQKGQEZZTNPOY@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-x23a.google.com (mail-oi0-x23a.google.com [IPv6:2607:f8b0:4003:c06::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5f432641 for ; Tue, 3 Jul 2018 16:17:48 +0000 (UTC) Received: by mail-oi0-x23a.google.com with SMTP id j5-v6sf1621015oiw.13 for ; Tue, 03 Jul 2018 09:17:47 -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=UKapppqCeBde3L2Y/zAwleLG5VIqUvE3/vqz7DJYiSU=; b=M4kcgOuf/dQmoyxpYj+XQycEbH1RJMDa8n71hkhUulBy3MhTReZVBGhxr0xUNHlKdl LZ4+nLBD/BG97id0pxSrqC/fclyZZPH4R3jPOK10oNnDP+ru9ip20s5MZxKSMV0R3bpt JmGh/Tl2K3JE6/KPoWe4KIay/IFM8Qv9Ss3pqiUZ0ktxzGYtnZZ0V2VXD8Dril/riGLe xqjNxkK2A8P5+JuWp9lHwFpAiG/saExviA0nZv+H7qZgzFwRQhjgUDM6CLieSUh4quNw 38kwXZE1v81E3JOczt5nqv/r1k8SKd1H+2I4FmBrsmUAQTm2xKtKFB8GUlQSnzHWE6HP +Xyg== 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=UKapppqCeBde3L2Y/zAwleLG5VIqUvE3/vqz7DJYiSU=; b=fO4vD40/+Lo/rstgcraj/scYFzSTgWxvsNssed3ig1W8Hop6LvZKAYLOURLCyRmUHd Edj7V1rQXBDjcr5P7PMaI0NpbAEso7pgcll6EP6mUtwu1K/gomP67oHi51c2len4x524 XMgUBtg8hw+VMLdoshuCPdXLbmSPHG8DQjSu0UN85gXlEJ/fXyzomHQqBECrvtqUV2ie yVAAjbzZVj0TfzlPny2vQSkUgxXBqODn0gzLRz5vzlBZntAlZYei4nuvxA9aAe1Egdtd m1o4fHxY5wJyZw9kYcFoOIlBThoweKeiWLxr+8lXXLK2rYWahl5CrgS0NO0Mj5u1sDQE toWQ== 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=UKapppqCeBde3L2Y/zAwleLG5VIqUvE3/vqz7DJYiSU=; b=Hj9D6cWqBk9c8K+ZL3lLpFyT3Vkw4AOwMjpoKnp4oRm7WcWh/NXO6ocHwGi4zaBrAw Pe3i45d5elUaPXRlVirJBpjgz3gyNp4fFCZMlMmDc731LXKGCjOFFwJ2h3/OTWjTMfuF QIG0t5qezEK3CEnGNeYl3DXM1ANMHjCDj3dR+UIVeHaywlVo64ZwQxrlmNibaY+WZLsV 0uKpz5WG1LuzXonyN7B1FLS09QN9XJX8zLDL6OfeROvm5ChIU4Su2l3C+Q3AoTfzxOU4 HGWeI9IEOkbztMPajToNjYMpDwbkpEfHaPPsJEpnqOAxNrckS+bq2tV+BNA2Jr9uUuXo kD8Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E0LETLP5oAuEZnjM9lHNx+3YkTazssoTmQNCyf6DEwqKyZCk8E2 FIPZLgWuvRKAoJIxi0XcYLA= X-Google-Smtp-Source: AAOMgpeRbM1d71VPLx/qbONW+jYJ96doIEwQtEAqzTi7cSK27yc2J4ByjECTbATKrBMZRs9kiRXHZQ== X-Received: by 2002:aca:2b06:: with SMTP id i6-v6mr540504oik.0.1530634666691; Tue, 03 Jul 2018 09:17:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:6c54:: with SMTP id h81-v6ls5957090oic.9.gmail; Tue, 03 Jul 2018 09:17:46 -0700 (PDT) X-Received: by 2002:aca:2b06:: with SMTP id i6-v6mr540502oik.0.1530634666258; Tue, 03 Jul 2018 09:17:46 -0700 (PDT) Date: Tue, 3 Jul 2018 09:17:25 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <4bec4b2f-117c-403d-a5a3-f14b9d3b8198@googlegroups.com> In-Reply-To: <67d3932e-aa85-41dd-9845-db62e2472772@googlegroups.com> References: <67d3932e-aa85-41dd-9845-db62e2472772@googlegroups.com> Subject: [HoTT] Re: Equality in the Model Type Framework MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_17567_2119409666.1530634645787" 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_17567_2119409666.1530634645787 Content-Type: multipart/alternative; boundary="----=_Part_17568_1477414811.1530634645788" ------=_Part_17568_1477414811.1530634645788 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Monday, July 2, 2018 at 11:38:47 PM UTC-4, Matt Oliveri wrote: > > If dependently-typed theories could use judgmental equality in axioms, an= d=20 > if one universe (without type constructors) was added to the framework, i= t=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. > Come to think of it, this last part probably isn't right. Internal=20 implication-like connectives generally wouldn't work with modes and=20 substructure the way rules should. Still wondering about equality. --=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_17568_1477414811.1530634645788 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Monday, July 2, 2018 at 11:38:47 PM UTC-4, Matt Oliveri= wrote:
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 cou= ld be specified at the theory level. This sounds nice.

Come to think of it, this last part probably isn't right. In= ternal implication-like connectives generally wouldn't work with modes = and substructure the way rules should.
Still wondering about equality.

--
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_17568_1477414811.1530634645788-- ------=_Part_17567_2119409666.1530634645787--