From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7KF3MJXIPBBYHH63MQKGQEH2IXV3Y@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-x237.google.com (mail-oi0-x237.google.com [IPv6:2607:f8b0:4003:c06::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b79cb030 for ; Thu, 5 Jul 2018 06:00:03 +0000 (UTC) Received: by mail-oi0-x237.google.com with SMTP id 13-v6sf6160461oiq.1 for ; Wed, 04 Jul 2018 23:00:03 -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=5gUgBgjEJeQvnrp64gOgl0tH4Bu+QkyHrZdAffq6/PM=; b=IIRzIFK5uLTz2Ssu08LBb4Fe3YA7ARQeooy/5xJmRaB+lwQtdEK3+wbFds6ZRPgKnY 7yRJoX/q3YpEv3F2zw/nOBEYO3iRD8svBbnFPx9RRxY3EseVWTdQW6yTSBEwynXdy1sG 9IgbI6HR9W+n2PYUafW9jNxHtVjeV83TiyrjaCnC60FeYrZKRCZcsmUh+NRJV+fpy7xF GmDAT0xd7MVfm2GSV9LqXptT0h1Jf0zD4lmCxOquAATyp62gXw0MJ+XAdIhEzLLzQJp1 CsapwuZkE7MjLPH8voy2KkSI3/ab8CNkyXyBiFPWErVwv5CuWuddlMl2yDBdKh2PiY+S eg3g== 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=5gUgBgjEJeQvnrp64gOgl0tH4Bu+QkyHrZdAffq6/PM=; b=jQj7mC8ELs9/Uk50tiT30roGmQQrhI2ff/X2RftERzQtjzAu8FdpCr3hJbiTcANFPL +wF7k/g0j0kFJblDeUxADzEGof24MZw6fan4Zs3TWPFIRt4R2rUgohdEx8RFiSrfTuU0 m4FSBj9kE903ETd5bqrz65cQFKjaVJy2a6G2YU5LrVqpxqEjnvSqQ93rmQOMqTLK4+Oh wWkXS9ZUxY0NaZgNPZq0ARIwPDHQYmiHMu4otbIOdtcoFIXvjjSG50DWprft35qRgDU5 AwTFjJie5D2ZaDWrCXpzMsmNwXPJj7N5TRwMRq+UqFH+KWatqg0tY9NgwMUqSfAyuxMP 9CBw== 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=5gUgBgjEJeQvnrp64gOgl0tH4Bu+QkyHrZdAffq6/PM=; b=khLFb4EWqGn0pNvAgxg0g5bpArI1PGwXF71l7Hqjsdd2ZCfLGYScyVwXbQsPDYaqrY IKU2zJbCqxBrO0glkQXZzK4kGZ/6EO3cZNpdPh7qk/aeHwvdZifaoVvRtF8WXEymLyFr qBUgDVASSKspaiooBCXkwFRH0iMmvQYE53weR56cqbN2CfMFtTIASNwbV9cV7dAmRe1f YhOuKnzQagvuz+CcVasH1LWGMc+74YTF2e+SERoTH635KCVpaQgQQrL23NKLENYGvxAq ugyDygWWeb75lEOKx2C0PhkoQhbFTH0Kvv+bVok+mEhYGwGsqvTOmsYa1pPSNJHoJAHd P5kw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E3FU4Qeylr5NvxhrIN1IO2xL38dTqAs5nzOgFjQLyROPj/Xa4Qo HGQN73+PZew6+RkJPh+7ing= X-Google-Smtp-Source: AAOMgpe0Oc0xdTYlH2naJ3jOq52BkDH5RvDpbQoaUSYfacyFfyc9IgXp+ym3N38nRCER4G+d88IDew== X-Received: by 2002:aca:c6ca:: with SMTP id w193-v6mr1066692oif.1.1530770400899; Wed, 04 Jul 2018 23:00:00 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:430a:: with SMTP id q10-v6ls390976oia.15.gmail; Wed, 04 Jul 2018 23:00:00 -0700 (PDT) X-Received: by 2002:aca:eb15:: with SMTP id j21-v6mr1076754oih.6.1530770400325; Wed, 04 Jul 2018 23:00:00 -0700 (PDT) Date: Wed, 4 Jul 2018 22:59:59 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: References: <67d3932e-aa85-41dd-9845-db62e2472772@googlegroups.com> <0137f575-f414-47ea-9264-47ddbf5d38f6@googlegroups.com> Subject: Re: [HoTT] Equality in the Model Type Framework MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_9024_990207549.1530770399668" 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_9024_990207549.1530770399668 Content-Type: multipart/alternative; boundary="----=_Part_9025_1065397834.1530770399668" ------=_Part_9025_1065397834.1530770399668 Content-Type: text/plain; charset="UTF-8" On Thursday, July 5, 2018 at 12:00:25 AM UTC-4, Michael Shulman wrote: > > So the things that a theory is "allowed to do" are a > subset of the things a doctrine is "allowed to do", but what gets > excluded is the "stuff" at the categorical top dimension, not the > "properties" (equations) at the categorical bottom dimension. > 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.) I believe intensional MLTT, at least, should be described by the > "tautological" or "simplest possible" mode theory with just one > comprehension-category mode and enough of the relevant F- and U-types, > including "indexed F-types" that specialize to Id-types. Would this support W types in the doctrine? Universes? Do universes somehow pop up out of the new U types, or are they special? -- 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_9025_1065397834.1530770399668 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Thursday, July 5, 2018 at 12:00:25 AM UTC-4, Michael Sh= ulman wrote:
So the things that= a theory is "allowed to do" are a
subset of the things a doctrine is "allowed to do", but what = gets
excluded is the "stuff" at the categorical top dimension, not= the
"properties" (equations) at the categorical bottom dimension.=

So on the syntactic side, this is saying that the= ories can't add constants or equations to the mode theory? (Like flat a= nd idempotence of flat.)

I believe intensional MLTT, at least, should be described by the
"tautological" or "simplest possible" mode theory w= ith just one
comprehension-category mode and enough of the relevant F- and U-types,
including "indexed F-types" that specialize to Id-types.

Would this support W types in the doctrine? Universes? Do = universes somehow pop up out of the new U types, or are they special?

--
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_9025_1065397834.1530770399668-- ------=_Part_9024_990207549.1530770399668--